proposition: Lemma monoidal_cat_triangle_eq_inv (X Y : Mon_V) : (nat_z_iso_to_trans_inv r_unitor X #⊗ id Y) · α ((X, I), Y) = (id X #⊗ nat_z_iso_to_trans_inv l_unitor Y).
proof: Proof. cbn. rewrite (tensor_z_isomorphism_right _ _ _ _ _ : #tensor _ = _). rewrite (tensor_z_isomorphism_left _ _ _ _ _ : #tensor _ = _). change (is_z_isomorphism_mor ?x) with (inv_from_z_iso (_,,x)). apply z_iso_inv_on_right, z_iso_inv_on_left. apply monoidal_cat_triangle_eq. 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