{-|
This is the weakest form of order provided. There is no standalone preorder,
partial order, or anything, because there are too many possible instances. For
the general case, just define regular functions. A `Group/PartiallyOrdered`
constrains the instances enough for a generic “less than” to be meaningful.
-}
let cat = ../../Category/Cat/semigroupal

let vObject = Type

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

in  λ(m : Type) → { le : m → m → Bool } ⩓ ../../Eq/Type m ⩓ ../Type Type Set m