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)).
Require Import UniMath.Foundations.PartD. 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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal. Require Import UniMath.CategoryTheory.Monoidal.Displayed.TotalMonoidal. Require Import UniMath.Bicategories.MonoidalCategories.EndofunctorsWhiskeredMonoidal. Require Import UniMath.Bicategories.MonoidalCategories.WhiskeredMonoidalFromBicategory. Require Import UniMath.Bicategories.MonoidalCategories.ActionBasedStrongFunctorsWhiskeredMonoidal. Require Import UniMath.Bicategories.Core.Bicat. Require Import UniMath.Bicategories.Core.BicategoryLaws. Require Import UniMath.Bicategories.Core.Unitors. Require Import UniMath.Bicategories.DisplayedBicats.DispBicat. Require Import UniMath.Bicategories.Core.Invertible_2cells. Import Bicat.Notations. Import BifunctorNotations. Import DisplayedBifunctorNotations.