proposition: Theorem colimit_adjoint `{Funext} {G : Graph} {D : Diagram G} {C : Type} : (Colimit D -> C) <~> DiagramMap D (diagram_const C).
proof: Proof. symmetry. refine (equiv_colimit_rec C oE _). apply equiv_diagram_const_cocone. Defined.
imports: Basics Types Diagrams.Diagram Diagrams.Graph Diagrams.Cocone Diagrams.ConstantDiagram Colimits.Coeq