{G : Graph} {D : Diagram G} (P : Type) (C : Cocone D P) : Colimit D -> P. Proof. srapply (Colimit_ind _ C). intros i j g x. refine (transport_const _ _ @ _). apply legs_comm. 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.