Definition I_coproduct_distribute_over_omega_limits_HSET (I : HSET) : ω_limits_distribute_over_I_coproducts HSET I HSET_ω_limits (CoproductsHSET (pr1 I) (pr2 I)). Proof. intro ind. use make_is_z_isomorphism. - exact (I_coproduct_distribute_over_omega_limit_HSET_inverse ind). - split. + apply funextsec ; intros [i [f p]]. use total2_paths_f. { apply idpath. } use total2_paths_f. 2: { repeat (apply funextsec ; intro). apply (pr2 (dob (ind (pr1 (identity (pr11 (coproduct_of_limit SET HSET_ω_limits (CoproductsHSET (pr1 I) (pr2 I)) ind)) _))) _)). } rewrite idpath_transportf. repeat (apply funextsec ; intro). apply (transportf_set ((λ u : pr1 I, pr1 (dob (ind u) x)))). apply (pr2 I). + apply funextsec ; intros [f p]. use total2_paths_f. * apply funextsec ; intro n. use total2_paths_f. { exact (! cochain_on_n_is_zero ind (f,,p) n). } cbn. etrans. 1: apply (transport_f_f (λ x : pr1 I, pr1 (pr1 (ind x) n))). etrans. 1: apply maponpaths_2, pathsinv0r. apply (idpath_transportf (λ x : pr1 I, pr1 (pr1 (ind x) n))). * repeat (apply funextsec ; intro). apply ( dob (coproduct_n_cochain SET (CoproductsHSET (pr1 I) (pr2 I)) ind) _). 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.MultiSortedBindingSig. Require Import UniMath.SubstitutionSystems.MultiSorted_alt. Require Import UniMath.CategoryTheory.Chains.OmegaContFunctors. Require Import UniMath.SubstitutionSystems.ContinuitySignature.GeneralLemmas. Require Import UniMath.SubstitutionSystems.ContinuitySignature.CommutingOfOmegaLimitsAndCoproducts. Require Import UniMath.SubstitutionSystems.ContinuitySignature.ContinuityOfMultiSortedSigToFunctor. Require Import UniMath.SubstitutionSystems.ContinuitySignature.MultiSortedSignatureFunctorEquivalence.