Definition skewmonoidal_pentagon_eq (V : skewmonoidal_category) : ∏ (a b c d : V), α' (a ⊗ b) c d · α' a b (c ⊗ d) = α' a b c #⊗ id d · α' a (b ⊗ c) d · id a #⊗ α' b c d := (pr2 (pr2 (pr2 (pr2 eq)))).
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.