proposition: Lemma totalcategory_associatornaturality : associator_naturality TαD.
proof: Proof. intros x x' y y' z z' f g h. use total2_paths_b. - exact (αnat (pr1 x) (pr1 x') (pr1 y) (pr1 y') (pr1 z) (pr1 z') (pr1 f) (pr1 g) (pr1 h)). - exact (dαnat (pr1 x) (pr1 x') (pr1 y) (pr1 y') (pr1 z) (pr1 z') (pr2 x) (pr2 x') (pr2 y) (pr2 y') (pr2 z) (pr2 z') (pr1 f) (pr1 g) (pr1 h) (pr2 f) (pr2 g) (pr2 h)). Qed.
imports: UniMath.Foundations.All UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesCurried UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.DisplayedMonoidalCurried UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalFunctorsCurried UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Total