Definition skewmonoidal_category : UU := ∑ (V : skewmonoidal_data), ρ' I · λ' I = identity (C := V) I × (∏ (a b : V), ρ' a #⊗ id b · α' a I b · id a #⊗ λ' b = id (a ⊗ b)) × (∏ (a b : V), α' I a b · λ' (a ⊗ b) = λ' a #⊗ id b) × (∏ (a b : V), ρ' (a⊗b) · α' a b I = id a #⊗ ρ' b) × (∏ (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).
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.