1 files changed, 0 insertions, 110 deletions
diff --git a/src/Obs/Sort.idr b/src/Obs/Sort.idr
deleted file mode 100644
index 4e0e9c9..0000000
--- a/src/Obs/Sort.idr
+++ /dev/null
@@ -1,110 +0,0 @@
-module Obs.Sort
-
-import Data.Bool
-import Data.Nat
-import Data.So
-
-import Decidable.Equality
-
-import Text.PrettyPrint.Prettyprinter
-
-%default total
-
--- Definition ------------------------------------------------------------------
-
-public export
-data Sort : Type where
-  Prop : Sort
-  Set  : Nat -> Sort
-
-%name Sort s, s', s'', s'''
-
-public export
-toNat : Sort -> Nat
-toNat Prop = 0
-toNat (Set i) = S i
-
--- Interfaces ------------------------------------------------------------------
-
-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"
-  show (Set 0)     = "Set"
-  show (Set (S i)) = "Set \{show (S i)}"
-
-export
-Pretty Sort where
-  prettyPrec d Prop        = pretty "Prop"
-  prettyPrec d (Set 0)     = pretty "Set"
-  prettyPrec d (Set (S i)) = parenthesise (d >= App) $ pretty "Set \{show (S i)}"
-
--- Operations ------------------------------------------------------------------
-
-infixr 5 ~>
-
-public export
-isSet : Sort -> Bool
-isSet = (> 0) . toNat
-
-public export
-suc : Sort -> Sort
-suc = Set . toNat
-
-public export
-ensureSet : Sort -> Sort
-ensureSet = max (Set 0)
-
-public export
-(~>) : Sort -> Sort -> Sort
-s ~> Prop    = Prop
-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