Definition preserves_associator {C D : category} {F : functor C D} {tuC : tensor_unit C} {tuD : tensor_unit D} (ptuF : functor_tensor_unit tuC tuD F) (αC : associator tuC) (αD : associator tuD) : UU := ∏ (x y z : C), ((pr1 pt_{ptuF} x y) ⊗^{tuD} (identity (F z))) · (pr1 pt_{ptuF} (x ⊗_{tuC} y) z) · (functor_on_morphisms F (pr1 αC x y z)) = (pr1 αD (F x) (F y) (F z)) · ((identity (F x)) ⊗^{tuD} (pr1 pt_{ptuF} y z)) · (pr1 pt_{ptuF} x (y ⊗_{tuC} 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.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Isos. Import TensorNotation. Import TensorUnitNotation. Import TensorNotation. Import TensorUnitNotation. Import TensorNotation. Import TensorUnitNotation. Import TensorNotation. Import TensorUnitNotation. Import UnitorsAssociatorNotation. Import TensorNotation. Import TensorUnitNotation. Import UnitorsAssociatorNotation.