Definition left_unitor_of_endofunctors: left_unitor (functorial_composition _ _ _) (functor_identity C). Proof. use make_nat_z_iso. + use make_nat_trans. * intro F. apply λ_functors. * apply is_nat_trans_left_unitor_data. + red. intro F. cbn. use nat_trafo_z_iso_if_pointwise_z_iso. intro c. use tpair. * exact (identity (pr1 F c)). * abstract ( apply Isos.is_inverse_in_precat_identity ). Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesTensored. Require Import UniMath.Bicategories.MonoidalCategories.MonoidalFromBicategory. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats.