{-|
A commutative monoid implies a preorder. Technically, a preorder could be
defined with `≤` where both `x ≤ y` and `y ≤ x` may be false. However, with
structural typing it makes it impossible to distinguish a preordered structure
from a totally-ordered structure.
-}
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) → { le : m → m → Bool } ⩓ ./Type object cat m