let cat = ../../Category/Cat/semigroupal

let vObject = Type

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

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