proposition: Corollary left_unitor_inv_of_tensor (X Y : Mon_V) : (nat_z_iso_to_trans_inv l_unitor _ #⊗ id _) · α ((_, _), _) = nat_z_iso_to_trans_inv l_unitor (X ⊗ Y).
proof: Proof. simpl. rewrite tensor_z_isomorphism_left. change (is_z_isomorphism_mor ?x) with (inv_from_z_iso (_,,x)). apply z_iso_inv_on_right, z_iso_inv_on_left. apply pathsinv0. apply left_unitor_of_tensor. Qed.
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