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. apply isaprop_is_linear_nat_trans. Qed.
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.FunctorCategory. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.Invertible_2cells. Require Import UniMath.Bicategories.Core.Examples.BicatOfCats. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Actegories.Actegories. Require Import UniMath.CategoryTheory.Actegories.MorphismsOfActegories. Import BifunctorNotations.