Lemma total_pentagonidentity {C : category} {D : disp_cat C} {M : monoidal C} {DM : disp_monoidal_data D M} (dpi : disp_pentagon_identity dα^{DM}) : pentagon_identity (total_associatordata dα^{DM}). Proof. intros w x y z. use total2_paths_b. - exact ((monoidal_pentagonidentity M) (pr1 w) (pr1 x) (pr1 y) (pr1 z)). - exact (dpi (pr1 w) (pr1 x) (pr1 y) (pr1 z) (pr2 w) (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.