{G : Graph} (D : Diagram G) : Cocone D (Colimit D) := Build_Cocone colim colimp. Global Instance unicocone_colimit `{Funext} {G : Graph} (D : Diagram G) : UniversalCocone ( D). Proof. srapply Build_UniversalCocone; intro Y. srapply (isequiv_adjointify _ (Colimit_rec Y) _ _). - intros C. srapply path_cocone. 1: reflexivity. intros i j f x; simpl. apply equiv_p1_1q. apply Colimit_rec_beta_colimp. - intro f. apply path_forall. srapply Colimit_ind. 1: reflexivity. intros i j g x; simpl. nrapply (transport_paths_FlFr' (g:=f)). apply equiv_p1_1q. apply Colimit_rec_beta_colimp. Defined.
Require Import Basics Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Diagrams.ConstantDiagram. Require Import Colimits.Coeq.