Lemma total_associator_nat_leftwhisker {C : category} {D : disp_cat C} {M : monoidal C} {DM : disp_monoidal_data D M} (dαlnat : disp_associator_nat_leftwhisker dα^{DM}) : associator_nat_leftwhisker (total_associatordata dα^{DM}). Proof. intros x y z z' h. use total2_paths_b. - exact ((associatorlaw_natleft (monoidal_associatorlaw M)) (pr1 x) (pr1 y) (pr1 z) (pr1 z') (pr1 h)). - exact (dαlnat (pr1 x) (pr1 y) (pr1 z) (pr1 z') (pr1 h) (pr2 x) (pr2 y) (pr2 z) (pr2 z') (pr2 h)). 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.