proposition: Lemma cochain_limit_standard_limit_weq (cha cha' : cochain type_precat) : cochain_limit cha ≃ cochain_limit cha' → standard_limit cha ≃ standard_limit cha'.
proof: Proof. intro f. apply (weqcomp (invweq (lim_equiv _))). apply (weqcomp f). apply (lim_equiv _). Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Notations UniMath.MoreFoundations.PartA UniMath.MoreFoundations.Univalence UniMath.MoreFoundations.WeakEquivalences UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.Type.Core UniMath.CategoryTheory.Categories.Type.Limits UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.Chains.Cochains UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Terminal UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.Induction.FunctorCoalgebras_legacy UniMath.Induction.PolynomialFunctors UniMath.Induction.M.Limits UniMath.Induction.M.Core