proposition: Lemma left_unitor_right_unitor_of_unit : l_unitor I = r_unitor I.
proof: Proof. apply I_pretensor_faithful. apply (pre_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 α ((_, _), _)))). apply (pathscomp0 (! (monoidal_cat_triangle_eq Mon_V I I))). use (pathscomp0 _ (right_unitor_of_tensor I I)). apply (post_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 r_unitor _))). apply (nat_trans_ax r_unitor). Defined.
imports: UniMath.Foundations.PartD UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.ProductCategory UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.whiskering