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