fact: Definition actionbicat_ax2 : UU := (∏ (a b c d : B) (f : B ⟦ a, b ⟧) (g : B ⟦ b, c ⟧) (h : B ⟦ c, d ⟧) (w : bidisp_actionbicat_disp_prebicat_1_id_comp_cells a) (x : bidisp_actionbicat_disp_prebicat_1_id_comp_cells b) (y : bidisp_actionbicat_disp_prebicat_1_id_comp_cells c) (z : bidisp_actionbicat_disp_prebicat_1_id_comp_cells d) (ff : w -->[ f] x) (gg : x -->[ g] y) (hh : y -->[ h] z), disp_2cells (rassociator f g h) (ff ;; gg ;; hh) (ff ;; (gg ;; hh))) × (∏ (a b c d : B) (f : B ⟦ a, b ⟧) (g : B ⟦ b, c ⟧) (h : B ⟦ c, d ⟧) (w : bidisp_actionbicat_disp_prebicat_1_id_comp_cells a) (x : bidisp_actionbicat_disp_prebicat_1_id_comp_cells b) (y : bidisp_actionbicat_disp_prebicat_1_id_comp_cells c) (z : bidisp_actionbicat_disp_prebicat_1_id_comp_cells d) (ff : w -->[ f] x) (gg : x -->[ g] y) (hh : y -->[ h] z), disp_2cells (lassociator f g h) (ff ;; (gg ;; hh)) (ff ;; gg ;; hh)) × (∏ (a b : B) (f g h : B ⟦ a, b ⟧) (r : f ==> g) (s : g ==> h) (x : bidisp_actionbicat_disp_prebicat_1_id_comp_cells a) (y : bidisp_actionbicat_disp_prebicat_1_id_comp_cells b) (ff : x -->[ f] y) (gg : x -->[ g] y) (hh : x -->[ h] y), disp_2cells r ff gg → disp_2cells s gg hh → disp_2cells (r • s) ff hh) × (∏ (a b c : B) (f : B ⟦ a, b ⟧) (g1 g2 : B ⟦ b, c ⟧) (r : g1 ==> g2) (x : bidisp_actionbicat_disp_prebicat_1_id_comp_cells a) (y : bidisp_actionbicat_disp_prebicat_1_id_comp_cells b) (z : bidisp_actionbicat_disp_prebicat_1_id_comp_cells c) (ff : x -->[ f] y) (gg1 : y -->[ g1] z) (gg2 : y -->[ g2] z), disp_2cells r gg1 gg2 → disp_2cells (f ◃ r) (ff ;; gg1) (ff ;; gg2)) × (∏ (a b c : B) (f1 f2 : B ⟦ a, b ⟧) (g : B ⟦ b, c ⟧) (r : f1 ==> f2) (x : bidisp_actionbicat_disp_prebicat_1_id_comp_cells a) (y : bidisp_actionbicat_disp_prebicat_1_id_comp_cells b) (z : bidisp_actionbicat_disp_prebicat_1_id_comp_cells c) (ff1 : x -->[ f1] y) (ff2 : x -->[ f2] y) (gg : y -->[ g] z), disp_2cells r ff1 ff2 → disp_2cells (r ▹ g) (ff1 ;; gg) (ff2 ;; gg)).
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