proposition: Lemma isaprop_bidisp_actbicat_disp_2cell_struct {C D : bicat_of_cats} {F G : bicat_of_cats ⟦C,D⟧ } {ξ : prebicat_cells bicat_of_cats F G} {ActC : disp_actbicat_disp_catdata C} {ActD : disp_actbicat_disp_catdata D} (Fl : ActC -->[F] ActD) (Gl : ActC -->[G] ActD) : isaprop (bidisp_actbicat_disp_2cell_struct C D F G ξ ActC ActD Fl Gl).
proof: Proof. apply isaprop_is_linear_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 UniMath.CategoryTheory.Actegories.Actegories UniMath.CategoryTheory.Actegories.MorphismsOfActegories