Definition rightwhiskering_dispfunctor {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) (dbri : disp_bifunctor_rightidax DF) (dbrc : disp_bifunctor_rightcompax DF) : ∏ (y : B) (yy : DB y), disp_functor (rightwhiskering_functor F y) DA DC. Proof. intros y yy. use tpair. - use tpair. + intros x xx. exact (xx ⊗⊗_{DF} yy). + intros x1 x2 xx1 xx2 f ff. exact (ff ⊗⊗^{DF}_{r} yy). - use tpair. + intros x xx. exact (dbri x y xx yy). + intros x1 x2 x3 xx1 xx2 xx3 f1 f2 ff1 ff2. cbn. exact (dbrc x1 x2 x3 y f1 f2 xx1 xx2 xx3 yy ff1 ff2). Defined.
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.