Definition skewmonoidal_assoc_ax (V : skewmonoidal_data) {x x' y y' z z' : V} (f : x --> x')(g : y --> y')(h : z --> z') : ((f #⊗ g) #⊗ h) · α' x' y' z' = α' x y z · (f #⊗ (g #⊗ h)) := nat_trans_ax (skewmonoidal_assoc_nt V) _ _ ((f #, g) #, h).
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.