`{Funext} {G : Graph} {D : Diagram G} {C : Type} : (Colimit D -> C) <~> DiagramMap D (diagram_const C). Proof. symmetry. refine (equiv_colimit_rec C oE _). apply equiv_diagram_const_cocone. 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.