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