fact: Definition fbracket_unique_pointwise (T : hss) {Z : Ptd} (f : U Z --> `T) : ∏ (α : functor_composite (U Z) `T ⟹ pr1 `T), (∏ c : C, pr1 f c = pr1 (η T) (pr1 (U Z) c) · α c) → (∏ c : C, pr1 (θ (`T ⊗ Z)) c · pr1 (#H α) c · pr1 (τ T) c = pr1 (τ T) (pr1 (U Z) c) · α c) → α = ⦃f⦄_{Z}.
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