{D1 D2 D3 : Diagram G} (m2 : DiagramMap D2 D3) (m1 : DiagramMap D1 D2) (X : Type) : (cocone_precompose (X:=X) m1) o (cocone_precompose m2) == cocone_precompose (diagram_comp m2 m1). Proof. intro C; simpl. srapply path_cocone. 1: reflexivity. intros i j g x; simpl. apply equiv_p1_1q. unfold CommutativeSquares.comm_square_comp. refine (concat_p_pp _ _ _ @ _). apply ap10, ap. rewrite 3 ap_V. refine ((inv_pp _ _)^ @ _). apply inverse2. rewrite ap_pp. apply ap. by rewrite ap_compose. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.