fact: Definition displayedtensor_id (dtd : displayedtensor_data) := ∏ (x y : C), ∏ (a : D x) (b : D y), ((id_disp a) ⊗^{{dtd}} (id_disp b)) = transportb _ (tid x y) (id_disp (a ⊗_{{dtd}} b)).
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