Definition cochain_weq {C : precategory} : (∑ (obs : ∏ n : nat, ob C), (∏ n : nat, obs (S n) --> obs n)) ≃ cochain C. Proof. use weqfibtototal; intro obs; cbn. use weq_iso. - intros ars a b aeqSb. refine (_ · ars b). exact (transportf (λ o, C ⟦ obs o, obs (S b) ⟧) aeqSb (identity _)). - exact (λ ars n, ars (S n) n (idpath _)). - intros ars; cbn. apply funextsec; intro n. apply id_left. - intros ars. cbn. apply funextsec; intro a. apply funextsec; intro b. apply funextsec; intro p. induction p. cbn. apply id_left. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Graphs.Limits. Require Import UniMath.CategoryTheory.Limits.Terminal.