fact: Definition displayedassociator_data (dtd : displayedtensor_data) : UU := ∏ (x y z : C), ∏ (a : D x) (b : D y) (c : D z), ((a ⊗_{{dtd}} b) ⊗_{{dtd}} c) -->[(α x y z)] (a ⊗_{{dtd}} (b ⊗_{{dtd}} c)).
imports: UniMath.Foundations.All UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesCurried UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Isos