Lemma is_omega_cocont_precomp_option_iter (BCC : BinCoproducts C) (TC : Terminal C) (CLC : Colims_of_shape nat_graph C) (n : nat) : is_omega_cocont (precomp_option_iter BCC TC n). Proof. destruct n; simpl. - apply is_omega_cocont_functor_identity. - apply is_omega_cocont_pre_composition_functor, CLC. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.Chains.All. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SignatureExamples. Require Import UniMath.SubstitutionSystems.SumOfSignatures. Require Import UniMath.SubstitutionSystems.BinProductOfSignatures. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial_alt. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.MonadsFromSubstitutionSystems. Require Import UniMath.SubstitutionSystems.Notation.