proposition: Lemma isaprop_bidisp_actionbicat_disp_2cell_eq_body {a a' : B} {f1 f2 : B ⟦ a, a' ⟧} (η : f1 ==> f2) (FA : V ⟶ category_from_bicat_and_ob a) (FA' : V ⟶ category_from_bicat_and_ob a') (δ1 : parameterized_distributivity_bicat_nat f1) (δ2 : parameterized_distributivity_bicat_nat f2) (v : V): isaprop (bidisp_actionbicat_disp_2cell_eq_body η FA FA' δ1 δ2 v).
proof: Proof. apply B. Qed.
imports: UniMath.Foundations.PartD UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Functors UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors UniMath.CategoryTheory.Monoidal.Displayed.Monoidal UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal UniMath.Bicategories.MonoidalCategories.EndofunctorsWhiskeredMonoidal UniMath.Bicategories.MonoidalCategories.WhiskeredMonoidalFromBicategory UniMath.Bicategories.MonoidalCategories.ActionBasedStrongFunctorsWhiskeredMonoidal UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.BicategoryLaws UniMath.Bicategories.Core.Unitors UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.Bicategories.Core.Invertible_2cells