open import NeilPrelude1

-- The Ordered Universe

module Ord1 where

infix    _≤_ _≥_ 

infix    _<=_ _<_ _>=_ _>_


-- Ordered Universe --

data OrdU : Set where
  bool : OrdU
  nat  : OrdU

ordSet : OrdU → Set
ordSet bool = Bool
ordSet nat  = ℕ

_<=_ : {t : OrdU} → ordSet t → ordSet t → Bool

_<=_ {bool} false _ = true
_<=_ {bool} true b = b

_<=_ {nat} O _ = true
_<=_ {nat} (S _) O = false
_<=_ {nat} (S m) (S n) = m <= n


_>=_ : {t : OrdU} → ordSet t → ordSet t → Bool
x >= y = y <= x

_>_ : {t : OrdU} → ordSet t → ordSet t → Bool
x > y = not (x <= y)

_<_ : {t : OrdU} → ordSet t → ordSet t → Bool
x < y = not (x >= y)


------------------------------------------------

data _≤_ : {u : OrdU} → ordSet u → ordSet u → Set where
  refl : {b : Bool}         -> b ≤ b
  f≤t  :                       false ≤ true
  ≤O   : {n : ℕ}            -> O ≤ n
  ≤S   : {m n : ℕ} -> m ≤ n -> S m ≤ S n
  

_≥_ : {u : OrdU} → ordSet u → ordSet u → Set
a ≥ b = b ≤ a