Definition pentagon_eq (α' : associator) : UU := ∏ (a b c d : C), pr1 α' ((a ⊗ b, c), d) · pr1 α' ((a, b), c ⊗ d) = pr1 α' ((a, b), c) #⊗ id d · pr1 α' ((a, b ⊗ c), d) · id a #⊗ pr1 α' ((b, c), d).
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.ProductCategory. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.whiskering.