proposition: Lemma compute_fbracket (T : hss) : ∏ {Z : Ptd} (f : Z --> ptd_from_alg T), ⦃#U f⦄_{Z} = (`T ∘ # U f : EndC⟦`T • U Z , `T • U (ptd_from_alg T)⟧) · ⦃identity (U (ptd_from_alg T))⦄_{ptd_from_alg T}.
proof: Proof. intros Z f. assert (A : f = f · identity _ ). { rewrite id_right; apply idpath. } rewrite A. rewrite functor_comp. rewrite <- fbracket_natural. rewrite id_right. apply idpath. Qed.
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