proposition: Lemma comp_fmonoidal_unit_inv_laws : is_inverse_in_precat (fmonoidal_preservesunit (comp_fmonoidal_lax Fm Gm)) comp_fmnoidal_unit_inv.
proof: Proof. unfold comp_fmnoidal_unit_inv. split. - cbn. etrans. { rewrite !assoc'. apply maponpaths. rewrite assoc. apply cancel_postcomposition. rewrite <- functor_comp. apply maponpaths. apply (pr12 (fmonoidal_preservesunitstrongly Fm)). } rewrite functor_id. rewrite id_left. apply (pr12 (fmonoidal_preservesunitstrongly Gm)). - cbn. etrans. { rewrite !assoc'. apply maponpaths. rewrite assoc. apply cancel_postcomposition. apply (pr22 (fmonoidal_preservesunitstrongly Gm)). } rewrite id_left. rewrite <- functor_comp. etrans. { apply maponpaths. apply (pr22 (fmonoidal_preservesunitstrongly Fm)). } apply functor_id. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.whiskering UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Structure.Symmetric