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