Definition termCochain {C : precategory} (TermC : Terminal C) (F : functor C C) : cochain C. Proof. use cochain_weq; use tpair. - exact (λ m, iter_functor F m TermC). - intros n; induction n as [|n IHn]. * exact (TerminalArrow TermC _). * exact (# F IHn). 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.