fact: Definition isbracketMor {T T' : hss} (β : algebra_mor _ T T') : UU := ∏ (Z : Ptd) (f : Z --> ptd_from_alg T), ⦃ f ⦄ · β = β •• U Z · ⦃ f · # ptd_from_alg_functor β ⦄.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.FunctorAlgebras UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PointedFunctorsComposition UniMath.SubstitutionSystems.Signatures UniMath.SubstitutionSystems.Notation