{D : Diagram G} `(f : X -> Y) `(g : Y -> Z) (C : Cocone D X) : cocone_postcompose C (g o f) = cocone_postcompose (cocone_postcompose C f) g. Proof. srapply path_cocone; intro i. 1: reflexivity. intros j h x; simpl. apply equiv_p1_1q, ap_compose. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.