Definition initChain {C : category} (InitC : Initial C) (F : functor C C) : chain C. Proof. exists (λ n, iter_functor F n InitC). intros m n Hmn. destruct Hmn. simpl. induction m as [|m IHm]; simpl. - exact (InitialArrow InitC _). - exact (# F IHm). Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. 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.Initial.