Lemma compute_fbracket : ∏ (C : category) (CP : BinCoproducts C) (H : Presignature C C C) (T : hss CP H) (Z : category_Ptd C) (f : category_Ptd C ⟦ Z, ptd_from_alg T ⟧), ⦃#U f⦄_{Z} = (`T ∘ # U f : [C, C] ⟦ `T • U Z , `T • U _ ⟧) · ⦃ identity (U (ptd_from_alg T)) ⦄_{ptd_from_alg T}. Proof. apply compute_fbracket. Qed.
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.SimplifiedHSS.SubstitutionSystems. Require Import UniMath.SubstitutionSystems.GenMendlerIteration. Require Import UniMath.CategoryTheory.RightKanExtension. Require Import UniMath.SubstitutionSystems.GenMendlerIteration. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.LiftingInitial. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.MonadsFromSubstitutionSystems. Require Import UniMath.SubstitutionSystems.LamSignature. Require Import UniMath.SubstitutionSystems.SimplifiedHSS.Lam. Require Import UniMath.SubstitutionSystems.Notation.