Lemma right_unitor_of_tensor (X Y : Mon_V) : r_unitor (X ⊗ Y) = α ((X, Y), I) · (id X #⊗ r_unitor Y). Proof. apply I_posttensor_faithful. rewrite tensor_comp_left. apply (post_comp_with_z_iso_is_inj (is_z_isomorphism_is_inverse_in_precat (pr2 α (_, _)))). rewrite assoc'. apply (transportb (λ h, _ = _ · h) (nat_trans_ax α _ _ ((_#, _)#, _))). simpl. rewrite assoc. apply (transportb (λ h, _ = _ · #tensor (id _ #, h)) (monoidal_cat_triangle_eq Mon_V _ _)). apply (transportf (λ k, _ = _ · #tensor (k #, _)) (id_left (id X))). change (?x · ?z #, ?y · ?w) with ((x #, y) · (z #, w)). rewrite (functor_comp tensor). apply (transportb (λ h, h · _ = _) (monoidal_cat_triangle_eq Mon_V _ _)). apply (transportf (λ h, _ · #tensor (h #, _) · _ = _) (functor_id tensor (X, Y))). rewrite assoc'. apply (transportb (λ h, _ · h = _) (nat_trans_ax α _ _ ((_#, _)#, _))). rewrite !assoc. apply cancel_postcomposition. apply monoidal_cat_pentagon_eq. Defined.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering.