{D1 D2: Diagram G} (m : DiagramMap D1 D2) {X} : (Cocone D2 X) -> (Cocone D1 X). Proof. intro C. srapply Build_Cocone; intro i. 1: exact (C i o m i). intros j g x; simpl. etransitivity. + apply ap. symmetry. apply DiagramMap_comm. + apply legs_comm. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.