{D : Diagram G} `(C : Cocone _ D X) : cocone_postcompose C idmap = C. Proof. srapply path_cocone; intro i. 1: reflexivity. intros j g x; simpl. apply equiv_p1_1q, ap_idmap. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.