{D : Diagram G} `(C : Cone X _ D) : cone_precompose C idmap = C. 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.