Lemma total_associator_iso_law {C : category} {D : disp_cat C} {M : monoidal C} {DM : disp_monoidal_data D M} (dαiso : disp_associator_iso dα^{DM} dαinv^{DM}) : associator_iso_law (total_associatordata dα^{DM}) (total_associatorinvdata dαinv^{DM}). Proof. intros x y z. - split. + use total2_paths_b. * exact (pr1 (associatorlaw_iso_law (monoidal_associatorlaw M) (pr1 x) (pr1 y) (pr1 z))). * exact (pr2 ((dαiso) (pr1 x) (pr1 y) (pr1 z) (pr2 x) (pr2 y) (pr2 z))). + use total2_paths_b. * exact (pr2 (associatorlaw_iso_law (monoidal_associatorlaw M) (pr1 x) (pr1 y) (pr1 z))). * exact (pr1 ((dαiso) (pr1 x) (pr1 y) (pr1 z) (pr2 x) (pr2 y) (pr2 z))). 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.