Definition disp_bifunctor_rightcompax {A B C : category} {F : bifunctor A B C} {DA : disp_cat A} {DB : disp_cat B} {DC : disp_cat C} (DF : disp_bifunctor_data F DA DB DC) : UU := ∏ (x1 x2 x3 : A) (y : B) (f1 : A⟦x1,x2⟧) (f2 : A⟦x2,x3⟧) (xx1 : DA x1) (xx2 : DA x2) (xx3 : DA x3) (yy : DB y) (ff1 : xx1 -->[f1] xx2) (ff2 : xx2 -->[f2] xx3), ((ff1 ;; ff2) ⊗⊗^{DF}_{r} yy = transportb _ (bifunctor_rightcomp F _ _ _ _ f1 f2) ((ff1 ⊗⊗^{DF}_{r} yy) ;; (ff2 ⊗⊗^{DF}_{r} yy)) ).
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.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Isos. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Core.Isos. Import BifunctorNotations. Import DisplayedBifunctorNotations.