(D : Diagram G) (X : Type) : cone_postcompose (X:=X) (diagram_idmap D) == idmap. Proof. intro C; srapply path_cone; simpl. 1: reflexivity. intros; simpl. refine (_ @ (concat_1p _)^). refine (concat_p1 _ @ concat_1p _ @ ap_idmap _). Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.