Definition preserves_associativity (tpd : tensor_preserving_data) := ∏ (x y z : C), (#F (α^{M}_{x,y,z})) ∘ (tpd (x ⊗_{M} y) z) ∘ ((tpd x y) ⊗^{N} (identity (F z))) = (tpd x (y ⊗_{M} z)) ∘ ((identity (F x)) ⊗^{N} (tpd y z)) ∘ α^{N}_{F x, F y, F z}.
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.Isos. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesCurried.