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. refine (foldr1_map_ind_nodep (BinProduct_of_Signatures _ _ _ BPC) _ _ is_omega_cocont _ _ _ xs). - apply is_omega_cocont_constant_functor. - intro n. apply is_omega_cocont_precomp_option_iter, CLC. - intros m sig Hyp. apply is_omega_cocont_BinProduct_of_Signatures. + apply is_omega_cocont_precomp_option_iter, CLC. + exact Hyp. + exact BPC. + exact H. 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.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.LiftingInitial_alt. Require Import UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems. Require Import UniMath.SubstitutionSystems.Notation.