proposition: Lemma isaprop_lax_monoidal_rightunitor_inverse {C : category} (luua : MonoidalCategoriesReordered.tensor_unit_unitors_associator C) : isaprop (lax_monoidal_rightunitor_inverse luua).
proof: Proof. apply isaproptotal2. { intro. apply impred_isaprop ; intro. apply Isos.isaprop_is_inverse_in_precat. } intros lui0 lui1 l0 l1. apply funextsec ; intro. use Isos.inverse_unique_precat. - apply luua. - apply l0. - apply l1. Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Univalence UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories