Lemma is_omega_cocont_Arity_to_Signature (TC : Terminal C) (CLC : Colims_of_shape nat_graph C) (H : ∏ (F : [C,C]), is_omega_cocont (constprod_functor1 F)) (xs : list nat) : is_omega_cocont (Arity_to_Signature TC xs). Proof. destruct xs as [[|n] xs]. - destruct xs; apply is_omega_cocont_constant_functor. - induction n as [|n IHn]. + destruct xs as [m []]; simpl. unfold Arity_to_Signature. apply is_omega_cocont_precomp_option_iter, CLC. + destruct xs as [m [k xs]]. apply is_omega_cocont_BinProduct_of_Signatures. * apply is_omega_cocont_precomp_option_iter, CLC. * apply (IHn (k,,xs)). * assumption. * intro x; apply (H x). 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.