{D1 D2 : Diagram G} (m : DiagramMap D1 D2) `(f : X -> Y) (C : Cocone D2 X) : cocone_postcompose (cocone_precompose m C) f = cocone_precompose m (cocone_postcompose C f). Proof. srapply path_cocone; intro i. 1: reflexivity. intros j g x; simpl. apply equiv_p1_1q. etransitivity. + apply ap_pp. + apply ap10, ap. symmetry. apply ap_compose. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.