Diagram G. Proof. srapply Build_Diagram. - exact (fun i => A * (D i)). - simpl; intros i j f x. exact (fst x, D _f f (snd x)). Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Colimits.Colimit. Require Import Colimits.Colimit_Sigma. Require Import Diagrams.Graph.