fact: Definition displayedleftunitor_data (dtd : displayedtensor_data) (i : D I) : UU := ∏ (x : C), ∏ (a : D x), ((i ⊗_{{dtd}} a)-->[(lu x)] a).
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