Definition I_coproduct_distribute_over_omega_limit_HSET_inverse {I : HSET} (ind : pr1 I → cochain SET) : SET ⟦ pr11 (limit_of_coproduct SET HSET_ω_limits (CoproductsHSET (pr1 I) (pr2 I)) ind), pr11 (coproduct_of_limit SET HSET_ω_limits (CoproductsHSET (pr1 I) (pr2 I)) ind) ⟧. Proof. intros [f p]. exists (pr1 (f 0)). exists (λ n, transportf (λ u, pr1 (dob (ind u) n)) ((cochain_on_n_is_zero ind (f,,p) n)) (pr2 (f n))). intros n m h. etrans. 2: { apply maponpaths. exact (fiber_paths (p n m h)). } rewrite transport_f_f. cbn. set (q := base_paths (pr1 (f n),, pr2 (ind (pr1 (f n))) n m h (pr2 (f n))) (f m) (p n m h) @ cochain_on_n_is_zero ind (f,, p) m). set (q' := cochain_on_n_is_zero ind (f,,p) n). assert (q0 : q = q'). { apply (pr2 I). } etrans. 2: { apply maponpaths_2. exact (! q0). } set (J := λ i n, (pr1 (ind i) n)). transparent assert (Jmor : (∏ (i : pr1 I) (n : nat), pr1 (J i (S n)) → pr1 (J i n))). { intros i0 n0. use (dmor (ind i0)). apply idpath. } set (f0 := λ n0, pr1 (f n0)). transparent assert (f' : (∏ n : nat, pr1 (J (f0 n) n))). { exact (λ n0, pr2 (f n0)). } transparent assert (p' : (∏ n : nat, f0 n = f0 0)). { exact (cochain_on_n_is_zero ind (f,,p)). } induction h. exact (dmor_distribute_over_transport_ω J Jmor f0 f' m p'). 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.