(C : Cone X D) {Y : Type} (f : Y -> X) : Cone Y D. Proof. srapply Build_Cone; intro i. 1: exact (C i o f). intros j g x. apply legs_comm. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.