Lemma left_unitor_of_tensor (X Y : Mon_V) : α ((I, X), Y) · l_unitor (X ⊗ Y) = l_unitor X #⊗ id Y. Proof. apply I_pretensor_faithful. rewrite tensor_comp_right. apply (pre_comp_with_z_iso_is_inj (pr2 α ((I, (I ⊗ X)), Y))). use (pathscomp0 _ (nat_trans_ax α _ _ ((_ #, _) #, _))). simpl. apply (pre_comp_with_z_iso_is_inj (functor_on_is_z_isomorphism (functor_fix_snd_arg _ _ _ tensor Y) (pr2 α ((I, I), X)))). simpl. unfold functor_fix_snd_arg_mor. change (make_dirprod ?x ?y) with (x #, y). rewrite !assoc. apply (transportf (λ h, _ = h · _) (functor_comp tensor _ _)). change ((?x #, ?y) · (?z #, ?w)) with (x · z #, y · w). apply (transportf (λ h, h · _ = _) (monoidal_cat_pentagon_eq Mon_V I I X Y)). rewrite assoc'. apply (transportf (λ h, _ · h = _) (monoidal_cat_triangle_eq Mon_V _ _)). simpl. apply (transportf (λ h, _ · #tensor (_ #, h) = _) (functor_id tensor (X, Y))). apply (pathscomp0 (! (nat_trans_ax α _ _ ((_ #, _) #, _)))). simpl. apply cancel_postcomposition. apply pathsinv0. apply maponpaths. apply dirprod_paths; simpl; [|apply id_left]. apply pathsinv0. apply monoidal_cat_triangle_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.