proposition: Lemma cochain_on_n_is_zero {I : HSET} (ind : pr1 I → cochain SET) (f : pr111 (limit_of_coproduct SET HSET_ω_limits (CoproductsHSET (pr1 I) (pr2 I)) ind)) : ∏ n : nat, pr1 (pr1 f n) = pr1 (pr1 f 0).
proof: Proof. induction f as [f p]. assert (q0 : ∏ n : nat, S n = n + 1). { exact (λ n, ! natpluscomm n 1). } assert (q : ∏ n : nat, pr1 (f (n+1)) = pr1 (f n)). { exact (λ n, base_paths _ _ (p (n+1) n (q0 n))). } assert (q' : ∏ n : nat, pr1 (f (S n)) = pr1 (f n)). { intro n. refine (_ @ q n). apply (maponpaths (λ z, pr1 (f z))). exact (q0 n). } intro n. induction n. - apply idpath. - exact (q' n @ IHn). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.Combinatorics.Lists UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.BinProducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Initial UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.exponentials UniMath.CategoryTheory.Adjunctions.Core UniMath.CategoryTheory.Chains.All UniMath.CategoryTheory.Categories.HSET.Core UniMath.CategoryTheory.Categories.HSET.Limits UniMath.CategoryTheory.Categories.HSET.Colimits UniMath.CategoryTheory.Categories.HSET.Structures UniMath.CategoryTheory.Categories.StandardCategories UniMath.CategoryTheory.Groupoids UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.SumOfSignatures UniMath.SubstitutionSystems.BinProductOfSignatures UniMath.SubstitutionSystems.MultiSorted_alt UniMath.CategoryTheory.Chains.OmegaContFunctors UniMath.SubstitutionSystems.ContinuitySignature.GeneralLemmas UniMath.SubstitutionSystems.ContinuitySignature.CommutingOfOmegaLimitsAndCoproducts UniMath.SubstitutionSystems.ContinuitySignature.ContinuityOfMultiSortedSigToFunctor UniMath.SubstitutionSystems.ContinuitySignature.MultiSortedSignatureFunctorEquivalence