Definition pentagon_identity {C : category} {T : tensor_data C} (α : associator_data T) : UU := ∏ (w x y z : C), ((identity w)⊗^{T} (α x y z)) ∘ ((α w (x⊗_{T} y) z) ∘ ((α w x y) ⊗^{T} (identity z))) = (α w x (y⊗_{T} z)) ∘ (α (w⊗_{T}x) y z).
Require Import UniMath.Foundations.All. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.Isos.