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