let kCat = ../Category/Cat/semigroupal

let vObject = Type

let object = Type

let cat =
      ../Category/Monoidal/Cartesian/extractMonoidal
        kCat
        vObject
        object
        ../Category/Set/monoidal/cartesian

in  λ(m : object) →
    λ(eq : ../Eq/Type m) →
    λ(monoid : ./Type object cat m) →
        { leftIdentity =
            λ(a : m) → eq.eq (monoid.product { _1 = monoid.unit {=}, _2 = a }) a
        , rightIdentity =
            λ(a : m) → eq.eq (monoid.product { _1 = a, _2 = monoid.unit {=} }) a
        }
      ∧ ../Semigroup/laws m eq (./extractSemigroup object cat m monoid)