Lemma omega_cocontConstCoprodFunctor : is_omega_cocont constcoprod_functor. Proof. intros hF c L ccL HcL cc. use tpair. - use tpair. + eapply BinCoproductArrow. * exact (BinCoproductIn1 (PC x (dob hF 0)) · pr1 cc 0). * use (let ccHcL : cocone hF HcL := _ in _). { use make_cocone. - intros n; exact (BinCoproductIn2 (PC x (dob hF n)) · pr1 cc n). - abstract ( intros m n e; destruct e; simpl; destruct cc as [f hf]; simpl in *; rewrite <- (hf m _ (idpath _)), !assoc; apply cancel_postcomposition; unfold constcoprod_functor; cbn; apply pathsinv0; etrans; [apply BinCoproductOfArrowsIn2|]; apply idpath). } apply (pr1 (pr1 (ccL HcL ccHcL))). + abstract ( destruct cc as [f hf]; simpl in *; simpl; intro n; unfold constcoprod_functor; cbn; etrans; [apply precompWithBinCoproductArrow |]; apply pathsinv0, BinCoproductArrowUnique; red in hf; [ rewrite id_left; induction n as [|n IHn]; [apply idpath|]; etrans; [| apply IHn]; unfold constant_functor; simpl; rewrite <- (hf n _ (idpath _)), assoc; unfold constant_functor; simpl; apply pathsinv0; etrans; [apply cancel_postcomposition; apply BinCoproductOfArrowsIn1 |]; now rewrite id_left | rewrite <- (hf n _ (idpath _)); destruct ccL as [t p]; destruct t as [t p0]; simpl in *; rewrite p0; simpl; now apply maponpaths, hf]). - abstract ( destruct cc as [f hf]; simpl in *; intro t; apply subtypePath; simpl; [ intro g; apply impred; intro; apply C | destruct t as [t p]; destruct ccL as [t0 p0]; unfold is_cocone_mor in *; unfold constcoprod_functor; destruct t0 as [t0 p1]; simpl; apply BinCoproductArrowUnique; [ unfold coconeIn in p; simpl in p; rewrite <- (p 0), assoc; apply cancel_postcomposition; apply pathsinv0; etrans; [apply BinCoproductOfArrowsIn1 |]; apply id_left | use (let temp : ∑ x0 : C ⟦ c, HcL ⟧, ∏ v : nat, coconeIn L v · x0 = BinCoproductIn2 (PC x (dob hF v)) · f v := _ in _); [ apply (tpair _ (BinCoproductIn2 (PC x c) · t)); intro n; unfold coconeIn in p; simpl in p; rewrite <- (p n), !assoc; apply cancel_postcomposition; apply pathsinv0; etrans; [apply BinCoproductOfArrowsIn2 |]; apply idpath|]; apply (maponpaths pr1 (p0 temp))]]). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.PartA. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Chains.All. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.PrecategoryBinProduct.