(D : Diagram G) (X : Type) : cocone_precompose (X:=X) (diagram_idmap D) == idmap. Proof. intro C; srapply path_cocone; simpl. 1: reflexivity. intros; simpl. apply concat_p1. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Graph. Require Import Diagrams.Diagram.