Definition BindingSigToMonadHSET : BindingSig → Monad HSET. Proof. intros sig; use (BindingSigToMonad _ _ _ _ _ _ sig). - apply BinProductsHSET. - apply BinCoproductsHSET. - apply TerminalHSET. - apply InitialHSET. - apply ColimsHSET_of_shape. - intros F. apply is_omega_cocont_constprod_functor1. apply Exponentials_functor_HSET. - apply CoproductsHSET. apply BindingSigIsaset. 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.