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