Definition fbracket_for_LamE_algebra_on_Lam : ∏ (C : category) (terminal : Terminal C) (CC : BinCoproducts C) (CP : BinProducts C) (KanExt : ∏ Z : category_Ptd C, GlobalRightKanExtensionExists C C (U Z) C) (Lam_Initial : Initial (FunctorAlg (Id_H C CC (Lam_Sig C terminal CC CP)))) (Z : category_Ptd C), category_Ptd C ⟦ Z , (ptd_from_alg_functor CC (LamE_Sig C terminal CC CP)) (LamE_algebra_on_Lam C terminal CC CP KanExt Lam_Initial) ⟧ → [C, C] ⟦ functor_composite (U Z) ` (LamE_algebra_on_Lam C terminal CC CP KanExt Lam_Initial), ` (LamE_algebra_on_Lam C terminal CC CP KanExt Lam_Initial) ⟧. Proof. apply fbracket_for_LamE_algebra_on_Lam. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Adjunctions.Core. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monads.Monads. Require Import UniMath.CategoryTheory.Limits.BinProducts. Require Import UniMath.CategoryTheory.Limits.BinCoproducts. Require Import UniMath.CategoryTheory.Limits.Initial. Require Import UniMath.CategoryTheory.Limits.Terminal. Require Import UniMath.CategoryTheory.FunctorAlgebras. Require Import UniMath.CategoryTheory.opp_precat. Require Import UniMath.CategoryTheory.yoneda. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.SubstitutionSystems.Signatures. Require Import UniMath.SubstitutionSystems.BinSumOfSignatures. Require Import UniMath.SubstitutionSystems.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.GenMendlerIteration. Require Import UniMath.CategoryTheory.RightKanExtension. Require Import UniMath.SubstitutionSystems.GenMendlerIteration. Require Import UniMath.SubstitutionSystems.LiftingInitial. Require Import UniMath.SubstitutionSystems.MonadsFromSubstitutionSystems. Require Import UniMath.SubstitutionSystems.LamSignature. Require Import UniMath.SubstitutionSystems.Lam. Require Import UniMath.SubstitutionSystems.Notation.