(C : forall y, Cocone (D y) (Q y)) : Cocone sigma_diagram (sig Q). Proof. srapply Build_Cocone; simpl; intros i x. 1: exact (x.1; legs (C x.1) i x.2). simpl; intros g x'. srapply path_sigma'. 1: reflexivity. apply legs_comm. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Colimits.Colimit.