proposition: Lemma isaprop_bidisp_actionbicat_disp_2cell_struct {a a' : B} {f1 f2 : B ⟦ a, a' ⟧} (η : f1 ==> f2) {M : disp_actionbicat_disp_catdata a} {M' : disp_actionbicat_disp_catdata a'} (FM1 : M -->[ f1] M') (FM2 : M -->[ f2] M'): isaprop (bidisp_actionbicat_disp_2cell_struct a a' f1 f2 η M M' FM1 FM2).
proof: Proof. apply impred. intro v. apply isaprop_bidisp_actionbicat_disp_2cell_eq_body. 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