Require Import UniMath.Foundations.PartD.
Require Import UniMath.Foundations.Propositions.
Require Import UniMath.Foundations.Sets.
Require Import UniMath.Foundations.NaturalNumbers.
Require Import UniMath.MoreFoundations.Tactics.

Require Import UniMath.CategoryTheory.total2_paths.
Require Import UniMath.CategoryTheory.Categories.
Require Import UniMath.CategoryTheory.functor_categories.
Require Import UniMath.CategoryTheory.limits.graphs.colimits.
Require Import UniMath.CategoryTheory.categories.HSET.Core.
Require Import UniMath.CategoryTheory.categories.HSET.Slice.
Require Import UniMath.CategoryTheory.categories.HSET.Limits.
Require Import UniMath.CategoryTheory.categories.HSET.Colimits.
Require Import UniMath.CategoryTheory.categories.HSET.Structures.
Require Import UniMath.CategoryTheory.limits.initial.
Require Import UniMath.CategoryTheory.FunctorAlgebras.
Require Import UniMath.CategoryTheory.limits.binproducts.
Require Import UniMath.CategoryTheory.limits.products.
Require Import UniMath.CategoryTheory.limits.bincoproducts.
Require Import UniMath.CategoryTheory.limits.coproducts.
Require Import UniMath.CategoryTheory.limits.terminal.
Require Import UniMath.CategoryTheory.limits.graphs.limits.
Require Import UniMath.CategoryTheory.PrecategoryBinProduct.
Require Import UniMath.CategoryTheory.ProductCategory.
Require Import UniMath.CategoryTheory.Adjunctions.
Require Import UniMath.CategoryTheory.EquivalencesExamples.
Require Import UniMath.CategoryTheory.exponentials.
Require Import UniMath.CategoryTheory.whiskering.
Require Import UniMath.CategoryTheory.RightKanExtension.
Require Import UniMath.CategoryTheory.slicecat.

Require Import UniMath.CategoryTheory.Chains.Chains.

Local Open Scope cat.

Section cocont_functors.

Lemma left_adjoint_cocont {C D : precategory} (F : functor C D)
  (H : is_left_adjoint F) (hsC : has_homsets C) (hsD : has_homsets D) : is_cocont F.
Proof.
now intros g d L ccL; apply left_adjoint_preserves_colimit.
Defined.

Section cocont_iso.

Context {C D : precategory} (hsD : has_homsets D) {F G : functor C D}
        (αiso : @iso [C,D,hsD] F G).

Section preserves_colimit_iso.

Context {g : graph} (d : diagram g C) (L : C) (cc : cocone d L) (HF : preserves_colimit F d L cc).

Let αinv := inv_from_iso αiso.
Let α := pr1 αiso.
Let Hα : is_iso α := pr2 αiso.

Local Definition ccFy y (ccGy : cocone (mapdiagram G d) y) : cocone (mapdiagram F d) y.
Proof.
use mk_cocone.
- intro v; apply (pr1 α (dob d v) · coconeIn ccGy v).
- abstract (simpl; intros u v e; rewrite <- (coconeInCommutes ccGy u v e), !assoc;
            apply cancel_postcomposition, nat_trans_ax).
Defined.

Lemma αinv_f_commutes y (ccGy : cocone (mapdiagram G d) y) (f : D⟦F L,y⟧)
       (Hf : ∏ v,coconeIn (mapcocone F d cc) v · f = coconeIn (ccFy y ccGy) v) :
       ∏ v, # G (coconeIn cc v) · (pr1 αinv L · f) = coconeIn ccGy v.
Proof.
intro v; rewrite assoc.
eapply pathscomp0; [apply cancel_postcomposition, nat_trans_ax|].
rewrite <- assoc; eapply pathscomp0; [apply maponpaths, (Hf v)|]; simpl; rewrite assoc.
eapply pathscomp0.
  apply cancel_postcomposition.
  apply (nat_trans_eq_pointwise (@iso_after_iso_inv [C,D,hsD] _ _ (isopair _ Hα))).
now rewrite id_left.
Qed.

Lemma αinv_f_unique y (ccGy : cocone (mapdiagram G d) y) (f : D⟦F L,y⟧)
     (Hf : ∏ v,coconeIn (mapcocone F d cc) v · f = coconeIn (ccFy y ccGy) v)
     (HHf : ∏ t : ∑ x, ∏ v, coconeIn (mapcocone F d cc) v · x = coconeIn _ v, t = f,, Hf)
      f' (Hf' : ∏ v, # G (coconeIn cc v) · f' = coconeIn ccGy v) :
      f' = pr1 αinv L · f.
Proof.
transparent assert (HH : (∑ x : D ⟦ F L, y ⟧,
            ∏ v : vertex g,
            coconeIn (mapcocone F d cc) v · x = coconeIn (ccFy y ccGy) v)).
{ use tpair.
  - apply (pr1 α L · f').
  - cbn. abstract (intro v; rewrite <- Hf', !assoc; apply cancel_postcomposition, nat_trans_ax).
}
apply pathsinv0.
generalize (maponpaths pr1 (HHf HH)); intro Htemp; simpl in ×.
rewrite <- Htemp; simpl; rewrite assoc.
eapply pathscomp0.
  apply cancel_postcomposition.
  apply (nat_trans_eq_pointwise (@iso_after_iso_inv [C,D,hsD] _ _ (isopair _ Hα))).
now apply id_left.
Qed.

Lemma preserves_colimit_iso : preserves_colimit G d L cc.
Proof.
intros HccL y ccGy.
set (H := HF HccL y (ccFy y ccGy)).
set (f := pr1 (pr1 H)); set (Hf := pr2 (pr1 H)); set (HHf := pr2 H).
use unique_exists.
- apply (pr1 αinv L · f).
- simpl; apply (αinv_f_commutes y ccGy f Hf).
- abstract (intro; apply impred; intro; apply hsD).
- abstract (simpl in *; intros f' Hf'; apply (αinv_f_unique y ccGy f Hf); trivial;
            intro t; rewrite (HHf t); reflexivity).
Defined.

End preserves_colimit_iso.

Lemma is_cocont_iso : is_cocont F → is_cocont G.
Proof.
now intros H g d c cc; apply (preserves_colimit_iso).
Defined.

Lemma is_omega_cocont_iso : is_omega_cocont F → is_omega_cocont G.
Proof.
now intros H g d c cc; apply (preserves_colimit_iso).
Defined.

End cocont_iso.

Section functor_identity.

Context {C : precategory} (hsC : has_homsets C).

Lemma preserves_colimit_identity {g : graph} (d : diagram g C) (L : C)
  (cc : cocone d L) : preserves_colimit (functor_identity C) d L cc.
Proof.
intros HcL y ccy; simpl.
set (CC := mk_ColimCocone _ _ _ HcL).
use tpair.
- use tpair.
  + apply (colimArrow CC), ccy.
  + abstract (simpl; intro n; apply (colimArrowCommutes CC)).
- abstract (simpl; intro t; apply subtypeEquality;
    [ simpl; intro v; apply impred; intro; apply hsC
    | apply (colimArrowUnique CC); intro n; apply (pr2 t)]).
Defined.

Lemma is_cocont_functor_identity : is_cocont (functor_identity C).
Proof.
now intros g; apply preserves_colimit_identity.
Defined.

Lemma is_omega_cocont_functor_identity : is_omega_cocont (functor_identity C).
Proof.
now intros c; apply is_cocont_functor_identity.
Defined.

Definition omega_cocont_functor_identity : omega_cocont_functor C C :=
  tpair _ _ is_omega_cocont_functor_identity.

End functor_identity.

Section constant_functor.

Context {C D : precategory} (hsD : has_homsets D) (x : D).

Lemma preserves_colimit_constant_functor {g : graph} (v : vertex g)
  (conn : ∏ (u : vertex g), edge v u)
  (d : diagram g C) (L : C) (cc : cocone d L) :
  preserves_colimit (constant_functor C D x) d L cc.
Proof.
intros HcL y ccy; simpl.
use tpair.
- apply (tpair _ (coconeIn ccy v)).
  abstract (now intro u; generalize (coconeInCommutes ccy _ _ (conn u));
            rewrite !id_left; intro H; rewrite H).
- abstract (intro p; apply subtypeEquality;
              [ intro; apply impred; intro; apply hsD
              | now destruct p as [p H]; rewrite <- (H v), id_left ]).
Defined.

Lemma is_omega_cocont_constant_functor : is_omega_cocont (constant_functor C D x).
Proof.
intros c L ccL HccL y ccy.
use tpair.
- apply (tpair _ (coconeIn ccy 0)).
  abstract (intro n; rewrite id_left; destruct ccy as [f Hf]; simpl;
            now induction n as [|n IHn]; [apply idpath|]; rewrite IHn, <- (Hf n (S n) (idpath _)), id_left).
- abstract (intro p; apply subtypeEquality;
              [ intros f; apply impred; intro; apply hsD
              | now simpl; destruct p as [p H]; rewrite <- (H 0), id_left]).
Defined.

Definition omega_cocont_constant_functor : omega_cocont_functor C D :=
  tpair _ _ is_omega_cocont_constant_functor.

End constant_functor.

Section functor_composite.

Context {C D E : precategory} (hsE : has_homsets E).

Lemma preserves_colimit_functor_composite (F : functor C D) (G : functor D E)
  {g : graph} (d : diagram g C) (L : C) (cc : cocone d L)
  (H1 : preserves_colimit F d L cc)
  (H2 : preserves_colimit G (mapdiagram F d) (F L) (mapcocone F _ cc)) :
  preserves_colimit (functor_composite F G) d L cc.
Proof.
intros HcL y ccy; simpl.
set (CC := mk_ColimCocone _ _ _ (H2 (H1 HcL))).
use tpair.
- use tpair.
  + apply (colimArrow CC), ccy.
  + abstract (simpl; intro v; apply (colimArrowCommutes CC)).
- abstract (simpl; intro t; apply subtypeEquality;
    [ intros f; apply impred; intro; apply hsE
    | simpl; apply (colimArrowUnique CC), (pr2 t) ]).
Defined.

Lemma is_cocont_functor_composite (F : functor C D) (G : functor D E)
  (HF : is_cocont F) (HG : is_cocont G) : is_cocont (functor_composite F G).
Proof.
intros g d L cc.
apply preserves_colimit_functor_composite; [ apply HF | apply HG ].
Defined.

Lemma is_omega_cocont_functor_composite (F : functor C D) (G : functor D E) :
  is_omega_cocont F → is_omega_cocont G → is_omega_cocont (functor_composite F G).
Proof.
intros hF hG c L cc.
apply preserves_colimit_functor_composite; [ apply hF | apply hG ].
Defined.

Definition omega_cocont_functor_composite
  (F : omega_cocont_functor C D) (G : omega_cocont_functor D E) :
  omega_cocont_functor C E := tpair _ _ (is_omega_cocont_functor_composite _ _ (pr2 F) (pr2 G)).

End functor_composite.

Section iter_functor.

Lemma is_cocont_iter_functor {C : precategory} (hsC : has_homsets C)
  (F : functor C C) (hF : is_cocont F) n : is_cocont (iter_functor F n).
Proof.
induction n as [|n IH]; simpl.
- apply (is_cocont_functor_identity hsC).
- apply (is_cocont_functor_composite hsC _ _ IH hF).
Defined.

Lemma is_omega_cocont_iter_functor {C : precategory} (hsC : has_homsets C)
  (F : functor C C) (hF : is_omega_cocont F) n : is_omega_cocont (iter_functor F n).
Proof.
induction n as [|n IH]; simpl.
- apply (is_omega_cocont_functor_identity hsC).
- apply (is_omega_cocont_functor_composite hsC _ _ IH hF).
Defined.

Definition omega_cocont_iter_functor {C : precategory} (hsC : has_homsets C)
  (F : omega_cocont_functor C C) n : omega_cocont_functor C C :=
  tpair _ _ (is_omega_cocont_iter_functor hsC _ (pr2 F) n).

End iter_functor.

Section pair_functor.

Context {A B C D : precategory} (F : functor A C) (G : functor B D)
        (hsA : has_homsets A) (hsB : has_homsets B) (hsC : has_homsets C) (hsD : has_homsets D).

Local Definition cocone_pr1_functor {g : graph} (cAB : diagram g (precategory_binproduct A B))
  (ab : A × B) (ccab : cocone cAB ab) :
  cocone (mapdiagram (pr1_functor A B) cAB) (ob1 ab).
Proof.
use mk_cocone.
- simpl; intro n; apply (mor1 (coconeIn ccab n)).
- abstract (simpl; intros m n e; now rewrite <- (coconeInCommutes ccab m n e)).
Defined.

Local Lemma isColimCocone_pr1_functor {g : graph} (cAB : diagram g (precategory_binproduct A B))
  (ab : A × B) (ccab : cocone cAB ab) (Hccab : isColimCocone cAB ab ccab) :
   isColimCocone (mapdiagram (pr1_functor A B) cAB) (ob1 ab)
     (mapcocone (pr1_functor A B) cAB ccab).
Proof.
intros x ccx.
transparent assert (HHH : (cocone cAB (x,, ob2 ab))).
{ use mk_cocone.
  - simpl; intro n; split;
      [ apply (pr1 ccx n) | apply (# (pr2_functor A B) (pr1 ccab n)) ].
  - abstract(simpl; intros m n e; apply pathsdirprod;
               [ apply (pr2 ccx m n e) | apply (maponpaths dirprod_pr2 ((pr2 ccab) m n e)) ]).
}
destruct (Hccab _ HHH) as [[[x1 x2] p1] p2].
use tpair.
- apply (tpair _ x1).
  abstract (intro n; apply (maponpaths pr1 (p1 n))).
- intro t.
  transparent assert (X : (∑ x0, ∏ v, coconeIn ccab v · x0 =
                                 precatbinprodmor (pr1 ccx v) (pr2 (pr1 ccab v)))).
  { use tpair.
    - split; [ apply (pr1 t) | apply (identity _) ].
    - cbn. abstract (intro n; rewrite id_right; apply pathsdirprod;
                 [ apply (pr2 t) | apply idpath ]).
  }
  abstract (apply subtypeEquality; simpl;
            [ intro f; apply impred; intro; apply hsA
            | apply (maponpaths (λ x, pr1 (pr1 x)) (p2 X))]).
Defined.

Lemma is_cocont_pr1_functor : is_cocont (pr1_functor A B).
Proof.
now intros c L ccL M H; apply isColimCocone_pr1_functor.
Defined.

Local Definition cocone_pr2_functor {g : graph} (cAB : diagram g (precategory_binproduct A B))
  (ab : A × B) (ccab : cocone cAB ab) :
  cocone (mapdiagram (pr2_functor A B) cAB) (pr2 ab).
Proof.
use mk_cocone.
- simpl; intro n; apply (pr2 (coconeIn ccab n)).
- abstract (simpl; intros m n e; now rewrite <- (coconeInCommutes ccab m n e)).
Defined.

Local Lemma isColimCocone_pr2_functor {g : graph} (cAB : diagram g (precategory_binproduct A B))
  (ab : A × B) (ccab : cocone cAB ab) (Hccab : isColimCocone cAB ab ccab) :
   isColimCocone (mapdiagram (pr2_functor A B) cAB) (pr2 ab)
     (mapcocone (pr2_functor A B) cAB ccab).
Proof.
intros x ccx.
transparent assert (HHH : (cocone cAB (pr1 ab,, x))).
{ use mk_cocone.
  - simpl; intro n; split;
      [ apply (# (pr1_functor A B) (pr1 ccab n)) | apply (pr1 ccx n) ].
  - abstract (simpl; intros m n e; apply pathsdirprod;
                [ apply (maponpaths pr1 (pr2 ccab m n e)) | apply (pr2 ccx m n e) ]).
 }
destruct (Hccab _ HHH) as [[[x1 x2] p1] p2].
use tpair.
- apply (tpair _ x2).
  abstract (intro n; apply (maponpaths dirprod_pr2 (p1 n))).
- intro t.
  transparent assert (X : (∑ x0, ∏ v, coconeIn ccab v · x0 =
                                 precatbinprodmor (pr1 (pr1 ccab v)) (pr1 ccx v))).
  { use tpair.
    - split; [ apply (identity _) | apply (pr1 t) ].
    - cbn. abstract (intro n; rewrite id_right; apply pathsdirprod;
                 [ apply idpath | apply (pr2 t) ]).
  }
  abstract (apply subtypeEquality; simpl;
              [ intro f; apply impred; intro; apply hsB
              | apply (maponpaths (λ x, dirprod_pr2 (pr1 x)) (p2 X)) ]).
Defined.

Lemma is_cocont_pr2_functor : is_cocont (pr2_functor A B).
Proof.
now intros c L ccL M H; apply isColimCocone_pr2_functor.
Defined.

Lemma isColimCocone_pair_functor {gr : graph}
  (HF : ∏ (d : diagram gr A) (c : A) (cc : cocone d c) (h : isColimCocone d c cc),
        isColimCocone _ _ (mapcocone F d cc))
  (HG : ∏ (d : diagram gr B) (c : B) (cc : cocone d c) (h : isColimCocone d c cc),
        isColimCocone _ _ (mapcocone G d cc)) :
  ∏ (d : diagram gr (precategory_binproduct A B)) (cd : A × B) (cc : cocone d cd),
  isColimCocone _ _ cc →
  isColimCocone _ _ (mapcocone (pair_functor F G) d cc).
Proof.
intros cAB ml ccml Hccml xy ccxy.
transparent assert (cFAX : (cocone (mapdiagram F (mapdiagram (pr1_functor A B) cAB)) (pr1 xy))).
{ use mk_cocone.
  - intro n; apply (pr1 (pr1 ccxy n)).
  - abstract (intros m n e; apply (maponpaths dirprod_pr1 (pr2 ccxy m n e))).
}
transparent assert (cGBY : (cocone (mapdiagram G (mapdiagram (pr2_functor A B) cAB)) (pr2 xy))).
{ use mk_cocone.
  - intro n; apply (pr2 (pr1 ccxy n)).
  - abstract (intros m n e; apply (maponpaths dirprod_pr2 (pr2 ccxy m n e))).
}
destruct (HF _ _ _ (isColimCocone_pr1_functor cAB ml ccml Hccml) _ cFAX) as [[f hf1] hf2].
destruct (HG _ _ _ (isColimCocone_pr2_functor cAB ml ccml Hccml) _ cGBY) as [[g hg1] hg2].
simpl in ×.
use tpair.
- apply (tpair _ (f,,g)).
  abstract (intro n; unfold precatbinprodmor, compose; simpl;
            now rewrite hf1, hg1).
- abstract (intro t; apply subtypeEquality; simpl;
             [ intro x; apply impred; intro; apply isaset_dirprod; [ apply hsC | apply hsD ]
             | induction t as [[f1 f2] p]; simpl in *; apply pathsdirprod;
               [ apply (maponpaths pr1 (hf2 (f1,, (λ n, maponpaths pr1 (p n)))))
               | apply (maponpaths pr1 (hg2 (f2,, (λ n, maponpaths dirprod_pr2 (p n)))))]]).
Defined.

Lemma is_cocont_pair_functor (HF : is_cocont F) (HG : is_cocont G) :
  is_cocont (pair_functor F G).
Proof.
intros gr cAB ml ccml Hccml.
now apply isColimCocone_pair_functor; [apply HF|apply HG|].
Defined.

Lemma is_omega_cocont_pair_functor (HF : is_omega_cocont F) (HG : is_omega_cocont G) :
  is_omega_cocont (pair_functor F G).
Proof.
now intros cAB ml ccml Hccml; apply isColimCocone_pair_functor.
Defined.

End pair_functor.

Section functor_into_product_precategory.

Context {I : UU} {A : precategory} (hsA : has_homsets A)
  {B : I → precategory} (hsB : ∀ i, has_homsets (B i)).

Lemma isColimCocone_in_product_precategory
  {g : graph} (c : diagram g (product_precategory B))
  (b : product_precategory B) (cc : cocone c b)
  (M : ∏ i, isColimCocone _ _ (mapcocone (pr_functor I B i) _ cc))
  : isColimCocone c b cc.
Proof.
  intros b' cc'.
  apply iscontraprop1.
  - abstract (
    apply invproofirrelevance; intros f1 f2;
    apply subtypeEquality;
    [ intros f; apply impred_isaprop; intros v;
      apply has_homsets_product_precategory, hsB | ];
    apply funextsec; intros i;
    assert (MM := M i _ (mapcocone (pr_functor I B i) _ cc'));
    assert (H := proofirrelevance _ (isapropifcontr MM));
    use (maponpaths pr1 (H (pr1 f1 i,,_) (pr1 f2 i,,_)));
      clear MM H; intros v ;
      [ exact (toforallpaths _ _ _ (pr2 f1 v) i) |
        exact (toforallpaths _ _ _ (pr2 f2 v) i) ]
      ) .
  - use tpair.
    + intros i.
      use (pr1 (pr1 (M i _ (mapcocone (pr_functor I B i) _ cc')))).
    + abstract (
          intros v; apply funextsec; intros i;
          use (pr2 (pr1 (M i _ (mapcocone (pr_functor I B i) _ cc'))) v)
        ).
Defined.

Lemma is_cocont_functor_into_product_precategory
  {F : functor A (product_precategory B)}
  (HF : ∏ (i : I), is_cocont (functor_composite F (pr_functor I B i))) :
  is_cocont F.
Proof.
  intros gr cA a cc Hcc.
  apply isColimCocone_in_product_precategory.
  intros i.
  rewrite <- mapcocone_functor_composite; try apply hsB.
  now apply HF, Hcc.
Defined.

Lemma is_omega_cocont_functor_into_product_precategory
  {F : functor A (product_precategory B)}
  (HF : ∏ (i : I), is_omega_cocont (functor_composite F (pr_functor I B i))) :
  is_omega_cocont F.
Proof.
  intros cA a cc Hcc.
  apply isColimCocone_in_product_precategory.
  intros i.
  rewrite <- mapcocone_functor_composite; try apply hsB.
  now apply HF, Hcc.
Defined.

End functor_into_product_precategory.

Section tuple_functor.

Context {I : UU} {A : precategory} {B : I → precategory} (hsB : ∏ i, has_homsets (B i)).

Lemma is_cocont_tuple_functor {F : ∏ i, functor A (B i)}
  (HF : ∏ i, is_cocont (F i)) : is_cocont (tuple_functor F).
Proof.
  apply is_cocont_functor_into_product_precategory; try apply hsB.
  intro i; rewrite (pr_tuple_functor hsB); apply HF.
Defined.

Lemma is_omega_cocont_tuple_functor {F : ∏ i, functor A (B i)}
  (HF : ∏ i, is_omega_cocont (F i)) : is_omega_cocont (tuple_functor F).
Proof.
  apply is_omega_cocont_functor_into_product_precategory; try apply hsB.
  intro i; rewrite (pr_tuple_functor hsB); apply HF.
Defined.

End tuple_functor.

Section family_functor.

Context {I : UU} {A B : precategory} (hsA : has_homsets A) (hsB : has_homsets B).

Hypothesis (HI : isdeceq I).

Local Definition ifI (i j : I) (a b : A) : A :=
  coprod_rect (λ _, A) (λ _,a) (λ _,b) (HI i j).

Local Lemma ifI_eq i x y : ifI i i x y = x.
Proof.
now unfold ifI; destruct (HI i i) as [p|p]; [|destruct (p (idpath _))].
Defined.

Local Lemma isColimCocone_pr_functor
  {g : graph} (c : diagram g (power_precategory I A))
  (L : power_precategory I A) (ccL : cocone c L)
  (M : isColimCocone c L ccL) : ∏ i,
  isColimCocone _ _ (mapcocone (pr_functor I (λ _, A) i) c ccL).
Proof.
intros i x ccx; simpl in ×.
transparent assert (HHH : (cocone c (λ j, ifI i j x (L j)))).
{ unfold ifI.
  use mk_cocone.
  - simpl; intros n j.
    destruct (HI i j) as [p|p].
    + apply (transportf (λ i, A ⟦ dob c n i, x ⟧) p (coconeIn ccx n)).
    + apply (# (pr_functor I (λ _, A) j) (coconeIn ccL n)).
  - abstract (simpl; intros m n e;
      apply funextsec; intro j; unfold compose; simpl;
      destruct (HI i j);
        [ destruct p; apply (pr2 ccx m n e)
        | apply (toforallpaths _ _ _ (pr2 ccL m n e) j)]).
}
destruct (M _ HHH) as [[x1 p1] p2].
use tpair.
- apply (tpair _ (transportf _ (ifI_eq _ _ _) (x1 i))).
  abstract (intro n;
    rewrite <- idtoiso_postcompose, assoc;
    eapply pathscomp0;
      [eapply cancel_postcomposition, (toforallpaths _ _ _ (p1 n) i)|];
    unfold ifI, ifI_eq; simpl;
    destruct (HI i i); [|destruct (n0 (idpath _))];
    rewrite idtoiso_postcompose, idpath_transportf;
    assert (hp : p = idpath i); [apply (isasetifdeceq _ HI)|];
    now rewrite hp, idpath_transportf).
- intro t.
  transparent assert (X : (∑ x0, ∏ n, coconeIn ccL n · x0 = coconeIn HHH n)).
  { use tpair.
    - simpl; intro j; unfold ifI.
      destruct (HI i j).
      + apply (transportf (λ i, A ⟦ L i, x ⟧) p (pr1 t)).
      + apply identity.
    - cbn. abstract (intro n; apply funextsec; intro j; unfold ifI; destruct (HI i j);
          [ now destruct p; rewrite <- (pr2 t), !idpath_transportf
          | apply id_right ]).
  }
  apply subtypeEquality; simpl; [intro f; apply impred; intro; apply hsA|].
  set (H := toforallpaths _ _ _ (maponpaths pr1 (p2 X)) i); simpl in H.
  rewrite <- H; clear H; unfold ifI_eq, ifI.
  destruct (HI i i) as [p|p]; [|destruct (p (idpath _))].
  assert (hp : p = idpath i); [apply (isasetifdeceq _ HI)|].
  now rewrite hp, idpath_transportf.
Defined.

Lemma is_cocont_pr_functor (i : I) : is_cocont (pr_functor I (λ _, A) i).
Proof.
now intros c L ccL M H; apply isColimCocone_pr_functor.
Defined.

Lemma isColimCocone_family_functor {gr : graph} (F : ∏ (i : I), functor A B)
  (HF : ∏ i (d : diagram gr A) (c : A) (cc : cocone d c) (h : isColimCocone d c cc),
        isColimCocone _ _ (mapcocone (F i) d cc)) :
  ∏ (d : diagram gr (product_precategory (λ _, A))) (cd : I → A) (cc : cocone d cd),
  isColimCocone _ _ cc →
  isColimCocone _ _ (mapcocone (family_functor I F) d cc).
Proof.
intros cAB ml ccml Hccml xy ccxy; simpl in ×.
transparent assert (cc : (∏ i, cocone (mapdiagram (F i) (mapdiagram (pr_functor I (λ _ : I, A) i) cAB)) (xy i))).
{ intro i; use mk_cocone.
  - intro n; use (pr1 ccxy n).
  - abstract (intros m n e; apply (toforallpaths _ _ _ (pr2 ccxy m n e) i)).
}
set (X i := HF i _ _ _ (isColimCocone_pr_functor _ _ _ Hccml i) (xy i) (cc i)).
use tpair.
- use tpair.
  + intro i; apply (pr1 (pr1 (X i))).
  + abstract (intro n; apply funextsec; intro j; apply (pr2 (pr1 (X j)) n)).
- abstract (intro t; apply subtypeEquality; simpl;
             [ intro x; apply impred; intro; apply impred_isaset; intro i; apply hsB
             | destruct t as [f1 f2]; simpl in *; apply funextsec; intro i;
               transparent assert (H : (∑ x : B ⟦ (F i) (ml i), xy i ⟧,
                                       ∏ n, # (F i) (coconeIn ccml n i) · x =
                                       coconeIn ccxy n i));
                [apply (tpair _ (f1 i)); intro n; apply (toforallpaths _ _ _ (f2 n) i)|];
               apply (maponpaths pr1 (pr2 (X i) H))]).
Defined.

Lemma is_cocont_family_functor
  {F : ∏ (i : I), functor A B} (HF : ∏ (i : I), is_cocont (F i)) :
  is_cocont (family_functor I F).
Proof.
intros gr cAB ml ccml Hccml.
apply isColimCocone_family_functor; trivial; intro i; apply HF.
Defined.

Lemma is_omega_cocont_family_functor
  {F : ∏ (i : I), functor A B} (HF : ∏ (i : I), is_omega_cocont (F i)) :
  is_omega_cocont (family_functor I F).
Proof.
now intros cAB ml ccml Hccml; apply isColimCocone_family_functor.
Defined.

End family_functor.

Section bindelta_functor.

Context {C : precategory} (PC : BinProducts C) (hsC : has_homsets C).

Lemma is_cocont_bindelta_functor : is_cocont (bindelta_functor C).
Proof.
apply (left_adjoint_cocont _ (is_left_adjoint_bindelta_functor PC) hsC).
abstract (apply (has_homsets_precategory_binproduct _ _ hsC hsC)).
Defined.

Lemma is_omega_cocont_bindelta_functor : is_omega_cocont (bindelta_functor C).
Proof.
now intros c L ccL; apply is_cocont_bindelta_functor.
Defined.

End bindelta_functor.

Section delta_functor.

Context {I : UU} {C : precategory} (PC : Products I C) (hsC : has_homsets C).

Lemma is_cocont_delta_functor : is_cocont (delta_functor I C).
Proof.
apply (left_adjoint_cocont _ (is_left_adjoint_delta_functor _ PC) hsC).
abstract (apply (has_homsets_power_precategory _ _ hsC)).
Defined.

Lemma is_omega_cocont_delta_functor :
  is_omega_cocont (delta_functor I C).
Proof.
now intros c L ccL; apply is_cocont_delta_functor.
Defined.

End delta_functor.

Section bincoprod_functor.

Context {C : precategory} (PC : BinCoproducts C) (hsC : has_homsets C).

Lemma is_cocont_bincoproduct_functor : is_cocont (bincoproduct_functor PC).
Proof.
apply (left_adjoint_cocont _ (is_left_adjoint_bincoproduct_functor PC)).
- abstract (apply has_homsets_precategory_binproduct; apply hsC).
- abstract (apply hsC).
Defined.

Lemma is_omega_cocont_bincoproduct_functor :
  is_omega_cocont (bincoproduct_functor PC).
Proof.
now intros c L ccL; apply is_cocont_bincoproduct_functor.
Defined.

End bincoprod_functor.

Section coprod_functor.

Context {I : UU} {C : precategory} (PC : Coproducts I C) (hsC : has_homsets C).

Lemma is_cocont_coproduct_functor :
  is_cocont (coproduct_functor _ PC).
Proof.
apply (left_adjoint_cocont _ (is_left_adjoint_coproduct_functor _ PC)).
- abstract (apply has_homsets_power_precategory; apply hsC).
- abstract (apply hsC).
Defined.

Lemma is_omega_cocont_coproduct_functor :
  is_omega_cocont (coproduct_functor _ PC).
Proof.
now intros c L ccL; apply is_cocont_coproduct_functor.
Defined.

End coprod_functor.

Section BinCoproduct_of_functors.

Context {C D : precategory} (HD : BinCoproducts D) (hsD : has_homsets D).

Lemma is_cocont_BinCoproduct_of_functors_alt {F G : functor C D}
  (HF : is_cocont F) (HG : is_cocont G) :
  is_cocont (BinCoproduct_of_functors_alt hsD HD F G).
Proof.
apply (is_cocont_functor_composite hsD).
- apply is_cocont_tuple_functor; [intros b; apply hsD|].
  induction i; assumption.
- apply is_cocont_coproduct_functor, hsD.
Defined.

Lemma is_omega_cocont_BinCoproduct_of_functors_alt {F G : functor C D}
  (HF : is_omega_cocont F) (HG : is_omega_cocont G) :
  is_omega_cocont (BinCoproduct_of_functors_alt hsD HD F G).
Proof.
apply (is_omega_cocont_functor_composite hsD).
- apply is_omega_cocont_tuple_functor; [intros b; apply hsD|].
  induction i; assumption.
- apply is_omega_cocont_coproduct_functor, hsD.
Defined.

Definition omega_cocont_BinCoproduct_of_functors_alt (F G : omega_cocont_functor C D) :
  omega_cocont_functor C D :=
    tpair _ _ (is_omega_cocont_BinCoproduct_of_functors_alt (pr2 F) (pr2 G)).

Lemma is_cocont_BinCoproduct_of_functors (F G : functor C D)
  (HF : is_cocont F) (HG : is_cocont G) :
  is_cocont (BinCoproduct_of_functors _ _ HD F G).
Proof.
exact (transportf _
         (BinCoproduct_of_functors_alt_eq_BinCoproduct_of_functors _ _ _ _ F G)
         (is_cocont_BinCoproduct_of_functors_alt HF HG)).
Defined.

Lemma is_omega_cocont_BinCoproduct_of_functors (F G : functor C D)
  (HF : is_omega_cocont F) (HG : is_omega_cocont G) :
  is_omega_cocont (BinCoproduct_of_functors _ _ HD F G).
Proof.
exact (transportf _
         (BinCoproduct_of_functors_alt_eq_BinCoproduct_of_functors _ _ _ _ F G)
         (is_omega_cocont_BinCoproduct_of_functors_alt HF HG)).
Defined.

Definition omega_cocont_BinCoproduct_of_functors
 (F G : omega_cocont_functor C D) :
  omega_cocont_functor C D :=
    tpair _ _ (is_omega_cocont_BinCoproduct_of_functors _ _ (pr2 F) (pr2 G)).

Lemma is_cocont_BinCoproduct_of_functors_alt2 {hsC : has_homsets C}
  (PC : BinProducts C) (F G : functor C D)
  (HF : is_cocont F) (HG : is_cocont G) :
  is_cocont (BinCoproduct_of_functors_alt2 HD F G).
Proof.
apply (is_cocont_functor_composite hsD).
  apply (is_cocont_bindelta_functor PC hsC).
apply (is_cocont_functor_composite hsD).
  apply (is_cocont_pair_functor _ _ hsC hsC hsD hsD HF HG).
apply (is_cocont_bincoproduct_functor _ hsD).
Defined.

Lemma is_omega_cocont_BinCoproduct_of_functors_alt2 (hsC : has_homsets C)
  (PC : BinProducts C) (F G : functor C D)
  (HF : is_omega_cocont F) (HG : is_omega_cocont G) :
  is_omega_cocont (BinCoproduct_of_functors_alt2 HD F G).
Proof.
apply (is_omega_cocont_functor_composite hsD).
  apply (is_omega_cocont_bindelta_functor PC hsC).
apply (is_omega_cocont_functor_composite hsD).
  apply (is_omega_cocont_pair_functor _ _ hsC hsC hsD hsD HF HG).
apply (is_omega_cocont_bincoproduct_functor _ hsD).
Defined.

Definition omega_cocont_BinCoproduct_of_functors_alt2 (hsC : has_homsets C)
  (PC : BinProducts C) (F G : omega_cocont_functor C D) :
  omega_cocont_functor C D :=
    tpair _ _ (is_omega_cocont_BinCoproduct_of_functors_alt2 hsC PC _ _ (pr2 F) (pr2 G)).

End BinCoproduct_of_functors.

Section coproduct_of_functors.

Context {I : UU} {C D : precategory} (HD : Coproducts I D) (hsD : has_homsets D).

Lemma is_cocont_coproduct_of_functors
  {F : ∏ (i : I), functor C D} (HF : ∏ i, is_cocont (F i)) :
  is_cocont (coproduct_of_functors I _ _ HD F).
Proof.
  use (transportf _
        (coproduct_of_functors_alt_eq_coproduct_of_functors _ _ _ _ hsD F)
        _).
  apply is_cocont_functor_composite; try apply hsD.
  - apply is_cocont_tuple_functor; try (intro; apply hsD).
    apply HF.
  - apply is_cocont_coproduct_functor; try apply hsD.
Defined.

Lemma is_omega_cocont_coproduct_of_functors
  {F : ∏ (i : I), functor C D} (HF : ∏ i, is_omega_cocont (F i)) :
  is_omega_cocont (coproduct_of_functors I _ _ HD F).
Proof.
  use (transportf _
        (coproduct_of_functors_alt_eq_coproduct_of_functors _ _ _ _ hsD F)
        _).
  apply is_omega_cocont_functor_composite; try apply hsD.
  - apply is_omega_cocont_tuple_functor; try (intro; apply hsD).
    apply HF.
  - apply is_omega_cocont_coproduct_functor; try apply hsD.
Defined.

Definition omega_cocont_coproduct_of_functors
  (F : ∏ i, omega_cocont_functor C D) :
  omega_cocont_functor C D :=
    tpair _ _ (is_omega_cocont_coproduct_of_functors (λ i, pr2 (F i))).

End coproduct_of_functors.

Section constprod_functors.

Context {C : precategory} (PC : BinProducts C) (hsC : has_homsets C) (hE : Exponentials PC).

Lemma is_cocont_constprod_functor1 (x : C) : is_cocont (constprod_functor1 PC x).
Proof.
exact (left_adjoint_cocont _ (hE _) hsC hsC).
Defined.

Lemma is_omega_cocont_constprod_functor1 (x : C) : is_omega_cocont (constprod_functor1 PC x).
Proof.
now intros c L ccL; apply is_cocont_constprod_functor1.
Defined.

Definition omega_cocont_constprod_functor1 (x : C) :
  omega_cocont_functor C C := tpair _ _ (is_omega_cocont_constprod_functor1 x).

Lemma is_cocont_constprod_functor2 (x : C) : is_cocont (constprod_functor2 PC x).
Proof.
apply left_adjoint_cocont; try apply hsC.
apply (is_left_adjoint_constprod_functor2 PC hsC), hE.
Defined.

Lemma is_omega_cocont_constprod_functor2 (x : C) : is_omega_cocont (constprod_functor2 PC x).
Proof.
now intros c L ccL; apply is_cocont_constprod_functor2.
Defined.

Definition omega_cocont_constprod_functor2 (x : C) :
  omega_cocont_functor C C := tpair _ _ (is_omega_cocont_constprod_functor2 x).

End constprod_functors.

Section binprod_functor.

Context {C : precategory} (PC : BinProducts C) (hsC : has_homsets C).

Variable omega_cocont_constprod_functor1 :
  ∏ x : C, is_omega_cocont (constprod_functor1 PC x).

Let omega_cocont_constprod_functor2 :
  ∏ x : C, is_omega_cocont (constprod_functor2 PC x).
Proof.
now intro x; apply (is_omega_cocont_iso hsC (flip_iso PC hsC x)).
Defined.

Local Definition fun_lt (cAB : chain (precategory_binproduct C C)) :
  ∏ i j, i < j →
              C ⟦ BinProductObject C (PC (ob1 (dob cAB i)) (ob2 (dob cAB j))),
                  BinProductObject C (PC (ob1 (dob cAB j)) (ob2 (dob cAB j))) ⟧.
Proof.
intros i j hij.
apply (BinProductOfArrows _ _ _ (mor1 (chain_mor cAB hij)) (identity _)).
Defined.

Local Definition fun_gt (cAB : chain (precategory_binproduct C C)) :
  ∏ i j, i > j →
              C ⟦ BinProductObject C (PC (ob1 (dob cAB i)) (ob2 (dob cAB j))),
                  BinProductObject C (PC (ob1 (dob cAB i)) (ob2 (dob cAB i))) ⟧.
Proof.
intros i j hij.
apply (BinProductOfArrows _ _ _ (identity _) (mor2 (chain_mor cAB hij))).
Defined.

Local Definition map_to_K (cAB : chain (precategory_binproduct C C)) (K : C)
  (ccK : cocone (mapchain (binproduct_functor PC) cAB) K) i j :
  C⟦BinProductObject C (PC (ob1 (dob cAB i)) (ob2 (dob cAB j))), K⟧.
Proof.
destruct (natlthorgeh i j).
- apply (fun_lt cAB _ _ h · coconeIn ccK j).
- destruct (natgehchoice _ _ h) as [H|H].
  × apply (fun_gt cAB _ _ H · coconeIn ccK i).
  × destruct H; apply (coconeIn ccK i).
Defined.

Local Lemma map_to_K_commutes (cAB : chain (precategory_binproduct C C)) (K : C)
  (ccK : cocone (mapchain (binproduct_functor PC) cAB) K)
  i j k (e : edge j k) :
   BinProduct_of_functors_mor C C PC (constant_functor C C (pr1 (pr1 cAB i)))
     (functor_identity C) (pr2 (dob cAB j)) (pr2 (dob cAB k))
     (mor2 (dmor cAB e)) · map_to_K cAB K ccK i k =
   map_to_K cAB K ccK i j.
Proof.
destruct e; simpl.
unfold BinProduct_of_functors_mor, map_to_K.
destruct (natlthorgeh i j) as [h|h].
- destruct (natlthorgeh i (S j)) as [h0|h0].
  × rewrite assoc, <- (coconeInCommutes ccK j (S j) (idpath _)), assoc; simpl.
    apply cancel_postcomposition; unfold fun_lt.
    rewrite BinProductOfArrows_comp, id_left.
    eapply pathscomp0; [apply BinProductOfArrows_comp|].
    rewrite id_right.
    apply BinProductOfArrows_eq; trivial; rewrite id_left; simpl.
    destruct (natlehchoice4 i j h0) as [h1|h1].
    + apply cancel_postcomposition, maponpaths, maponpaths, isasetbool.
    + destruct h1; destruct (isirreflnatlth _ h).
  × destruct (isirreflnatlth _ (natlthlehtrans _ _ _ (natlthtolths _ _ h) h0)).
- destruct (natlthorgeh i (S j)) as [h0|h0].
  × destruct (natgehchoice i j h) as [h1|h1].
    + destruct (natlthchoice2 _ _ h1) as [h2|h2].
      { destruct (isirreflnatlth _ (istransnatlth _ _ _ h0 h2)). }
      { destruct h2; destruct (isirreflnatlth _ h0). }
    + destruct h1; simpl.
      rewrite <- (coconeInCommutes ccK i (S i) (idpath _)), assoc.
      eapply pathscomp0; [apply cancel_postcomposition, BinProductOfArrows_comp|].
      rewrite id_left, id_right.
      apply cancel_postcomposition, BinProductOfArrows_eq; trivial.
      simpl; destruct (natlehchoice4 i i h0) as [h1|h1]; [destruct (isirreflnatlth _ h1)|].
      apply maponpaths, maponpaths, isasetnat.
  × destruct (natgehchoice i j h) as [h1|h1].
    + destruct (natgehchoice i (S j) h0) as [h2|h2].
      { unfold fun_gt; rewrite assoc.
        eapply pathscomp0; [eapply cancel_postcomposition, BinProductOfArrows_comp|].
        rewrite id_right.
        apply cancel_postcomposition, BinProductOfArrows_eq; trivial.
        now rewrite <- (chain_mor_right h1 h2). }
      { destruct h; unfold fun_gt; simpl.
        generalize h1; clear h1.
        rewrite h2; intro h1.
        apply cancel_postcomposition.
        apply BinProductOfArrows_eq; trivial; simpl.
        destruct (natlehchoice4 j j h1); [destruct (isirreflnatlth _ h)|].
        apply maponpaths, maponpaths, isasetnat. }
    + destruct h1; destruct (negnatgehnsn _ h0).
Qed.

Local Definition ccAiB_K (cAB : chain (precategory_binproduct C C)) (K : C)
  (ccK : cocone (mapchain (binproduct_functor PC) cAB) K) i :
  cocone (mapchain (constprod_functor1 PC (pr1 (pr1 cAB i)))
         (mapchain (pr2_functor C C) cAB)) K.
Proof.
use mk_cocone.
+ intro j; apply (map_to_K cAB K ccK i j).
+ simpl; intros j k e; apply map_to_K_commutes.
Defined.

Section omega_cocont_binproduct.

Context {cAB : chain (precategory_binproduct C C)} {LM : C × C}
        {ccLM : cocone cAB LM} (HccLM : isColimCocone cAB LM ccLM)
        {K : C} (ccK : cocone (mapchain (binproduct_functor PC) cAB) K).

Let L := pr1 LM : C.
Let M := pr2 LM : (λ _ : C, C) (pr1 LM).
Let cA := mapchain (pr1_functor C C) cAB : chain C.
Let cB := mapchain (pr2_functor C C) cAB : chain C.
Let HA := isColimCocone_pr1_functor hsC _ _ _ HccLM
  : isColimCocone cA L (cocone_pr1_functor cAB LM ccLM).
Let HB := isColimCocone_pr2_functor hsC _ _ _ HccLM
  : isColimCocone cB M (cocone_pr2_functor cAB LM ccLM).

Let HAiB := λ i, omega_cocont_constprod_functor1 (pr1 (pr1 cAB i)) _ _ _ HB.

Let CCAiB := λ i, mk_ColimCocone _ _ _ (HAiB i).

Let HAiM := mk_ColimCocone _ _ _ (omega_cocont_constprod_functor2 M _ _ _ HA).

Let ccAiB_K := λ i, ccAiB_K _ _ ccK i.

Local Definition f i j : C
   ⟦ BinProduct_of_functors_ob C C PC (constant_functor C C (pr1 (dob cAB i)))
       (functor_identity C) (pr2 (dob cAB j)),
     BinProduct_of_functors_ob C C PC (constant_functor C C (pr1 (dob cAB (S i))))
       (functor_identity C) (pr2 (dob cAB j)) ⟧.
Proof.
  apply BinProductOfArrows; [apply (dmor cAB (idpath _)) | apply identity ].
Defined.

Local Lemma fNat : ∏ i u v (e : edge u v),
   dmor (mapchain (constprod_functor1 PC _) cB) e · f i v =
   f i u · dmor (mapchain (constprod_functor1 PC _) cB) e.
Proof.
  intros i j k e; destruct e; simpl.
  eapply pathscomp0; [apply BinProductOfArrows_comp|].
  eapply pathscomp0; [|eapply pathsinv0; apply BinProductOfArrows_comp].
  now rewrite !id_left, !id_right.
Qed.

Local Definition AiM_chain : chain C.
Proof.
  use tpair.
  - intro i; apply (colim (CCAiB i)).
  - intros i j e; destruct e.
    apply (colimOfArrows (CCAiB i) (CCAiB (S i)) (f i) (fNat i)).
Defined.

Local Lemma AiM_chain_eq : ∏ i, dmor AiM_chain (idpath (S i)) =
                       dmor (mapchain (constprod_functor2 PC M) cA) (idpath _).
Proof.
  intro i; simpl; unfold colimOfArrows, BinProduct_of_functors_mor; simpl.
  apply pathsinv0, colimArrowUnique.
  simpl; intro j.
  unfold colimIn; simpl; unfold BinProduct_of_functors_mor, f; simpl.
  eapply pathscomp0; [apply BinProductOfArrows_comp|].
  apply pathsinv0.
  eapply pathscomp0; [apply BinProductOfArrows_comp|].
  now rewrite !id_left, !id_right.
Qed.

Local Lemma ccAiM_K_subproof : ∏ u v (e : edge u v),
   dmor (mapdiagram (constprod_functor2 PC M) cA) e ·
   colimArrow (CCAiB v) K (ccAiB_K v) = colimArrow (CCAiB u) K (ccAiB_K u).
Proof.
  intros i j e; destruct e; simpl.
  generalize (AiM_chain_eq i); simpl; intro H; rewrite <- H; clear H; simpl.
  eapply pathscomp0.
  apply (precompWithColimOfArrows _ _ (CCAiB i) (CCAiB (S i)) _ _ K (ccAiB_K (S i))).
  apply (colimArrowUnique (CCAiB i) K (ccAiB_K i)).
  simpl; intros j.
  eapply pathscomp0; [apply (colimArrowCommutes (CCAiB i) K)|]; simpl.
  unfold map_to_K.
  destruct (natlthorgeh (S i) j).
  + destruct (natlthorgeh i j).
    × rewrite assoc; apply cancel_postcomposition.
      unfold f, fun_lt; simpl.
      eapply pathscomp0; [apply BinProductOfArrows_comp|].
      now rewrite id_right, <- (chain_mor_right h0 h).
    × destruct (isasymmnatgth _ _ h h0).
  + destruct (natgehchoice (S i) j h).
    × destruct h.
      { destruct (natlthorgeh i j).
        - destruct (natlthchoice2 _ _ h) as [h2|h2].
          + destruct (isirreflnatlth _ (istransnatlth _ _ _ h0 h2)).
          + destruct h2; destruct (isirreflnatlth _ h0).
        - destruct (natgehchoice i j h).
          + destruct h.
            rewrite <- (coconeInCommutes ccK i _ (idpath _)); simpl.
            rewrite !assoc; apply cancel_postcomposition.
            unfold f, fun_gt.
            rewrite BinProductOfArrows_comp.
            eapply pathscomp0; [apply BinProductOfArrows_comp|].
            now rewrite !id_left, !id_right, <- (chain_mor_left h1 h0).
          + destruct p.
            rewrite <- (coconeInCommutes ccK i _ (idpath _)), assoc.
            apply cancel_postcomposition.
            unfold f, fun_gt.
            eapply pathscomp0; [apply BinProductOfArrows_comp|].
            rewrite id_left, id_right.
            apply BinProductOfArrows_eq; trivial; simpl.
            destruct (natlehchoice4 i i h0); [destruct (isirreflnatlth _ h1)|].
            apply maponpaths, maponpaths, isasetnat.
       }
    × destruct p, h.
      destruct (natlthorgeh i (S i)); [|destruct (negnatgehnsn _ h)].
      apply cancel_postcomposition; unfold f, fun_lt.
      apply BinProductOfArrows_eq; trivial; simpl.
      destruct (natlehchoice4 i i h); [destruct (isirreflnatlth _ h0)|].
      assert (H : idpath (S i) = maponpaths S p). apply isasetnat.
      now rewrite H.
Qed.

Local Definition ccAiM_K := mk_cocone _ ccAiM_K_subproof.

Local Lemma is_cocone_morphism :
 ∏ v : nat,
   BinProductOfArrows C (PC L M) (PC (pr1 (dob cAB v)) (pr2 (dob cAB v)))
     (pr1 (coconeIn ccLM v)) (pr2 (coconeIn ccLM v)) ·
   colimArrow HAiM K ccAiM_K = coconeIn ccK v.
Proof.
  intro i.
  generalize (colimArrowCommutes HAiM K ccAiM_K i).
  assert (H : coconeIn ccAiM_K i = colimArrow (CCAiB i) K (ccAiB_K i)).
  { apply idpath. }
  rewrite H; intros HH.
  generalize (colimArrowCommutes (CCAiB i) K (ccAiB_K i) i).
  rewrite <- HH; simpl; unfold map_to_K.
  destruct (natlthorgeh i i); [destruct (isirreflnatlth _ h)|].
  destruct (natgehchoice i i h); [destruct (isirreflnatgth _ h0)|].
  simpl; destruct h, p.
  intros HHH.
  rewrite <- HHH, assoc.
  apply cancel_postcomposition.
  unfold colimIn; simpl; unfold BinProduct_of_functors_mor; simpl.
  apply pathsinv0.
  eapply pathscomp0; [apply BinProductOfArrows_comp|].
  now rewrite id_left, id_right.
Qed.

Local Lemma is_unique_cocone_morphism :
 ∏ t : ∑ x : C ⟦ BinProductObject C (PC L M), K ⟧,
       ∏ v : nat,
       BinProductOfArrows C (PC L M) (PC (pr1 (dob cAB v)) (pr2 (dob cAB v)))
         (pr1 (coconeIn ccLM v)) (pr2 (coconeIn ccLM v)) · x =
       coconeIn ccK v, t = colimArrow HAiM K ccAiM_K,, is_cocone_morphism.
Proof.
  intro t.
  apply subtypeEquality; simpl.
  + intro; apply impred; intros; apply hsC.
  + apply (colimArrowUnique HAiM K ccAiM_K).
    induction t as [t p]; simpl; intro i.
    apply (colimArrowUnique (CCAiB i) K (ccAiB_K i)).
    simpl; intros j; unfold map_to_K.
    induction (natlthorgeh i j) as [h|h].
    × rewrite <- (p j); unfold fun_lt.
      rewrite !assoc.
      apply cancel_postcomposition.
      unfold colimIn; simpl; unfold BinProduct_of_functors_mor; simpl.
      eapply pathscomp0; [apply BinProductOfArrows_comp|].
      apply pathsinv0.
      eapply pathscomp0; [apply BinProductOfArrows_comp|].
      rewrite !id_left, id_right.
      apply BinProductOfArrows_eq; trivial.
      apply (maponpaths pr1 (chain_mor_coconeIn cAB LM ccLM i j h)).
    × destruct (natgehchoice i j h).
      { unfold fun_gt; rewrite <- (p i), !assoc.
        apply cancel_postcomposition.
        unfold colimIn; simpl; unfold BinProduct_of_functors_mor; simpl.
        eapply pathscomp0; [apply BinProductOfArrows_comp|].
        apply pathsinv0.
        eapply pathscomp0; [apply BinProductOfArrows_comp|].
        now rewrite !id_left, id_right, <- (chain_mor_coconeIn cAB LM ccLM _ _ h0). }
      { destruct p0.
        rewrite <- (p i), assoc.
        apply cancel_postcomposition.
        unfold colimIn; simpl; unfold BinProduct_of_functors_mor; simpl.
        eapply pathscomp0; [apply BinProductOfArrows_comp|].
        now rewrite id_left, id_right. }
Qed.

Local Definition isColimProductOfColims : ∃! x : C ⟦ BinProductObject C (PC L M), K ⟧,
   ∏ v : nat,
   BinProductOfArrows C (PC L M) (PC (pr1 (dob cAB v)) (pr2 (dob cAB v)))
     (pr1 (coconeIn ccLM v)) (pr2 (coconeIn ccLM v)) · x =
   coconeIn ccK v.
Proof.
use tpair.
- use tpair.
  + apply (colimArrow HAiM K ccAiM_K).
  + cbn. apply is_cocone_morphism.
- cbn. apply is_unique_cocone_morphism.
Defined.

End omega_cocont_binproduct.

Lemma is_omega_cocont_binproduct_functor : is_omega_cocont (binproduct_functor PC).
Proof.
intros cAB LM ccLM HccLM K ccK; simpl in ×.
apply isColimProductOfColims, HccLM.
Defined.

End binprod_functor.