Definition STLC : HSET_over_sort2 := alg_carrier _ (InitialObject STLC_Functor_Initial). Let STLC_mor : HSET_over_sort2⟦STLC_Functor STLC,STLC⟧ := alg_map _ (InitialObject STLC_Functor_Initial). Let STLC_alg : algebra_ob STLC_Functor := InitialObject STLC_Functor_Initial. Local Lemma BP : BinProducts [HSET_over_sort,HSET]. Proof. apply BinProducts_functor_precat, BinProductsHSET. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Sets. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.Combinatorics.Lists. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. 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.Slice. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Coproducts. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.slicecat. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial_alt. Require Import UniMath.SubstitutionSystems.Notation. Require Import UniMath.SubstitutionSystems.MonadsMultiSorted. Require Import UniMath.SubstitutionSystems.MultiSorted. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.MultiSortedMonadConstruction.