proposition: Lemma triangle_eq_of_pointedfunctors : triangle_eq tensor_pointedfunctors (id_Ptd C) left_unitor_of_pointedfunctors right_unitor_of_pointedfunctors associator_of_pointedfunctors.
proof: Proof. intros PF1 PF2. apply eq_ptd_mor. apply (nat_trans_eq (homset_property C)). intro c. cbn. do 2 rewrite id_right. apply pathsinv0, id_left. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.HorizontalComposition UniMath.CategoryTheory.PointedFunctors UniMath.CategoryTheory.PointedFunctorsComposition UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal