Define sorts.

1 files changed, 44 insertions, 0 deletions

diff --git a/src/Obs/Sort.idr b/src/Obs/Sort.idr
new file mode 100644
index 0000000..16eaa96
--- /dev/null
+++ b/src/Obs/Sort.idr
@@ -0,0 +1,44 @@
+module Obs.Sort
+
+-- Definition ------------------------------------------------------------------
+
+public export
+data Sort : Type where
+  Prop : Sort
+  Set  : Nat -> Sort
+
+%name Sort s, s', s'', s'''
+
+-- Interfaces ------------------------------------------------------------------
+
+export
+Eq Sort where
+  Prop    == Prop    = True
+  (Set i) == (Set j) = True
+  _       == _       = False
+
+export
+Show Sort where
+  show Prop        = "Prop"
+  show (Set 0)     = "Set"
+  show (Set (S i)) = "Set \{show (S i)}"
+
+-- Operations ------------------------------------------------------------------
+
+infix 5 ~>
+
+public export
+suc : Sort -> Sort
+suc Prop    = Set 0
+suc (Set i) = Set (S i)
+
+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)
+
+public export
+(~>) : Sort -> Sort -> Sort
+s ~> Prop    = Prop
+s ~> (Set k) = lub s (Set k)