Lemma is_omega_cocont_BindingSigToSignature : ∏ (C : category) (BPC : BinProducts C) (BCC : BinCoproducts C) (TC : Terminal C), Colims_of_shape nat_graph C → (∏ F : functor_category C C, is_omega_cocont (constprod_functor1 (BinProducts_functor_precat C C BPC) F)) → ∏ (sig : BindingSig) (CC : Coproducts (BindingSigIndex sig) C), is_omega_cocont (pr1 (BindingSigToSignature BPC BCC TC sig CC)). Proof. exact @UniMath.SubstitutionSystems.SimplifiedHSS.BindingSigToMonad.is_omega_cocont_BindingSigToSignature. Defined.
Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.Categories.HSET.Core. Require Import UniMath.CategoryTheory.Categories.HSET.Colimits. Require Import UniMath.CategoryTheory.Categories.HSET.Limits. Require Import UniMath.CategoryTheory.Categories.HSET.Structures. Require Import UniMath.CategoryTheory.Limits.Graphs.Colimits. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.Products. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.Chains.All. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.exponentials. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.SubstitutionSystems.SignatureCategory. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.BindingSigToMonad. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial_alt.