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. 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.
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.