fact: Definition displayedrightunitor_is_nat_iso {i : D I} {dtd : displayedtensor_data} (dru : displayedrightunitor_data dtd i) : UU := ∏ (x : C), ∏ (a : D x), is_z_iso_disp (ru x,, ruiso x) (dru 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