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