proposition: Lemma isaprop_bidisp_monbicat_disp_2cell_struct {C D : bicat_of_cats} {F G : bicat_of_cats ⟦C,D⟧ } {α : prebicat_cells bicat_of_cats F G} {M : disp_monbicat_disp_catdata C} {N : disp_monbicat_disp_catdata D} (Fm : M -->[ F] N) (Gm : M -->[ G] N) : isaprop (bidisp_monbicat_disp_2cell_struct C D F G α M N Fm Gm).
proof: Proof. apply isaprop_is_mon_nat_trans. Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.FunctorCategory UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Total UniMath.Bicategories.Core.Bicat UniMath.Bicategories.Core.Invertible_2cells UniMath.Bicategories.Core.Examples.BicatOfCats UniMath.Bicategories.DisplayedBicats.DispBicat UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors UniMath.CategoryTheory.Monoidal.Categories UniMath.CategoryTheory.Monoidal.Functors