cocone_E' : Cocone (diagram_sigma E) (sig E'). Proof. srapply Build_Cocone; cbn. - intros i w. exists (colim i w.1); cbn. exact w.2. - intros i j g x; cbn. srapply path_sigma'. + apply colimp. + apply transport_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.