Lemma isaprop_lax_monoidal_leftunitor_inverse {C : category} (luua : MonoidalCategoriesReordered.tensor_unit_unitors_associator C) : isaprop (lax_monoidal_leftunitor_inverse luua). 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.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Univalence. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesReordered. Require Import UniMath.Bicategories.MonoidalCategories.UnivalenceMonCat.CurriedMonoidalCategories. Import BifunctorNotations.