Expand definition of Sort.

1 files changed, 63 insertions, 12 deletions

diff --git a/src/Obs/Sort.idr b/src/Obs/Sort.idr
index f76453a..4e0e9c9 100644
--- a/src/Obs/Sort.idr
+++ b/src/Obs/Sort.idr
@@ -1,5 +1,11 @@
 module Obs.Sort
 
+import Data.Bool
+import Data.Nat
+import Data.So
+
+import Decidable.Equality
+
 import Text.PrettyPrint.Prettyprinter
 
 %default total
@@ -13,14 +19,47 @@ data Sort : Type where
 
 %name Sort s, s', s'', s'''
 
+public export
+toNat : Sort -> Nat
+toNat Prop = 0
+toNat (Set i) = S i
+
 -- Interfaces ------------------------------------------------------------------
 
-export
+public export
 Eq Sort where
   Prop    == Prop    = True
   (Set i) == (Set j) = i == j
   _       == _       = False
 
+public export
+Ord Sort where
+  compare = compare `on` toNat
+
+  min Prop s' = Prop
+  min (Set _) Prop = Prop
+  min (Set i) (Set j) = Set (minimum i j)
+
+  max Prop s' = s'
+  max (Set i) s' = Set (maximum i (pred $ toNat s'))
+
+export
+Uninhabited (Prop = Set i) where uninhabited Refl impossible
+
+export
+Uninhabited (Set i = Prop) where uninhabited Refl impossible
+
+export
+Injective Set where
+  injective Refl = Refl
+
+public export
+DecEq Sort where
+  decEq Prop Prop = Yes Refl
+  decEq Prop (Set _) = No absurd
+  decEq (Set _) Prop = No absurd
+  decEq (Set i) (Set j) = decEqCong $ decEq i j
+
 export
 Show Sort where
   show Prop        = "Prop"
@@ -38,22 +77,34 @@ Pretty Sort where
 infixr 5 ~>
 
 public export
-suc : Sort -> Sort
-suc Prop    = Set 0
-suc (Set i) = Set (S i)
+isSet : Sort -> Bool
+isSet = (> 0) . toNat
 
 public export
-ensureSet : Sort -> Sort
-ensureSet Prop    = Set 0
-ensureSet (Set i) = Set i
+suc : Sort -> Sort
+suc = Set . toNat
 
 public export
-lub : Sort -> Sort -> Sort
-lub Prop    s'      = s'
-lub (Set i) Prop    = Set i
-lub (Set i) (Set j) = Set (max i j)
+ensureSet : Sort -> Sort
+ensureSet = max (Set 0)
 
 public export
 (~>) : Sort -> Sort -> Sort
 s ~> Prop    = Prop
-s ~> (Set k) = lub s (Set k)
+s ~> (Set k) = max (Set k) s
+
+-- Properties ------------------------------------------------------------------
+
+export
+maxIsSet : (s, s' : Sort) -> isSet (max s s') = isSet s || isSet s'
+maxIsSet Prop s = Refl
+maxIsSet (Set _) s = Refl
+
+export
+impredicative : (s, s' : Sort) -> isSet (s ~> s') = isSet s'
+impredicative s Prop = Refl
+impredicative s (Set i) = Refl
+
+export
+ensureSetIsSet : (s : Sort) -> So (isSet (ensureSet s))
+ensureSetIsSet s = Oh