Colimit (diagram_sigma E) <~> sig E'. Proof. srapply colimit_unicity. 3: apply iscolimit_colimit. rapply Build_IsColimit. apply unicocone_cocone_E'. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Diagrams.DDiagram. Require Import Colimits.Colimit.