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