Definition coproduct_of_functors_omega_cont (C : category) (F : (pr1 I) → C ⟶ D) (ω_distr : ω_limits_distribute_over_I_coproducts D I ω_lim CP) : (∏ i : pr1 I, is_omega_cont (F i)) -> is_omega_cont (coproduct_of_functors _ _ _ CP F). Proof. intro Fi_cont. intros coch l l_cone l_lim. use Limits.is_z_iso_isLim. { apply ω_lim. } transparent assert (ind : (pr1 I -> cochain D)). { intro i. exists (λ n, F i (dob coch n)). exact (λ n m p, #(F i) (dmor coch p)). } set (distr := ω_distr ind). set (distr1 := pr1 distr). unfold limit_of_coproduct in distr1. unfold coproduct_of_limit in distr1. use make_is_z_isomorphism. - refine (distr1 · _). use CoproductOfArrows. intro i. set (Fi_l := Fi_cont i coch l l_cone l_lim). apply (pr1 (isLim_is_z_iso _ _ _ _ Fi_l)). - split. + cbn. transparent assert (i_iso : (is_z_isomorphism (CoproductOfArrows (pr1 I) D (CP (λ i : pr1 I, lim (ω_lim (ind i)))) (CP (λ i : pr1 I, F i l)) (λ i : pr1 I, limArrow (make_LimCone (mapdiagram (F i) coch) (F i l) (mapcone (F i) coch l_cone) (Fi_cont i coch l l_cone l_lim)) (lim (ω_lim (ind i))) (limCone (ω_lim (ind i))))))). { use CoproductOfArrowsIsos. intro i. set (Fi_l := Fi_cont i coch l l_cone l_lim). apply (pr2 (z_iso_inv (_ ,, isLim_is_z_iso _ _ _ _ Fi_l))). } etrans. 1: apply assoc. use (z_iso_inv_to_right _ _ _ _ (_ ,, i_iso)). etrans. 2: apply pathsinv0, id_left. use CoproductArrowUnique. intro i. cbn. etrans. 1: apply assoc. etrans. 1: apply maponpaths_2, postCompWithLimArrow. use (z_iso_inv_to_right _ _ _ _ (distr1 ,, _)). { unfold coproduct_distribute_over_omega_limits in distr. apply (pr2 (z_iso_inv (_,,distr))). } apply pathsinv0, limArrowUnique. intro n. cbn. etrans. 1: apply assoc'. etrans. 1: { apply maponpaths. set (t := limArrowCommutes (ω_lim (mapdiagram (coproduct_of_functors (pr1 I) C D CP F) coch))). exact (t (pr11 (CP (λ i0 : pr1 I, lim (ω_lim (ind i0))))) (limit_of_coproduct_as_cone_of_coproduct_to_limit D ω_lim CP ind) n). } cbn. unfold CoproductOfArrows. etrans. 1: apply assoc'. etrans. 1: { apply maponpaths. apply (CoproductInCommutes _ _ _ (CP (λ i0 : pr1 I, lim (ω_lim (ind i0))))). } etrans. 2: apply pathsinv0, (CoproductInCommutes _ _ _ (CP (λ j : pr1 I, F j l))). etrans. 1: apply assoc. apply maponpaths_2. exact (limArrowCommutes (ω_lim (ind i)) (F i l) (mapcone (F i) coch l_cone) n). + cbn. etrans. 1: apply assoc'. apply pathsinv0. use (z_iso_inv_to_left _ _ _ (_,,_)). { unfold coproduct_distribute_over_omega_limits in distr. apply (pr2 (z_iso_inv (_,,distr))). } etrans. 1: apply id_right. apply pathsinv0. use limArrowUnique. intro n. etrans. 1: apply assoc'. etrans. 1: { apply maponpaths. apply (limArrowCommutes (ω_lim (mapdiagram (coproduct_of_functors (pr1 I) C D CP F) coch))). } etrans. 1: apply CoproductOfArrows_comp. use CoproductArrowUnique. intro i. etrans. 1: apply (CoproductInCommutes _ _ _ (CP (λ i0 : pr1 I, lim (ω_lim (ind i0))))). apply maponpaths_2. exact (limArrowCommutes ( (make_LimCone (mapdiagram (F i) coch) (F i l) (mapcone (F i) coch l_cone) (Fi_cont i coch l l_cone l_lim))) _ (limCone (ω_lim (ind i))) n). Defined.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. 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.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.Chains.All. 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.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Categories.StandardCategories. Require Import UniMath.CategoryTheory.Groupoids. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SumOfSignatures. Require Import UniMath.SubstitutionSystems.BinProductOfSignatures. Require Import UniMath.SubstitutionSystems.MultiSorted_alt. Require Import UniMath.CategoryTheory.Chains.OmegaContFunctors. Require Import UniMath.SubstitutionSystems.ContinuitySignature.GeneralLemmas.