proposition: Lemma actionbicat_disp_locally_groupoid : disp_locally_groupoid bidisp_actionbicat_disp_bicat.
proof: Proof. red. intros a a' f1 f2 ηinvertible [FA FAm] [FA' FA'm] [δ1 [tria1 penta1]] [δ2 [tria2 penta2]] is2cell. use tpair. - red. cbn. red. intro v. red. transparent assert (invertible1 : (invertible_2cell (FA v · f2) (FA v · f1))). { use make_invertible_2cell. - exact (FA v ◃ ηinvertible ^-1). - is_iso. } transparent assert (invertible2 : (invertible_2cell (f2 · FA' v) (f1 · FA' v))). { use make_invertible_2cell. - exact (ηinvertible ^-1 ▹ FA' v). - is_iso. } apply (lhs_right_invert_cell _ _ _ invertible1). rewrite vassocl. apply pathsinv0, (lhs_left_invert_cell _ _ _ invertible2). exact (is2cell v). - split; apply isaprop_bidisp_actionbicat_disp_2cell_struct. 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