Definition skewMonoid_Mor_laws {T T' : skewMonoid_data} (α : V ⟦T , T'⟧) : UU := (μ T · α = α #⊗ α · μ T') × η T · α = η T'.
Require Import UniMath.Foundations.PartD. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Functors. Require Import UniMath.CategoryTheory.Core.NaturalTransformations. Require Import UniMath.CategoryTheory.PrecategoryBinProduct. Require Import UniMath.CategoryTheory.SkewMonoidal.SkewMonoidalCategories.