proposition: Lemma cochain_limit_is_limit : ∑ c : cone coch cochain_limit, is_limit_cone c.
proof: Proof. assert (H : (∑ c : cone coch cochain_limit, is_limit_cone c) ≃ ∑ c : cone coch (standard_limit coch), is_limit_cone c ). { induction (weqtopaths lim_equiv). apply idweq. } apply H. eapply tpair. apply limit_universal. Defined.
imports: UniMath.Foundations.PartD UniMath.Foundations.Sets UniMath.MoreFoundations.Univalence UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Categories.Type.Core UniMath.CategoryTheory.Limits.Graphs.Limits UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Chains.Cochains