Diagram G. Proof. srapply Build_Diagram. - exact (fun i => {y: Y & D y i}). - simpl; intros i j g x. exact (x.1; D x.1 _f g x.2). Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Colimits.Colimit.