(y: Y) : DiagramMap (D y) sigma_diagram. Proof. srapply Build_DiagramMap. 1: exact (fun i x => (y; x)). reflexivity. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Colimits.Colimit.