(HQ : forall y, IsColimit (D y) (Q y)) : IsColimit sigma_diagram (sig Q). Proof. pose (SigmaC := sigma_cocone (fun y => HQ y)). srapply (Build_IsColimit SigmaC). srapply Build_UniversalCocone. intros X; srapply isequiv_adjointify. - intros CX x. srapply (cocone_postcompose_inv (HQ x.1) _ x.2). srapply (cocone_precompose _ CX). apply sigma_diagram_map. - intro CX. pose (CXy := fun y => cocone_precompose (sigma_diagram_map y) CX). change (cocone_postcompose SigmaC (fun x => cocone_postcompose_inv (HQ x.1) (CXy x.1) x.2) = CX). srapply path_cocone; simpl. + intros i x. change (legs (cocone_postcompose (HQ x.1) (cocone_postcompose_inv (HQ x.1) (CXy x.1))) i x.2 = CX i x). exact (ap10 (apD10 (ap legs (eisretr (cocone_postcompose (HQ x.1)) (CXy _))) i) x.2). + intros i j g [y x]; simpl. set (py := (eisretr (cocone_postcompose (HQ y)) (CXy y))). set (py1 := ap legs py). specialize (apD legs_comm py); intro py2. simpl in *. rewrite (path_forall _ _(transport_forall_constant _ _)) in py2. apply apD10 in py2; specialize (py2 i); simpl in py2. rewrite (path_forall _ _(transport_forall_constant _ _)) in py2. apply apD10 in py2; specialize (py2 j); simpl in py2. rewrite (path_forall _ _(transport_forall_constant _ _)) in py2. apply apD10 in py2; specialize (py2 g); simpl in py2. rewrite (path_forall _ _(transport_forall_constant _ _)) in py2. apply apD10 in py2; specialize (py2 x); simpl in py2. rewrite transport_paths_FlFr in py2. rewrite concat_1p, concat_pp_p in py2. apply moveL_Mp in py2. rewrite (ap_path_sigma_1p (fun x01 x02 => cocone_postcompose_inv (HQ x01) (CXy x01) x02)). *) subst py1. etransitivity. * etransitivity. 2:exact py2. apply ap. rewrite (ap_compose legs (fun x0 => x0 i x)). rewrite (ap_apply_lD2 _ i x). reflexivity. * apply ap10, ap. rewrite (ap_compose legs (fun x0 => x0 j _)). rewrite (ap_apply_lD2 _ j _). reflexivity. - intros f. apply path_forall; intros [y x]; simpl. rewrite <- cocone_precompose_postcompose. srapply (apD10 (g := fun x => f (y; x)) _ x). snrapply equiv_moveR_equiv_V. srapply path_cocone. 1: reflexivity. intros i j g x'; simpl. hott_simpl. exact (ap_compose _ _ _)^. Defined.
Require Import Basics. Require Import Types. Require Import Diagrams.Diagram. Require Import Diagrams.Graph. Require Import Diagrams.Cocone. Require Import Colimits.Colimit.