Lemma total_associator_nat_rightwhisker {C : category} {D : disp_cat C} {M : monoidal C} {DM : disp_monoidal_data D M} (dαrnat : disp_associator_nat_rightwhisker dα^{DM}) : associator_nat_rightwhisker (total_associatordata dα^{DM}). Proof. intros x1 x2 y z f. use total2_paths_b. - exact ((associatorlaw_natright (monoidal_associatorlaw M)) (pr1 x1) (pr1 x2) (pr1 y) (pr1 z) (pr1 f)). - exact (dαrnat (pr1 x1) (pr1 x2) (pr1 y) (pr1 z) (pr1 f) (pr2 x1) (pr2 x2) (pr2 y) (pr2 z) (pr2 f)). Qed.
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.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories. Require Import UniMath.CategoryTheory.Monoidal.Displayed.WhiskeredDisplayedBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Displayed.Monoidal. Require Import UniMath.CategoryTheory.Monoidal.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Total. Import BifunctorNotations. Import MonoidalNotations. Import DisplayedBifunctorNotations. Import DisplayedMonoidalNotations.