Definition displayedleftunitor_is_nat_iso {i : D I} {dtd : displayedtensor_data} (dlu : displayedleftunitor_data dtd i) : UU := ∏ (x : C), ∏ (a : D x), is_z_iso_disp (lu x,, luiso x) (dlu x a).
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Monoidal.AlternativeDefinitions.MonoidalCategoriesCurried. Require Import UniMath.CategoryTheory.DisplayedCats.Core. Require Import UniMath.CategoryTheory.DisplayedCats.Functors. Require Import UniMath.CategoryTheory.DisplayedCats.Constructions. Require Import UniMath.CategoryTheory.DisplayedCats.Isos.