Lemma comp_fmonoidal_tensor_inv_laws (x y : C) : is_inverse_in_precat (fmonoidal_preservestensordata (comp_fmonoidal_lax Fm Gm) x y) (comp_fmonoidal_tensor_inv x y). Proof. unfold comp_fmonoidal_tensor_inv. split. - cbn. etrans. { rewrite !assoc'. apply maponpaths. rewrite assoc. apply cancel_postcomposition. rewrite <- functor_comp. apply maponpaths. apply (pr12 (fmonoidal_preservestensorstrongly Fm x y)). } rewrite functor_id. rewrite id_left. apply (pr12 (fmonoidal_preservestensorstrongly Gm (F x) (F y))). - cbn. etrans. { rewrite !assoc'. apply maponpaths. rewrite assoc. apply cancel_postcomposition. apply (pr22 (fmonoidal_preservestensorstrongly Gm (F x) (F y))). } rewrite id_left. rewrite <- functor_comp. etrans. { apply maponpaths. apply (pr22 (fmonoidal_preservestensorstrongly Fm x y)). } apply functor_id. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.whiskering. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Structure.Symmetric. Import BifunctorNotations. Import MonoidalNotations.