Add more program structure to type universes.

1 files changed, 222 insertions, 0 deletions

diff --git a/src/Obs/Universe.idr b/src/Obs/Universe.idr
new file mode 100644
index 0000000..1517c4c
--- /dev/null
+++ b/src/Obs/Universe.idr
@@ -0,0 +1,222 @@
+||| Provides definitions of proof-relevance and type universes.
+module Obs.Universe
+
+import Data.Bool
+import Data.Bool.Decidable
+import Data.Nat
+import Data.Nat.Order.Properties
+import Data.So
+
+import Decidable.Equality
+
+import Text.PrettyPrint.Prettyprinter
+
+%default total
+
+-- Definition ------------------------------------------------------------------
+
+||| Proof relevance of terms
+public export
+data Relevance = Irrelevant | Relevant
+
+%name Relevance r, r'
+
+||| Type universes.
+public export
+data Universe : Type where
+  ||| Impredicative universe of strict propositions.
+  Prop : Universe
+  ||| Predicative hierarchy of universes.
+  Set  : Nat -> Universe
+
+%name Universe s, s', s'', s'''
+
+||| Converts universes to naturals as a helper for writing implementations.
+public export
+toNat : Universe -> Nat
+toNat Prop = 0
+toNat (Set i) = S i
+
+-- Interfaces ------------------------------------------------------------------
+
+public export
+Eq Relevance where
+  Irrelevant == Irrelevant = True
+  Relevant == Relevant = True
+  _ == _ = False
+
+export
+Uninhabited (Irrelevant = Relevant) where uninhabited Refl impossible
+
+export
+Uninhabited (Relevant = Irrelevant) where uninhabited Refl impossible
+
+export
+DecEq Relevance where
+  decEq Irrelevant Irrelevant = Yes Refl
+  decEq Irrelevant Relevant = No absurd
+  decEq Relevant Irrelevant = No absurd
+  decEq Relevant Relevant = Yes Refl
+
+public export
+Eq Universe where
+  (==) = (==) `on` toNat
+
+public export
+Ord Universe where
+  compare = compare `on` toNat
+  (<) = lt `on` toNat
+  (>) = gt `on` toNat
+  (<=) = lte `on` toNat
+  (>=) = gte `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 Universe 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 Universe where
+  showPrec d Prop = "Prop"
+  showPrec d (Set 0) = "Set"
+  showPrec d (Set (S i)) = showParens (d >= App) $ "Set \{show (S i)}"
+
+export
+Pretty Universe 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 ~>
+
+||| Computes the proof-relevance of a pair.
+public export
+pair : (fst, snd : Relevance) -> Relevance
+pair Irrelevant = id
+pair Relevant = const Relevant
+
+||| Computes the proof-relevance of a function.
+public export
+function : (dom, cod : Relevance) -> Relevance
+function = const id
+
+||| Gets the proof-relevance of values in a universe.
+public export
+relevance : Universe -> Relevance
+relevance Prop = Irrelevant
+relevance (Set k) = Relevant
+
+||| True if values in `s` are proof-irrelevant.
+public export
+isIrrelevant : (s : Universe) -> Bool
+isIrrelevant = (Irrelevant ==) . relevance
+
+||| True if values in `s` are proof-relevant.
+public export
+isRelevant : (s : Universe) -> Bool
+isRelevant = (Relevant ==) . relevance
+
+||| Returns the smallest universe containing `s`
+||| @ s the universe to contain
+public export
+succ : (s : Universe) -> Universe
+succ = Set . toNat
+
+||| The universe of a dependent product.
+||| @ dom the domain universe
+||| @ cod the codomain universe
+public export
+(~>) : (dom, cod : Universe) -> Universe
+dom ~> Prop    = Prop
+dom ~> (Set k) = max (Set k) dom
+
+-- Views -----------------------------------------------------------------------
+
+namespace Predicates
+  public export
+  data IsIrrelevant : Universe -> Type where
+    Prop : IsIrrelevant Prop
+
+  public export
+  data IsRelevant : Universe -> Type where
+    Set : IsRelevant (Set k)
+
+  export
+  Uninhabited (IsIrrelevant (Set k)) where
+    uninhabited _ impossible
+
+  export
+  Uninhabited (IsRelevant Prop) where
+    uninhabited _ impossible
+
+  export
+  isIrrelevant : (s : Universe) -> Dec (IsIrrelevant s)
+  isIrrelevant Prop = Yes Prop
+  isIrrelevant (Set k) = No absurd
+
+  export
+  isRelevant : (s : Universe) -> Dec (IsRelevant s)
+  isRelevant Prop = No absurd
+  isRelevant (Set k) = Yes Set
+
+-- Properties ------------------------------------------------------------------
+
+export
+pairRelevantRight : (fst : Relevance) -> pair fst Relevant = Relevant
+pairRelevantRight Irrelevant = Refl
+pairRelevantRight Relevant = Refl
+
+succContains : (s : Universe) -> So (s < succ s)
+succContains Prop = Oh
+succContains (Set k) = eqToSo $ LteIslte k k reflexive
+
+succLeast : (s, s' : Universe) -> So (s < s') -> So (succ s <= s')
+succLeast s s' prf = prf
+
+irrelevantReflection : (s : Universe) -> Reflects (IsIrrelevant s) (isIrrelevant s)
+irrelevantReflection Prop = RTrue Prop
+irrelevantReflection (Set k) = RFalse absurd
+
+relevantReflection : (s : Universe) -> Reflects (IsRelevant s) (isRelevant s)
+relevantReflection Prop = RFalse absurd
+relevantReflection (Set k) = RTrue Set
+
+export
+forgetIsIrrelevant : IsIrrelevant s -> relevance s = Irrelevant
+forgetIsIrrelevant Prop = Refl
+
+export
+forgetIsRelevant : IsRelevant s -> relevance s = Relevant
+forgetIsRelevant Set = Refl
+
+export
+pairRelevance : (s, s' : Universe) -> relevance (max s s') = pair (relevance s) (relevance s')
+pairRelevance Prop s' = Refl
+pairRelevance (Set k) s' = Refl
+
+export
+functionRelevance : (s, s' : Universe) ->
+  relevance (s ~> s') = function (relevance s) (relevance s')
+functionRelevance s Prop = Refl
+functionRelevance s (Set k) = Refl