proposition: Lemma lim_equiv : cochain_limit ≃ (standard_limit coch).
proof: Proof. unfold cochain_limit, standard_limit; cbn. apply weqfibtototal; intro. use weq_iso. - intros eq. intros u v e. specialize (eq v). unfold π', π in *; unfold dmor. refine (_ @ eq). apply simplify_cochain_step. - intros eq; intro; apply eq. - abstract ( intro; apply funextsec; intro; reflexivity ). - abstract ( intro; cbn; do 2 (apply funextsec; intro); apply funextsec; intro p; induction p; reflexivity ). 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