sigma_diagram (fun _ : A => D) ~d~ prod_diagram. Proof. unshelve econstructor. - srapply Build_DiagramMap; cbn. + intro i; apply equiv_sigma_prod0. + reflexivity. - intro i; cbn. apply equiv_sigma_prod0. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Colimits.Colimit. Require Import Colimits.Colimit_Sigma. Require Import Diagrams.Graph.