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