Definition left_unitor_of_pointedfunctors: left_unitor tensor_pointedfunctors (id_Ptd C). Proof. use make_nat_z_iso. + use make_nat_trans. * intro PF. exists (λ_functors (pr1 PF)). abstract ( intro c; cbn; rewrite id_right; apply id_left ). * abstract ( intros PF PF' α; apply eq_ptd_mor; apply (nat_trans_eq (homset_property C)); intro c; cbn; rewrite id_left; rewrite id_right; etrans; [apply cancel_postcomposition, functor_id | apply id_left] ). + intro PF. cbn. apply ptd_mor_z_iso_from_underlying_mor. intro c. cbn. apply identity_is_z_iso. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.UnitorsAndAssociatorsForEndofunctors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.HorizontalComposition. Require Import UniMath.CategoryTheory.PointedFunctors. Require Import UniMath.CategoryTheory.PointedFunctorsComposition. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsTensored. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsMonoidal.