Definition laxassociator {C : category} (tu : tensor_unit C) : UU := ∑ α : associator_data tu, (associator_nat_leftwhisker α) × (associator_nat_rightwhisker α) × (associator_nat_leftrightwhisker α).
Require Import UniMath.Foundations.All. Require Import UniMath.MoreFoundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Monoidal.WhiskeredBifunctors. Require Import UniMath.CategoryTheory.Monoidal.Categories.