Definition displayedtriangle_identity {dtd : displayedtensor_data} {i : D I} (dlud : displayedleftunitor_data dtd i) (drud : displayedrightunitor_data dtd i) (dα : displayedassociator_data dtd) := ∏ (x y : C), ∏ (a : D x) (b : D y), ((dα x I y a i b) ;; ((id_disp a) ⊗^{{dtd}} dlud y b )) = transportb _ (tri x y) ((drud x a) ⊗^{{dtd}} id_disp b).
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.