Add more program structure to type universes.

12 files changed, 521 insertions, 402 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index b32af2d..a9ef411 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -25,7 +25,7 @@ abstractSyntax ctx (Var var) = do
   let Just i = lookup var ctx
     | Nothing => inScope "unbound variable" $ fatal var
   pure (Var var i)
-abstractSyntax ctx (Sort s) = pure (Sort s)
+abstractSyntax ctx (Universe s) = pure (Universe s)
 abstractSyntax ctx (Pi var a b) = do
   a <- abstractSyntaxBounds ctx a
   b <- abstractSyntaxBounds (bind ctx var.val) b
diff --git a/src/Obs/Main.idr b/src/Obs/Main.idr
index 4d7c856..7162a20 100644
--- a/src/Obs/Main.idr
+++ b/src/Obs/Main.idr
@@ -9,6 +9,7 @@ import Obs.Parser
 import Obs.Syntax
 import Obs.Term
 import Obs.Typing
+import Obs.Universe
 
 import System
 import System.File
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index a756728..d660111 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -1,10 +1,9 @@
 module Obs.NormalForm
 
 import Data.List.Elem
-import Data.So
 
-import Obs.Sort
 import Obs.Substitution
+import Obs.Universe
 
 import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
@@ -13,29 +12,33 @@ import Text.PrettyPrint.Prettyprinter
 
 -- Definition ------------------------------------------------------------------
 
-data NormalForm  : Sorted.Family Bool
+data NormalForm  : Sorted.Family Relevance
 
 public export
-data Constructor : Unsorted.Family Bool where
-  Sort : (s : Sort) -> Constructor ctx
-  Pi : (s, s' : Sort)
+TypeNormalForm : Unsorted.Family Relevance
+TypeNormalForm = NormalForm Relevant
+
+public export
+data Constructor : Unsorted.Family Relevance where
+  Universe : (s : Universe) -> Constructor ctx
+  Pi : (s, s' : Universe)
     -> (var : String)
-    -> (a : NormalForm True ctx)
-    -> (b : NormalForm True (isSet s :: ctx))
+    -> (a : TypeNormalForm ctx)
+    -> (b : TypeNormalForm (relevance s :: ctx))
     -> Constructor ctx
-  Lambda : (s : Sort)
+  Lambda : (s : Universe)
     -> (var : String)
-    -> NormalForm True (isSet s :: ctx)
+    -> NormalForm Relevant (relevance s :: ctx)
     -> Constructor ctx
-  Sigma : (s, s' : Sort)
+  Sigma : (s, s' : Universe)
     -> (var : String)
-    -> (a : NormalForm True ctx)
-    -> (b : NormalForm True (isSet s :: ctx))
+    -> (a : TypeNormalForm ctx)
+    -> (b : TypeNormalForm (relevance s :: ctx))
     -> Constructor ctx
-  Pair : (s, s' : Sort)
-    -> (prf : So (isSet (max s s')))
-    -> NormalForm (isSet s) ctx
-    -> NormalForm (isSet s') ctx
+  Pair : (s, s' : Universe)
+    -> (prf : IsRelevant (max s s'))
+    -> NormalForm (relevance s) ctx
+    -> NormalForm (relevance s') ctx
     -> Constructor ctx
   Bool : Constructor ctx
   True : Constructor ctx
@@ -44,61 +47,61 @@ data Constructor : Unsorted.Family Bool where
   Bottom : Constructor ctx
 
 public export
-data Neutral : Unsorted.Family Bool where
+data Neutral : Unsorted.Family Relevance where
   Var : (var : String)
-    -> (sort : Sort)
-    -> (prf : So (isSet sort))
-    -> (i : Elem True ctx)
+    -> (sort : Universe)
+    -> (prf : IsRelevant sort)
+    -> (i : Elem Relevant ctx)
     -> Neutral ctx
-  App : (b : Bool) -> Neutral ctx -> NormalForm b ctx -> Neutral ctx
-  Fst : (b : Bool) -> Neutral ctx -> Neutral ctx
-  Snd : (b : Bool) -> Neutral ctx -> Neutral ctx
-  If : Neutral ctx -> (f, g : NormalForm True ctx) -> Neutral ctx
+  App : (r : Relevance) -> Neutral ctx -> NormalForm r ctx -> Neutral ctx
+  Fst : (r : Relevance) -> Neutral ctx -> Neutral ctx
+  Snd : (r : Relevance) -> Neutral ctx -> Neutral ctx
+  If : Neutral ctx -> (f, g : NormalForm Relevant ctx) -> Neutral ctx
   Absurd : Neutral ctx
-  Equal : Neutral ctx -> NormalForm True ctx -> NormalForm True ctx -> Neutral ctx
-  EqualL : (a : Neutral ctx) -> (b : NormalForm True ctx) -> Neutral ctx
+  Equal : Neutral ctx -> NormalForm Relevant ctx -> NormalForm Relevant ctx -> Neutral ctx
+  EqualL : (a : Neutral ctx) -> (b : TypeNormalForm ctx) -> Neutral ctx
   EqualR : (a : Constructor ctx) -> (b : Neutral ctx) -> Neutral ctx
   EqualStuck : (a, b : Constructor ctx) -> Neutral ctx
   CastL : (a : Neutral ctx) ->
-    (b : NormalForm True ctx) ->
-    NormalForm True ctx ->
+    (b : TypeNormalForm ctx) ->
+    NormalForm Relevant ctx ->
     Neutral ctx
-  CastR : (a : Constructor ctx) -> (b : Neutral ctx) -> NormalForm True ctx -> Neutral ctx
-  CastStuck : (a, b : Constructor ctx) -> NormalForm True ctx -> Neutral ctx
+  CastR : (a : Constructor ctx) -> (b : Neutral ctx) -> NormalForm Relevant ctx -> Neutral ctx
+  CastStuck : (a, b : Constructor ctx) -> NormalForm Relevant ctx -> Neutral ctx
 
 public export
-data NormalForm : Sorted.Family Bool where
-  Ntrl : Neutral ~|> NormalForm True
-  Cnstr : Constructor ~|> NormalForm True
-  Irrel : NormalForm False ctx
+data NormalForm : Sorted.Family Relevance where
+  Ntrl : Neutral ~|> NormalForm Relevant
+  Cnstr : Constructor ~|> NormalForm Relevant
+  Irrel : NormalForm Irrelevant ctx
 
 %name Constructor t, u, v
 %name Neutral t, u, v
 %name NormalForm t, u, v
 
 public export
-record Definition (ctx : List Bool) where
+record Definition (ctx : List Relevance) where
   constructor MkDefinition
   name : WithBounds String
-  sort : Sort
-  ty   : NormalForm True ctx
-  tm   : NormalForm (isSet sort) ctx
+  sort : Universe
+  ty   : TypeNormalForm ctx
+  tm   : NormalForm (relevance sort) ctx
 
 public export
-data Context : List Bool -> Type where
+data Context : List Relevance -> Type where
   Nil  : Context []
-  (:<) : Context ctx -> (def : Definition ctx) -> Context (isSet def.sort :: ctx)
+  (:<) : Context ctx -> (def : Definition ctx) -> Context (relevance def.sort :: ctx)
 
 %name Context ctx, ctx', ctx''
 
 -- Convenience Casts -----------------------------------------------------------
 
 public export
-Cast Sort (Constructor ctx) where
-  cast s = Sort s
+Cast Universe (Constructor ctx) where
+  cast s = Universe s
 
 public export
-Cast Sort (NormalForm True ctx) where
+Cast Universe (NormalForm Relevant ctx) where
   cast s = Cnstr $ cast s
 
 -- Pretty Print ----------------------------------------------------------------
@@ -106,7 +109,7 @@ Cast Sort (NormalForm True ctx) where
 prettyPrec : Prec -> NormalForm b ctx -> Doc ann
 
 prettyPrecCnstr : Prec -> Constructor ctx -> Doc ann
-prettyPrecCnstr d (Sort s) = prettyPrec d s
+prettyPrecCnstr d (Universe s) = prettyPrec d s
 prettyPrecCnstr d (Pi s s' var a b) =
   let lhs = case var of
               "" => align (prettyPrec App a)
@@ -208,7 +211,7 @@ Pretty (NormalForm b ctx) where
 rename : NormalForm ~|> Hom Elem NormalForm
 
 renameCnstr : Constructor ~|> Hom Elem Constructor
-renameCnstr (Sort s) f = Sort s
+renameCnstr (Universe s) f = Universe s
 renameCnstr (Pi s s' var a b) f = Pi s s' var (rename a f) (rename b (lift [(_ ** ())] f))
 renameCnstr (Lambda s var t) f = Lambda s var (rename t (lift [(_ ** ())] f))
 renameCnstr (Sigma s s' var a b) f =
@@ -240,18 +243,18 @@ rename (Cnstr t) f = Cnstr $ renameCnstr t f
 rename Irrel f = Irrel
 
 export
-Unsorted.Rename Bool Constructor where
+Unsorted.Rename Relevance Constructor where
   rename = renameCnstr
 
 export
-Unsorted.Rename Bool Neutral where
+Unsorted.Rename Relevance Neutral where
   rename = renameNtrl
   
 export
-Sorted.Rename Bool NormalForm where
+Sorted.Rename Relevance NormalForm where
   rename = NormalForm.rename
 
 export
-PointedRename Bool (\b => (String, (s : Sort ** isSet s = b))) NormalForm where
-  point {s = False} _ _ = Irrel
-  point {s = True} (var, (s ** prf)) i = Ntrl (Var var s (eqToSo prf) i)
+PointedRename Relevance (\r => (String, (s : Universe ** relevance s = r))) NormalForm where
+  point {s = Irrelevant} _ _ = Irrel
+  point {s = Relevant} (var, (s@(Set _) ** prf)) i = Ntrl (Var var s Set i)
diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr
index 82e84b9..ed06fa2 100644
--- a/src/Obs/NormalForm/Normalise.idr
+++ b/src/Obs/NormalForm/Normalise.idr
@@ -1,14 +1,14 @@
 module Obs.NormalForm.Normalise
 
 import Data.Bool
-import Data.So
+import Data.Nat
 
 import Decidable.Equality
 
 import Obs.Logging
 import Obs.NormalForm
-import Obs.Sort
 import Obs.Substitution
+import Obs.Universe
 
 import Text.PrettyPrint.Prettyprinter
 
@@ -17,19 +17,19 @@ import Text.PrettyPrint.Prettyprinter
 -- Aliases ---------------------------------------------------------------------
 
 public export 0
-LogConstructor : Type -> Unsorted.Family Bool
+LogConstructor : Type -> Unsorted.Family Relevance
 LogConstructor ann ctx = Logging ann (Constructor ctx)
 
 public export 0
-LogNormalForm : Type -> Sorted.Family Bool
+LogNormalForm : Type -> Sorted.Family Relevance
 LogNormalForm ann b ctx = Logging ann (NormalForm b ctx)
 
 0
-LogNormalForm' : Type -> Sorted.Family Bool
+LogNormalForm' : Type -> Sorted.Family Relevance
 LogNormalForm' ann b ctx = Either (Logging ann (NormalForm b ctx)) (Elem b ctx)
 
 -- Copied and specialised from Obs.Substitution
-lift : (ctx : List (b ** (String, (s ** isSet s = b))))
+lift : (ctx : List (r ** (String, (s ** relevance s = r))))
   -> Map ctx' (LogNormalForm' ann) ctx''
   -> Map (map DPair.fst ctx ++ ctx') (LogNormalForm' ann) (map DPair.fst ctx ++ ctx'')
 lift [] f = f
@@ -42,184 +42,187 @@ lift ((s ** y) :: ctx) f = add (LogNormalForm' ann)
 subst' : NormalForm ~|> Hom (LogNormalForm' ann) (LogNormalForm ann)
 
 export
-doApp : {b' : _} -> NormalForm b ctx -> NormalForm b' ctx -> LogNormalForm ann b ctx
+doApp : {domain : _} ->
+  NormalForm (function domain codomain) ctx ->
+  NormalForm domain ctx ->
+  LogNormalForm ann codomain ctx
 doApp (Ntrl t) u = pure (Ntrl $ App _ t u)
 doApp (Cnstr (Lambda s var t)) u = inScope "doApp" $ do
   trace $ pretty {ann} "substituting" <++> pretty u <+> softline <+> pretty "for \{var} in" <++> pretty t
-  let Yes Refl = decEq b' (isSet s)
-    | No _ => fatal "internal sort mismatch"
+  let Yes Refl = decEq domain (relevance s)
+    | No _ => fatal "internal relevance mismatch"
   subst' t (add (LogNormalForm' ann) (Left $ pure u) Right)
 doApp (Cnstr t) u = inScope "wrong constructor for apply" $ fatal t
 doApp Irrel u = pure Irrel
 
 export
-doFst : (b, b' : _) -> NormalForm (b || b') ctx -> LogNormalForm ann b ctx
-doFst False b' t = pure Irrel
-doFst True b' (Ntrl t) = pure (Ntrl $ Fst b' t)
-doFst True b' (Cnstr (Pair (Set _) s' prf t u)) = pure t
-doFst True b' (Cnstr t) = inScope "wrong constructor for fst" $ fatal t
+doFst : (fst, snd : _) -> NormalForm (pair fst snd) ctx -> LogNormalForm ann fst ctx
+doFst Irrelevant snd t = pure Irrel
+doFst Relevant snd (Ntrl t) = pure (Ntrl $ Fst snd t)
+doFst Relevant snd (Cnstr (Pair (Set _) s' prf t u)) = pure t
+doFst Relevant snd (Cnstr t) = inScope "wrong constructor for fst" $ fatal t
 
 export
-doSnd : (b, b' : _) -> NormalForm (b || b') ctx -> LogNormalForm ann b' ctx
-doSnd b False t = pure Irrel
-doSnd b True t =
-  let t' : NormalForm True ctx
-      t' = rewrite sym $ orTrueTrue b in t
+doSnd : (fst, snd : _) -> NormalForm (pair fst snd) ctx -> LogNormalForm ann snd ctx
+doSnd fst Irrelevant t = pure Irrel
+doSnd fst Relevant t =
+  let t' : NormalForm Relevant ctx
+      t' = rewrite sym $ pairRelevantRight fst in t
   in case t' of
-  Ntrl t => pure (Ntrl $ Snd b t)
+  Ntrl t => pure (Ntrl $ Snd fst t)
   Cnstr (Pair _ (Set _) prf t u) => pure u
   Cnstr t => inScope "wrong constructor for snd" $ fatal t
 
 export
-doIf : {b : _} ->
-  NormalForm True ctx ->
-  NormalForm b ctx ->
-  NormalForm b ctx ->
-  LogNormalForm ann b ctx
-doIf {b = False} t u v = pure Irrel
-doIf {b = True} (Ntrl t) u v = pure (Ntrl $ If t u v)
-doIf {b = True} (Cnstr True) u v = pure u
-doIf {b = True} (Cnstr False) u v = pure v
-doIf {b = True} (Cnstr t) u v = inScope "wrong constructor for case" $ fatal t
+doIf : {r : _} ->
+  NormalForm Relevant ctx ->
+  NormalForm r ctx ->
+  NormalForm r ctx ->
+  LogNormalForm ann r ctx
+doIf {r = Irrelevant} t u v = pure Irrel
+doIf {r = Relevant} (Ntrl t) u v = pure (Ntrl $ If t u v)
+doIf {r = Relevant} (Cnstr True) u v = pure u
+doIf {r = Relevant} (Cnstr False) u v = pure v
+doIf {r = Relevant} (Cnstr t) u v = inScope "wrong constructor for case" $ fatal t
 
 export
-doAbsurd : (b : _) -> NormalForm b ctx
-doAbsurd False = Irrel
-doAbsurd True = Ntrl Absurd
+doAbsurd : (r : _) -> NormalForm r ctx
+doAbsurd Irrelevant = Irrel
+doAbsurd Relevant = Ntrl Absurd
 
 export
-doCast : (b' : _) -> (a, b : NormalForm True ctx) -> NormalForm b' ctx -> LogNormalForm ann b' ctx
+doCast : (r : _) -> (a, b : TypeNormalForm ctx) -> NormalForm r ctx -> LogNormalForm ann r ctx
 
 doCastR : (a : Constructor ctx) ->
-  (b : NormalForm True ctx) ->
-  NormalForm True ctx ->
-  LogNormalForm ann True ctx
+  (b : TypeNormalForm ctx) ->
+  NormalForm Relevant ctx ->
+  LogNormalForm ann Relevant ctx
 doCastR a (Ntrl b) t = pure (Ntrl $ CastR a b t)
-doCastR (Sort _) (Cnstr (Sort _)) t = pure t
+doCastR (Universe _) (Cnstr (Universe _)) t = pure t
 doCastR ty@(Pi s s'@(Set _) var a b) (Cnstr ty'@(Pi l l' _ a' b')) t =
-  let y : NormalForm (isSet s) (isSet s :: ctx)
+  let y : NormalForm (relevance s) (relevance s :: ctx)
       y = point (var, (s ** Refl)) Here
   in do
   let Yes Refl = decEq (s, s') (l, l')
     | No _ => pure (Ntrl $ CastStuck ty ty' t)
-  x <- assert_total (doCast (isSet s) (weaken [isSet s] a') (weaken [isSet s] a) y)
+  x <- assert_total (doCast (relevance s) (weaken [relevance s] a') (weaken [relevance s] a) y)
   b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure x) (Right . There)))
   b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure y) (Right . There)))
-  t <- assert_total (doApp (Sorted.weaken [isSet s] t) x)
-  t <- assert_total (doCast True b b' t)
+  t <- assert_total (doApp (Sorted.weaken [relevance s] t) x)
+  t <- assert_total (doCast Relevant b b' t)
   pure (Cnstr $ Lambda s var t)
 doCastR ty@(Sigma s@(Set k) s' var a b) (Cnstr ty'@(Sigma l l' _ a' b')) t = do
   let Yes Refl = decEq (s, s') (l, l')
     | No _ => pure (Ntrl $ CastStuck ty ty' t)
-  t1 <- doFst True (isSet s') t
-  u1 <- assert_total (doCast True a a' t)
+  t1 <- doFst Relevant (relevance s') t
+  u1 <- assert_total (doCast Relevant a a' t)
   b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t1) Right))
   b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure u1) Right))
-  t2 <- doSnd True (isSet s') t
-  u2 <- assert_total (doCast (isSet s') b b' t2)
-  pure (Cnstr $ Pair (Set k) s' Oh u1 u2)
+  t2 <- doSnd Relevant (relevance s') t
+  u2 <- assert_total (doCast (relevance s') b b' t2)
+  pure (Cnstr $ Pair (Set k) s' Set u1 u2)
 doCastR ty@(Sigma Prop s'@(Set k) var a b) (Cnstr ty'@(Sigma Prop l' _ a' b')) t = do
   let Yes Refl = decEq s' l'
     | No _ => pure (Ntrl $ CastStuck ty ty' t)
   b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure Irrel) Right))
   b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure Irrel) Right))
-  t2 <- doSnd False True t
-  u2 <- assert_total (doCast True b b' t2)
-  pure (Cnstr $ Pair Prop (Set k) Oh Irrel u2)
+  t2 <- doSnd Irrelevant Relevant t
+  u2 <- assert_total (doCast Relevant b b' t2)
+  pure (Cnstr $ Pair Prop (Set k) Set Irrel u2)
 doCastR Bool (Cnstr Bool) t = pure t
 doCastR a (Cnstr b) t = pure (Ntrl $ CastStuck a b t)
 
-doCast False a b t = pure Irrel
-doCast True (Ntrl a) b t = pure (Ntrl $ CastL a b t)
-doCast True (Cnstr a) b t = doCastR a b t
+doCast Irrelevant a b t = pure Irrel
+doCast Relevant (Ntrl a) b t = pure (Ntrl $ CastL a b t)
+doCast Relevant (Cnstr a) b t = doCastR a b t
 
 export
-doEqual : (b : _) ->
-  (a : NormalForm True ctx) ->
-  NormalForm b ctx ->
-  NormalForm b ctx ->
-  LogNormalForm ann True ctx
+doEqual : (r : _) ->
+  (a : TypeNormalForm ctx) ->
+  NormalForm r ctx ->
+  NormalForm r ctx ->
+  LogNormalForm ann Relevant ctx
 
 -- Relies heavily on typing
-doEqualR : (a : Constructor ctx) -> (b : NormalForm True ctx) -> LogNormalForm ann True ctx
+doEqualR : (a : Constructor ctx) -> (b : TypeNormalForm ctx) -> LogNormalForm ann Relevant ctx
 doEqualR a (Ntrl b) = pure (Ntrl $ EqualR a b)
-doEqualR (Sort _) (Cnstr (Sort s)) = pure (Cnstr Top)
+doEqualR (Universe _) (Cnstr (Universe s)) = pure (Cnstr Top)
 doEqualR ty@(Pi s s' var a b) (Cnstr ty'@(Pi l l' _ a' b')) =
-  let u : NormalForm (isSet s) (isSet s :: ctx)
+  let u : NormalForm (relevance s) (relevance s :: ctx)
       u = point (var, (s ** Refl)) Here
   in do
   let Yes Refl = decEq (s, s') (l, l')
     | No _ => pure (Ntrl $ EqualStuck ty ty')
-  eq1 <- assert_total (doEqual True (cast s) a' a)
-  t <- doCast (isSet s) (weaken [isSet s] a') (weaken [isSet s] a) u
+  eq1 <- assert_total (doEqual Relevant (cast s) a' a)
+  t <- doCast (relevance s) (weaken [relevance s] a') (weaken [relevance s] a) u
   b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t) (Right . There)))
   b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure u) (Right . There)))
-  eq2 <- assert_total (doEqual True (cast s') b b')
-  pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [False] $ Pi s Prop var a eq2))
+  eq2 <- assert_total (doEqual Relevant (cast s') b b')
+  pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [Irrelevant] $ Pi s Prop var a eq2))
 doEqualR ty@(Sigma s s' var a b) (Cnstr ty'@(Sigma l l' _ a' b')) =
-  let t : NormalForm (isSet s) (isSet s :: ctx)
+  let t : NormalForm (relevance s) (relevance s :: ctx)
       t = point (var, (s ** Refl)) Here
   in do
   let Yes Refl = decEq (s, s') (l, l')
     | No _ => pure (Ntrl $ EqualStuck ty ty')
-  eq1 <- assert_total (doEqual True (cast s) a a')
-  u <- doCast (isSet s) (weaken [isSet s] a) (weaken [isSet s] a') t
+  eq1 <- assert_total (doEqual Relevant (cast s) a a')
+  u <- doCast (relevance s) (weaken [relevance s] a) (weaken [relevance s] a') t
   b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t) (Right . There)))
   b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure u) (Right . There)))
-  eq2 <- assert_total (doEqual True (cast s') b b')
-  pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [False] $ Pi s Prop var a eq2))
+  eq2 <- assert_total (doEqual Relevant (cast s') b b')
+  pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [Irrelevant] $ Pi s Prop var a eq2))
 doEqualR Bool (Cnstr Bool) = pure (Cnstr Top)
 doEqualR Top (Cnstr Top) = pure (Cnstr Top)
 doEqualR Bottom (Cnstr Bottom) = pure (Cnstr Top)
 doEqualR a (Cnstr b) = pure (Ntrl $ EqualStuck a b)
 
 export
-doEqualSet : (a, b : NormalForm True ctx) -> LogNormalForm ann True ctx
+doEqualSet : (a, b : TypeNormalForm ctx) -> LogNormalForm ann Relevant ctx
 doEqualSet (Ntrl a) b = pure (Ntrl $ EqualL a b)
 doEqualSet (Cnstr a) b = doEqualR a b
 
-doEqual False a t u = pure (Cnstr Top)
-doEqual True (Ntrl a) t u = pure (Ntrl $ Equal a t u)
-doEqual True (Cnstr (Sort Prop)) t u = do
+doEqual Irrelevant a t u = pure (Cnstr Top)
+doEqual Relevant (Ntrl a) t u = pure (Ntrl $ Equal a t u)
+doEqual Relevant (Cnstr (Universe Prop)) t u = do
   pure (Cnstr $ Sigma Prop Prop ""
-    (Cnstr $ Pi Prop Prop "" t (Sorted.weaken [False] u))
-    (Cnstr $ Unsorted.weaken [False] $ Pi Prop Prop "" u (Sorted.weaken [False] t)))
-doEqual True (Cnstr (Sort (Set _))) t u = doEqualSet t u
-doEqual True (Cnstr (Pi s (Set k) var a b)) t u =
-  let x : NormalForm (isSet s) (isSet s :: ctx)
+    (Cnstr $ Pi Prop Prop "" t (Sorted.weaken [Irrelevant] u))
+    (Cnstr $ Unsorted.weaken [Irrelevant] $ Pi Prop Prop "" u (Sorted.weaken [Irrelevant] t)))
+doEqual Relevant (Cnstr (Universe (Set _))) t u = doEqualSet t u
+doEqual Relevant (Cnstr (Pi s (Set k) var a b)) t u =
+  let x : NormalForm (relevance s) (relevance s :: ctx)
       x = point (var, (s ** Refl)) Here
   in do
-  t <- assert_total (doApp (weaken [isSet s] t) x)
-  u <- assert_total (doApp (weaken [isSet s] u) x)
-  eq <- doEqual True b t u
+  t <- assert_total (doApp (weaken [relevance s] t) x)
+  u <- assert_total (doApp (weaken [relevance s] u) x)
+  eq <- doEqual Relevant b t u
   pure (Cnstr $ Pi s Prop var a eq)
-doEqual True (Cnstr (Sigma s@(Set _) s' var a b)) t u = do
-  t1 <- doFst True (isSet s') t
-  u1 <- doFst True (isSet s') u
-  t2 <- doSnd True (isSet s') t
-  u2 <- doSnd True (isSet s') u
-  eq1 <- doEqual True a t1 u1
+doEqual Relevant (Cnstr (Sigma s@(Set _) s' var a b)) t u = do
+  t1 <- doFst Relevant (relevance s') t
+  u1 <- doFst Relevant (relevance s') u
+  t2 <- doSnd Relevant (relevance s') t
+  u2 <- doSnd Relevant (relevance s') u
+  eq1 <- doEqual Relevant a t1 u1
   bt1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t1) Right))
   bu1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure u1) Right))
-  t2' <- doCast (isSet s') bt1 bu1 t2
-  eq2 <- doEqual (isSet s') (assert_smaller b bu1) t2' u2
-  pure (Cnstr $ Sigma Prop Prop "_" eq1 (Sorted.weaken [False] eq2))
-doEqual True (Cnstr (Sigma Prop (Set k) var a b)) t u = do
-  t2 <- doSnd False True t
-  u2 <- doSnd False True u
+  t2' <- doCast (relevance s') bt1 bu1 t2
+  eq2 <- doEqual (relevance s') (assert_smaller b bu1) t2' u2
+  pure (Cnstr $ Sigma Prop Prop "_" eq1 (Sorted.weaken [Irrelevant] eq2))
+doEqual Relevant (Cnstr (Sigma Prop (Set k) var a b)) t u = do
+  t2 <- doSnd Irrelevant Relevant t
+  u2 <- doSnd Irrelevant Relevant u
   bt1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure $ Irrel) Right))
   bu1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure $ Irrel) Right))
-  t2' <- doCast True bt1 bu1 t2
-  eq2 <- doEqual True (assert_smaller b bu1) t2' u2
-  pure (Cnstr $ Sigma Prop Prop "_" (Cnstr Top) (Sorted.weaken [False] eq2))
-doEqual True (Cnstr Bool) t u = do
-  true <- doIf u (Cnstr Top) (Cnstr Bottom)
-  false <- doIf u (Cnstr Bottom) (Cnstr Top)
-  doIf t true false
-doEqual True (Cnstr a) t u = inScope "wrong constructor for equal" $ fatal a
+  t2' <- doCast Relevant bt1 bu1 t2
+  eq2 <- doEqual Relevant (assert_smaller b bu1) t2' u2
+  pure (Cnstr $ Sigma Prop Prop "_" (Cnstr Top) (Sorted.weaken [Irrelevant] eq2))
+doEqual Relevant (Cnstr Bool) t u = do
+  relevant <- doIf u (Cnstr Top) (Cnstr Bottom)
+  irrelevant <- doIf u (Cnstr Bottom) (Cnstr Top)
+  doIf t relevant irrelevant
+doEqual Relevant (Cnstr a) t u = inScope "wrong constructor for equal" $ fatal a
 
 substCnstr : Constructor ~|> Hom (LogNormalForm' ann) (LogConstructor ann)
-substCnstr (Sort s) f = pure (Sort s)
+substCnstr (Universe s) f = pure (Universe s)
 substCnstr (Pi s s' var a b) f = do
   a <- subst' a f
   b <- subst' b (lift [(_ ** (var, (s ** Refl)))] f)
@@ -241,26 +244,26 @@ substCnstr False f = pure False
 substCnstr Top f = pure Top
 substCnstr Bottom f = pure Bottom
 
-substNtrl : Neutral ~|> Hom (LogNormalForm' ann) (LogNormalForm ann True)
+substNtrl : Neutral ~|> Hom (LogNormalForm' ann) (LogNormalForm ann Relevant)
 substNtrl (Var var sort prf i) f = case f i of
   Left t => t
   Right j => pure (Ntrl $ Var var sort prf j)
-substNtrl (App b t u) f = do
+substNtrl (App r t u) f = do
   t <- substNtrl t f
   u <- subst' u f
   assert_total (doApp t u)
-substNtrl (Fst b t) f = do
+substNtrl (Fst r t) f = do
   t <- substNtrl t f
-  doFst True b t
-substNtrl (Snd b t) f = do
+  doFst Relevant r t
+substNtrl (Snd r t) f = do
   t <- substNtrl t f
-  doSnd b True $ rewrite orTrueTrue b in t
+  doSnd r Relevant $ rewrite pairRelevantRight r in t
 substNtrl (If t u v) f = do
   t <- substNtrl t f
   u <- subst' u f
   v <- subst' v f
   doIf t u v
-substNtrl Absurd f = pure (doAbsurd True)
+substNtrl Absurd f = pure (doAbsurd Relevant)
 substNtrl (Equal a t u) f = do
   a <- substNtrl a f
   t <- subst' t f
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 758b019..f92a0e2 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -4,7 +4,7 @@ import Data.String
 import Data.Vect
 
 import Obs.Logging
-import Obs.Sort
+import Obs.Universe
 import Obs.Syntax
 
 import System
@@ -299,13 +299,13 @@ parens p = match OTPOpen *> optional whitespace *> p <* optional whitespace <* m
 var : Grammar state ObsToken True (WithBounds Syntax)
 var = map (map Var) ident
 
-noArgSort : Grammar state ObsToken True (WithBounds Sort)
-noArgSort = bounds $
+noArgUniverse : Grammar state ObsToken True (WithBounds Universe)
+noArgUniverse = bounds $
   map (const Prop) (match OTProp <* commit) <|>
   map (const (Set 0)) (match OTSet <* commit)
 
-sort : Grammar state ObsToken True (WithBounds Sort)
-sort = bounds $
+universe : Grammar state ObsToken True (WithBounds Universe)
+universe = bounds $
   map (const Prop) (match OTProp <* commit) <|>
   map Set (match OTSet *> commit *> option 0 (match OTNat <* commit))
 
@@ -326,7 +326,7 @@ lambda p =
   [| MkPair (ident <* whitespace <* match OTFatArrow <* whitespace) p |]
 
 partial
-noSortsTerm : Grammar state ObsToken True (WithBounds Syntax)
+noUniversesTerm : Grammar state ObsToken True (WithBounds Syntax)
 partial
 term : Grammar state ObsToken True (WithBounds Syntax)
 partial
@@ -340,17 +340,17 @@ equals : Grammar state ObsToken True (WithBounds Syntax)
 partial
 exp : Grammar state ObsToken True (WithBounds Syntax)
 
-noSortsTerm =
+noUniversesTerm =
   parens exp <|>
   var <|>
   bounds (map (uncurry Pair) (pair exp)) <|>
   bounds (choiceMap (\(k, s) => map (const s) (match k)) termForms)
 
-term = noSortsTerm <|> map (map Sort) noArgSort
+term = noUniversesTerm <|> map (map Universe) noArgUniverse
 
 head =
-  noSortsTerm <|>
-  map (map Sort) sort <|>
+  noUniversesTerm <|>
+  map (map Universe) universe <|>
   bounds
     (choiceMap
       (\(hd, (n ** f)) => match hd *> commit *>
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
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 7bf4b61..32e86c0 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -1,7 +1,7 @@
 ||| Raw syntax for terms. This is before eliminating names.
 module Obs.Syntax
 
-import Obs.Sort
+import Obs.Universe
 
 import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
@@ -13,8 +13,8 @@ import Text.PrettyPrint.Prettyprinter
 public export
 data Syntax : Type where
   Var : String -> Syntax
-  -- Sorts
-  Sort : Sort -> Syntax
+  -- Universes
+  Universe : Universe -> Syntax
   -- Dependent Products
   Pi : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
   Lambda : WithBounds String -> WithBounds Syntax -> Syntax
@@ -55,7 +55,7 @@ prettyPrec : Prec -> Syntax -> Doc ann
 prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
 
 prettyPrec d (Var var) = pretty var
-prettyPrec d (Sort s) = prettyPrec d s
+prettyPrec d (Universe s) = prettyPrec d s
 prettyPrec d (Pi var a b) =
   parenthesise (d > Open) $
   group $
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 422af87..c4d9e40 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -2,7 +2,7 @@
 module Obs.Term
 
 import Data.Fin
-import Obs.Sort
+import Obs.Universe
 import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
 
@@ -13,8 +13,8 @@ import Text.PrettyPrint.Prettyprinter
 public export
 data Term : Nat -> Type where
   Var : String -> Fin n -> Term n
-  -- Sorts
-  Sort : Sort -> Term n
+  -- Universes
+  Universe : Universe -> Term n
   -- Dependent Product
   Pi : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
   Lambda : WithBounds String -> WithBounds (Term (S n)) -> Term n
@@ -74,7 +74,7 @@ prettyPrec : Prec -> Term n -> Doc ann
 prettyPrecBounds : Prec -> WithBounds (Term n) -> Doc ann
 
 prettyPrec d (Var var _) = pretty var
-prettyPrec d (Sort s) = prettyPrec d s
+prettyPrec d (Universe s) = prettyPrec d s
 prettyPrec d (Pi var a b) =
   parenthesise (d > Open) $
   group $
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index 4cc6d8e..7bb5deb 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -9,11 +9,11 @@ import Decidable.Equality
 import Obs.Logging
 import Obs.NormalForm
 import Obs.NormalForm.Normalise
-import Obs.Sort
 import Obs.Substitution
 import Obs.Term
 import Obs.Typing.Context
 import Obs.Typing.Conversion
+import Obs.Universe
 
 import System
 
@@ -33,44 +33,44 @@ mismatch lhs rhs = fatal $
 typeMismatch : Doc ann -> Doc ann -> Logging ann a
 typeMismatch lhs rhs = inScope "type mismatch" $ mismatch lhs rhs
 
-sortMismatch : Doc ann -> Doc ann -> Logging ann a
-sortMismatch lhs rhs = inScope "sort mismatch" $ mismatch lhs rhs
+universeMismatch : Doc ann -> Doc ann -> Logging ann a
+universeMismatch lhs rhs = inScope "universe mismatch" $ mismatch lhs rhs
 
 -- Utilities -------------------------------------------------------------------
 
-MkPair : (s, s' : Sort)
-  -> NormalForm (isSet s) ctx
-  -> NormalForm (isSet s') ctx
-  -> NormalForm (isSet (max s s')) ctx
+MkPair : (s, s' : Universe)
+  -> NormalForm (relevance s) ctx
+  -> NormalForm (relevance s') ctx
+  -> NormalForm (relevance (max s s')) ctx
 MkPair Prop Prop t u = u
-MkPair Prop s'@(Set _) t u = Cnstr $ Pair Prop s' Oh t u
-MkPair s@(Set _) s' t u = Cnstr $ Pair s s' Oh t u
+MkPair Prop s'@(Set _) t u = Cnstr $ Pair Prop s' Set t u
+MkPair s@(Set _) s' t u = Cnstr $ Pair s s' Set t u
 
 -- Checking and Inference ------------------------------------------------------
 
 check : (tyCtx : TyContext ctx)
-  -> (s : Sort)
-  -> NormalForm True ctx
+  -> (s : Universe)
+  -> TypeNormalForm ctx
   -> WithBounds (Term (length ctx))
-  -> Logging ann (NormalForm (isSet s) ctx)
+  -> Logging ann (NormalForm (relevance s) ctx)
 
 checkType : (tyCtx : TyContext ctx)
-  -> (s : Sort)
+  -> (s : Universe)
   -> WithBounds (Term (length ctx))
-  -> Logging ann (NormalForm True ctx)
-checkType ctx s tm = check ctx (suc s) (cast s) tm
+  -> Logging ann (TypeNormalForm ctx)
+checkType ctx s tm = check ctx (succ s) (cast s) tm
 
 infer : (tyCtx : TyContext ctx)
   -> WithBounds (Term (length ctx))
-  -> Logging ann (s ** (NormalForm True ctx, NormalForm (isSet s) ctx))
+  -> Logging ann (s ** (TypeNormalForm ctx, NormalForm (relevance s) ctx))
 
 inferType : {default typeMismatch tag : forall a . Doc ann -> Doc ann -> Logging ann a}
   -> (tyCtx : TyContext ctx)
   -> WithBounds (Term (length ctx))
-  -> Logging ann (Sort, NormalForm True ctx)
+  -> Logging ann (Universe, TypeNormalForm ctx)
 inferType ctx tm = inBounds tm.bounds $ do
-  (Set _ ** (Cnstr (Sort s), a)) <- infer ctx tm
-    | (_ ** (a, t)) => tag (pretty "sort") (pretty a)
+  (Set _ ** (Cnstr (Universe s), a)) <- infer ctx tm
+    | (_ ** (a, t)) => tag (pretty "universe") (pretty a)
   pure (s, a)
 
 check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of
@@ -79,7 +79,7 @@ check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of
     trace $ pretty {ann} "checking body has type" <++> pretty b
     t <- check (ctx ::< MkFreeVar l a var.val) l' b (assert_smaller tm t)
     let Yes Refl = decEq s (l ~> l')
-      | No _ => fatal "internal sort mismatch"
+      | No _ => fatal "internal universe mismatch"
     pure $ case l' of
       Prop => Irrel
       Set _ => Cnstr (Lambda l var.val t)
@@ -92,7 +92,7 @@ check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of
     trace $ pretty {ann} "checking second has type" <++> pretty b
     u <- check ctx l' b (assert_smaller tm u)
     let Yes Refl = decEq s (max l l')
-      | No _ => fatal "internal sort mismatch"
+      | No _ => fatal "internal universe mismatch"
     pure $ MkPair l l' t u
   (_, Pair t u) => typeMismatch (pretty "pair type") (pretty ty)
   (_, Absurd t) => do
@@ -108,7 +108,7 @@ check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of
       | No _ => typeMismatch (pretty a) (pretty b)
     a' <- subst a (reduce ctx)
     b' <- subst b (reduce ctx)
-    Just _ <- inScope "convert" $ runMaybeT $ convert (suc s) (cast s) a' b'
+    Just _ <- inScope "convert" $ runMaybeT $ convert (succ s) (cast s) a' b'
     | Nothing => inScope "conversion failed" $ mismatch (pretty a) (pretty b)
     pure t
 
@@ -117,16 +117,16 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
     info $ pretty {ann} "encountered variable" <++> pretty tm.val
     let def = index' ctx i
     pure (def.sort ** (def.ty, def.tm))
-  (Sort s) => do
-    info $ pretty {ann} "encountered sort" <++> pretty tm.val
-    pure (suc (suc s) ** (cast (suc s), cast s))
+  (Universe s) => do
+    info $ pretty {ann} "encountered universe" <++> pretty tm.val
+    pure (succ (succ s) ** (cast (succ s), cast s))
   (Pi var a b) => do
     info "encountered pi"
     (s, a) <- inferType ctx (assert_smaller tm a)
     trace $ pretty {ann} "domain type is" <++> pretty a
     (s', b) <- inferType (ctx ::< MkFreeVar s a var.val) (assert_smaller tm b)
     trace $ pretty {ann} "codomain type is" <++> pretty b
-    pure (suc (s ~> s') ** (cast (s ~> s'), Cnstr (Pi s s' var.val a b)))
+    pure (succ (s ~> s') ** (cast (s ~> s'), Cnstr (Pi s s' var.val a b)))
   (Lambda var t) => fatal "cannot infer type of lambda"
   (App t u) => do
     info "encountered application"
@@ -137,17 +137,17 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
     u <- check ctx l a (assert_smaller tm u)
     trace $ pretty {ann} "argument is well typed"
     let Yes Refl = decEq s (l ~> l')
-      | No _ => fatal "internal sort mismatch"
+      | No _ => fatal "internal universe mismatch"
     ty <- subst1 u b
     tm <- doApp t u
-    pure (l' ** (ty, rewrite sym $ impredicative l l' in tm))
+    pure (l' ** (ty, rewrite sym $ functionRelevance l l' in tm))
   (Sigma var a b) => do
     info "encountered sigma"
     (s, a) <- inferType ctx (assert_smaller tm a)
     trace $ pretty {ann} "first type is" <++> pretty a
     (s', b) <- inferType (ctx ::< MkFreeVar s a var.val) (assert_smaller tm b)
     trace $ pretty {ann} "second type is" <++> pretty b
-    pure (suc (max s s') ** (cast (max s s'), Cnstr (Sigma s s' var.val a b)))
+    pure (succ (max s s') ** (cast (max s s'), Cnstr (Sigma s s' var.val a b)))
   (Pair t u) => fatal "cannot infer type of pair"
   (Fst t) => do
     info "encountered first"
@@ -155,9 +155,9 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
       | (_ ** (ty, _)) => inBounds t.bounds $ typeMismatch (pretty "pair type") (pretty ty)
     trace $ pretty {ann} "pair has type" <++> pretty ty
     let Yes Refl = decEq s (max l l')
-      | No _ => fatal "internal sort mismatch"
+      | No _ => fatal "internal universe mismatch"
     let ty = a
-    tm <- doFst (isSet l) (isSet l') (rewrite sym $ maxIsSet l l' in t)
+    tm <- doFst (relevance l) (relevance l') (rewrite sym $ pairRelevance l l' in t)
     pure (l ** (ty, tm))
   (Snd t) => do
     info "encountered second"
@@ -165,11 +165,11 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
       | (_ ** (ty, _)) => inBounds t.bounds $ typeMismatch (pretty "pair type") (pretty ty)
     trace $ pretty {ann} "pair has type" <++> pretty ty
     let Yes Refl = decEq s (max l l')
-      | No _ => fatal "internal sort mismatch"
-    let t = rewrite sym $ maxIsSet l l' in t
-    fst <- doFst (isSet l) (isSet l') t
+      | No _ => fatal "internal universe mismatch"
+    let t = rewrite sym $ pairRelevance l l' in t
+    fst <- doFst (relevance l) (relevance l') t
     ty <- subst1 fst b
-    tm <- doSnd (isSet l) (isSet l') t
+    tm <- doSnd (relevance l) (relevance l') t
     pure (l' ** (ty, tm))
   Bool => do
     info "encountered bool"
@@ -197,13 +197,13 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
     pure (s ** (ty, tm))
   Top => do
     info "encountered top"
-    pure (Set 0 ** (cast Prop, Cnstr Top))
+    pure (Set 0 ** (Cnstr (Universe Prop), Cnstr Top))
   Point => do
     info "encountered point"
     pure (Prop ** (Cnstr Top, Irrel))
   Bottom => do
     info "encountered bottom"
-    pure (Set 0 ** (cast Prop, Cnstr Bottom))
+    pure (Set 0 ** (Cnstr (Universe Prop), Cnstr Bottom))
   (Absurd t) => fatal "cannot infer type of absurd"
   (Equal t u) => do
     info "encountered equal"
@@ -211,13 +211,13 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
     trace $ pretty {ann} "left side has type" <++> pretty a
     u <- check ctx s a (assert_smaller tm u)
     trace "right side is well typed"
-    eq <- doEqual (isSet s) a t u
-    pure (Set 0 ** (cast Prop, eq))
+    eq <- doEqual (relevance s) a t u
+    pure (Set 0 ** (Cnstr (Universe Prop), eq))
   (Refl t) => do
     info "encountered refl"
     (s ** (a, t)) <- infer ctx (assert_smaller tm t)
     trace "argument is well typed"
-    eq <- doEqual (isSet s) a t t
+    eq <- doEqual (relevance s) a t t
     pure (Prop ** (eq, Irrel))
   (Transp b t u t' e) => do
     info "encountered transp"
@@ -225,12 +225,12 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
     trace $ pretty {ann} "index type is" <++> pretty a
     t' <- check ctx s a (assert_smaller tm t')
     trace "new index is well typed"
-    b <- check ctx (s ~> Set 0) (Cnstr $ Pi s (Set 0) "" a (cast Prop)) (assert_smaller tm b)
+    b <- check ctx (s ~> Set 0) (Cnstr $ Pi s (Set 0) "" a (Cnstr (Universe Prop))) (assert_smaller tm b)
     trace "transporting in Prop"
     oldB <- doApp b t
     u <- check ctx Prop oldB (assert_smaller tm u)
     trace "old-indexed proposition is well typed"
-    eq <- doEqual (isSet s) a t t'
+    eq <- doEqual (relevance s) a t t'
     trace $ pretty {ann} "checking equality has type" <++> pretty eq
     e <- check ctx Prop eq (assert_smaller tm e)
     trace "equality is well typed"
@@ -242,19 +242,19 @@ infer ctx tm = inBounds tm.bounds $ case tm.val of
     trace $ pretty {ann} "old type is" <++> pretty a
     b <- checkType ctx s (assert_smaller tm b)
     trace $ pretty {ann} "new type is" <++> pretty b
-    eq <- doEqual True (cast s) a b
+    eq <- doEqual Relevant (cast s) a b
     e <- check ctx Prop eq (assert_smaller tm e)
     trace "equality is well typed"
     t <- check ctx s a (assert_smaller tm t)
     trace "value is well typed"
-    tm <- doCast (isSet s) a b t
+    tm <- doCast (relevance s) a b t
     pure (s ** (b, tm))
   (CastId t) => do
     info "encountered castRefl"
     (s ** (a, t)) <- infer ctx (assert_smaller tm t)
     trace $ pretty {ann} "argument has type" <++> pretty a
-    lhs <- doCast (isSet s) a a t
-    ret <- doEqual (isSet s) a lhs t
+    lhs <- doCast (relevance s) a a t
+    ret <- doEqual (relevance s) a lhs t
     pure (Prop ** (ret, Irrel))
 
 -- Checking Definitions and Blocks ---------------------------------------------
diff --git a/src/Obs/Typing/Context.idr b/src/Obs/Typing/Context.idr
index 636c9f2..4706dca 100644
--- a/src/Obs/Typing/Context.idr
+++ b/src/Obs/Typing/Context.idr
@@ -8,7 +8,7 @@ import Obs.Logging
 import Obs.NormalForm
 import Obs.NormalForm.Normalise
 import Obs.Substitution
-import Obs.Sort
+import Obs.Universe
 
 import Text.Bounded
 
@@ -17,40 +17,40 @@ import Text.Bounded
 infix 5 ::<
 
 public export
-record FreeVar (ctx : List Bool) where
+record FreeVar (ctx : List Relevance) where
   constructor MkFreeVar
-  sort : Sort
-  ty : NormalForm True ctx
+  sort : Universe
+  ty : TypeNormalForm ctx
   name : String
 
 public export
-record TyDef (b : Bool) (ctx : List Bool) where
+record TyDef (b : Relevance) (ctx : List Relevance) where
   constructor MkDefinition
   name : String
-  sort : Sort
-  ty : NormalForm True ctx
-  tm : NormalForm (isSet sort) ctx
-  correct : isSet sort = b
+  sort : Universe
+  ty : TypeNormalForm ctx
+  tm : NormalForm (relevance sort) ctx
+  correct : relevance sort = b
 
 public export
-data TyContext : Unsorted.Family Bool where
+data TyContext : Unsorted.Family Relevance where
   Nil   : TyContext []
-  (:<)  : TyContext ctx -> (def : Definition ctx) -> TyContext (isSet def.sort :: ctx)
-  (::<) : TyContext ctx -> (var : FreeVar ctx) -> TyContext (isSet var.sort :: ctx)
+  (:<)  : TyContext ctx -> (def : Definition ctx) -> TyContext (relevance def.sort :: ctx)
+  (::<) : TyContext ctx -> (var : FreeVar ctx) -> TyContext (relevance var.sort :: ctx)
 
 -- Properties ------------------------------------------------------------------
 
-freeVars : TyContext ctx -> List Bool
+freeVars : TyContext ctx -> List Relevance
 freeVars [] = []
 freeVars (ctx :< def) = freeVars ctx
-freeVars (ctx ::< var) = isSet var.sort :: freeVars ctx
+freeVars (ctx ::< var) = relevance var.sort :: freeVars ctx
 
-Sorted.Rename Bool TyDef where
+Sorted.Rename Relevance TyDef where
   rename def f = {ty := rename def.ty f, tm := rename def.tm f} def
 
 -- Construction ----------------------------------------------------------------
 
-fromDef : (def : Definition ctx) -> TyDef (isSet def.sort) ctx
+fromDef : (def : Definition ctx) -> TyDef (relevance def.sort) ctx
 fromDef def = MkDefinition
   { name = def.name.val
   , sort = def.sort
@@ -59,11 +59,11 @@ fromDef def = MkDefinition
   , correct = Refl
   }
 
-fromVar : (var : FreeVar ctx) -> TyDef (isSet var.sort) (isSet var.sort :: ctx)
+fromVar : (var : FreeVar ctx) -> TyDef (relevance var.sort) (relevance var.sort :: ctx)
 fromVar var = MkDefinition
   { name = var.name
   , sort = var.sort
-  , ty = weaken [isSet var.sort] var.ty
+  , ty = weaken [relevance var.sort] var.ty
   , tm = point (var.name, (var.sort ** Refl)) Here
   , correct = Refl
   }
@@ -80,10 +80,10 @@ getContext : TyContext ctx -> (ctx' ** ctx = ctx')
 getContext [] = ([] ** Refl)
 getContext (ctx :< def) =
   let (ctx' ** prf) = getContext ctx in
-  (isSet def.sort :: ctx' ** cong (isSet def.sort ::) prf)
+  (relevance def.sort :: ctx' ** cong (relevance def.sort ::) prf)
 getContext (ctx ::< var) =
   let (ctx' ** prf) = getContext ctx in
-  (isSet var.sort :: ctx' ** cong (isSet var.sort ::) prf)
+  (relevance var.sort :: ctx' ** cong (relevance var.sort ::) prf)
 
 export
 index : TyContext ctx -> Map ctx TyDef ctx
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr
index d5dc86a..766c21e 100644
--- a/src/Obs/Typing/Conversion.idr
+++ b/src/Obs/Typing/Conversion.idr
@@ -4,36 +4,36 @@ import Control.Monad.Maybe
 import Control.Monad.Trans
 
 import Data.Bool
-import Data.So
+import Data.Nat
 
 import Decidable.Equality
 
 import Obs.Logging
 import Obs.NormalForm
 import Obs.NormalForm.Normalise
-import Obs.Sort
 import Obs.Substitution
+import Obs.Universe
 
 %default total
 
 -- Conversion ------------------------------------------------------------------
 
 export
-convert : (s : Sort)
-  -> (a : NormalForm True ctx)
-  -> (t, u : NormalForm (isSet s) ctx)
-  -> MaybeT (Logging ann) (NormalForm (isSet s) ctx)
+convert : (s : Universe)
+  -> (a : TypeNormalForm ctx)
+  -> (t, u : NormalForm (relevance s) ctx)
+  -> MaybeT (Logging ann) (NormalForm (relevance s) ctx)
 
-untypedConvert : (t, u : NormalForm True ctx) -> MaybeT (Logging ann) (NormalForm True ctx)
+untypedConvert : (t, u : NormalForm Relevant ctx) -> MaybeT (Logging ann) (NormalForm Relevant ctx)
 -- Diagonals
-untypedConvert (Cnstr (Sort s)) (Cnstr (Sort s')) =
-  if s == s' then pure (Cnstr (Sort s)) else nothing
+untypedConvert (Cnstr (Universe s)) (Cnstr (Universe s')) =
+  if s == s' then pure (Cnstr (Universe s)) else nothing
 untypedConvert (Cnstr (Pi s s' var a b)) (Cnstr (Pi l l' _ a' b')) = do
   let Yes Refl = decEq s l
     | No _ => nothing
   lift $ trace "going back to type-directed conversion"
-  a <- assert_total (convert (suc s) (cast s) a a')
-  b <- assert_total (convert (suc s') (cast s') b b')
+  a <- assert_total (convert (succ s) (cast s) a a')
+  b <- assert_total (convert (succ s') (cast s') b b')
   pure (Cnstr $ Pi s s' var a b)
 untypedConvert (Cnstr (Lambda s var t)) (Cnstr (Lambda s' _ u)) = do
   let Yes Refl = decEq s s'
@@ -45,8 +45,8 @@ untypedConvert (Cnstr (Sigma s s' var a b)) (Cnstr (Sigma l l' _ a' b')) = do
   let Yes Refl = decEq s l
     | No _ => nothing
   lift $ trace "going back to type-directed conversion"
-  a <- assert_total (convert (suc s) (cast s) a a')
-  b <- assert_total (convert (suc s') (cast s') b b')
+  a <- assert_total (convert (succ s) (cast s) a a')
+  b <- assert_total (convert (succ s') (cast s') b b')
   pure (Cnstr $ Sigma s s' var a b)
 untypedConvert (Cnstr (Pair s@(Set _) s'@(Set _) prf t u)) (Cnstr (Pair l l' prf' t' u')) = do
   let Yes Refl = decEq (s, s') (l, l')
@@ -54,19 +54,19 @@ untypedConvert (Cnstr (Pair s@(Set _) s'@(Set _) prf t u)) (Cnstr (Pair l l' prf
   lift $ trace "converting pair pointwise"
   t <- untypedConvert t t'
   u <- untypedConvert u u'
-  pure (Cnstr $ Pair l l' Oh t u)
+  pure (Cnstr $ Pair l l' Set t u)
 untypedConvert (Cnstr (Pair s@(Set _) Prop prf t u)) (Cnstr (Pair l Prop prf' t' u')) = do
   let Yes Refl = decEq s l
     | No _ => nothing
   lift $ trace "converting pair pointwise"
   t <- untypedConvert t t'
-  pure (Cnstr $ Pair l Prop Oh t Irrel)
+  pure (Cnstr $ Pair l Prop Set t Irrel)
 untypedConvert (Cnstr (Pair Prop s'@(Set _) prf t u)) (Cnstr (Pair Prop l' prf' t' u')) = do
   let Yes Refl = decEq s' l'
     | No _ => nothing
   lift $ trace "converting pair pointwise"
   u <- untypedConvert u u'
-  pure (Cnstr $ Pair Prop l' Oh Irrel u)
+  pure (Cnstr $ Pair Prop l' Set Irrel u)
 untypedConvert (Cnstr Bool) (Cnstr Bool) = pure (Cnstr Bool)
 untypedConvert (Cnstr True) (Cnstr True) = pure (Cnstr True)
 untypedConvert (Cnstr False) (Cnstr False) = pure (Cnstr False)
@@ -74,23 +74,23 @@ untypedConvert (Cnstr Top) (Cnstr Top) = pure (Cnstr Top)
 untypedConvert (Cnstr Bottom) (Cnstr Bottom) = pure (Cnstr Bottom)
 untypedConvert t@(Ntrl (Var _ _ _ i)) (Ntrl (Var _ _ _ j)) =
   if elemToNat i == elemToNat j then pure t else nothing
-untypedConvert lhs@(Ntrl (App b t u)) rhs@(Ntrl (App b' t' u')) = do
-  let Yes Refl = decEq b b'
+untypedConvert lhs@(Ntrl (App r t u)) rhs@(Ntrl (App r' t' u')) = do
+  let Yes Refl = decEq r r'
     | No _ => nothing
   lift $ trace "checking parts of a spine"
   t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
-  let True = b'
-    | False => lift $ doApp t Irrel
+  let Relevant = r'
+    | Irrelevant => lift $ doApp t Irrel
   u <- untypedConvert u u'
   lift $ doApp t u
-untypedConvert lhs@(Ntrl (Fst b t)) rhs@(Ntrl (Fst b' t')) = do
+untypedConvert lhs@(Ntrl (Fst r t)) rhs@(Ntrl (Fst r' t')) = do
   lift $ trace "checking full pair for fst"
   t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
-  lift $ doFst True b t
-untypedConvert lhs@(Ntrl (Snd b t)) rhs@(Ntrl (Snd b' t')) = do
+  lift $ doFst Relevant r t
+untypedConvert lhs@(Ntrl (Snd r t)) rhs@(Ntrl (Snd r' t')) = do
   lift $ trace "checking full pair for snd"
   t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
-  lift $ doSnd b True (rewrite orTrueTrue b in t)
+  lift $ doSnd r Relevant (rewrite pairRelevantRight r in t)
 untypedConvert lhs@(Ntrl (If t f g)) rhs@(Ntrl (If t' f' g')) = do
   lift $ trace "checking all branches of if"
   t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
@@ -139,25 +139,25 @@ untypedConvert lhs@(Ntrl (CastStuck a b t)) rhs@(Ntrl (CastStuck a' b' t')) = do
   lift $ doCast _ a b t
 -- Pi types
 untypedConvert t@(Cnstr (Lambda s var _)) (Ntrl u) = do
-  u <- lift $ doApp (Ntrl $ weaken [isSet s] u) (point (var, (s ** Refl)) Here)
+  u <- lift $ doApp (Ntrl $ weaken [relevance s] u) (point (var, (s ** Refl)) Here)
   assert_total (untypedConvert t (Cnstr (Lambda s var u)))
 untypedConvert (Ntrl t) u@(Cnstr (Lambda s var _)) = do
-  t <- lift $ doApp (Ntrl $ weaken [isSet s] t) (point (var, (s ** Refl)) Here)
+  t <- lift $ doApp (Ntrl $ weaken [relevance s] t) (point (var, (s ** Refl)) Here)
   assert_total (untypedConvert (Cnstr (Lambda s var t)) u)
 -- Sigma types
 untypedConvert t@(Cnstr (Pair s s' prf _ _)) t'@(Ntrl _) =
-  let t'' : NormalForm (isSet s || isSet s') ctx
-      t'' = rewrite trans (sym $ maxIsSet s s') (soToEq prf) in t'
+  let t'' : NormalForm (pair (relevance s) (relevance s')) ctx
+      t'' = rewrite trans (sym $ pairRelevance s s') (forgetIsRelevant prf) in t'
   in do
-  t' <- lift $ doFst (isSet s) (isSet s') t''
-  u' <- lift $ doSnd (isSet s) (isSet s') t''
+  t' <- lift $ doFst (relevance s) (relevance s') t''
+  u' <- lift $ doSnd (relevance s) (relevance s') t''
   assert_total (untypedConvert t (Cnstr (Pair s s' prf t' u')))
 untypedConvert t@(Ntrl _) t'@(Cnstr (Pair s s' prf _ _)) =
-  let t'' : NormalForm (isSet s || isSet s') ctx
-      t'' = rewrite trans (sym $ maxIsSet s s') (soToEq prf) in t
+  let t'' : NormalForm (pair (relevance s) (relevance s')) ctx
+      t'' = rewrite trans (sym $ pairRelevance s s') (forgetIsRelevant prf) in t
   in do
-  t <- lift $ doFst (isSet s) (isSet s') t''
-  u <- lift $ doSnd (isSet s) (isSet s') t''
+  t <- lift $ doFst (relevance s) (relevance s') t''
+  u <- lift $ doSnd (relevance s) (relevance s') t''
   assert_total (untypedConvert (Cnstr (Pair s s' prf t u)) t')
 -- Bools
 -- no cases because diagonals complete
@@ -168,33 +168,33 @@ convert Prop a Irrel Irrel = pure Irrel
 convert (Set k) (Ntrl a) t u = do
   lift $ trace $ pretty {ann} "cannot do type-directed conversion on" <++> pretty a
   untypedConvert t u
-convert (Set k) (Cnstr (Sort s)) t u = do
+convert (Set k) (Cnstr (Universe s)) t u = do
   lift $ trace $ pretty {ann} "converting in type" <++> pretty s
   untypedConvert t u
 convert (Set k) (Cnstr (Pi s s'@(Set _) var a b)) t u = do
   -- s' must be Set, otherwise ty is in Prop
   lift $ trace "converting pi type"
-  t' <- lift $ doApp (Sorted.weaken [isSet s] t) (point (var, (s ** Refl)) Here)
-  u' <- lift $ doApp (Sorted.weaken [isSet s] u) (point (var, (s ** Refl)) Here)
+  t' <- lift $ doApp (Sorted.weaken [relevance s] t) (point (var, (s ** Refl)) Here)
+  u' <- lift $ doApp (Sorted.weaken [relevance s] u) (point (var, (s ** Refl)) Here)
   t <- convert s' b t' u'
   pure (Cnstr $ Lambda s var t)
 convert (Set k) ty@(Cnstr (Sigma s@(Set j) s' var a b)) t u = do
   lift $ trace "converting sigma type"
-  t1 <- lift $ doFst True (isSet s') t
-  u1 <- lift $ doFst True (isSet s') u
+  t1 <- lift $ doFst Relevant (relevance s') t
+  u1 <- lift $ doFst Relevant (relevance s') u
   t1 <- convert s a t1 u1
-  t2 <- lift $ doSnd True (isSet s') t
-  u2 <- lift $ doSnd True (isSet s') u
+  t2 <- lift $ doSnd Relevant (relevance s') t
+  u2 <- lift $ doSnd Relevant (relevance s') u
   b <- lift $ subst1 t1 b
   t2 <- convert s' (assert_smaller ty b) t2 u2
-  pure (Cnstr $ Pair s s' Oh t1 t2)
+  pure (Cnstr $ Pair s s' Set t1 t2)
 convert (Set k) ty@(Cnstr (Sigma Prop s'@(Set _) var a b)) t u = do
   lift $ trace "converting sigma type (snd only)"
-  t2 <- lift $ doSnd False True t
-  u2 <- lift $ doSnd False True u
+  t2 <- lift $ doSnd Irrelevant Relevant t
+  u2 <- lift $ doSnd Irrelevant Relevant u
   b <- lift $ subst1 Irrel b
   t2 <- convert s' (assert_smaller ty b) t2 u2
-  pure (Cnstr $ Pair Prop s' Oh Irrel t2)
+  pure (Cnstr $ Pair Prop s' Set Irrel t2)
 convert (Set 0) (Cnstr Bool) (Cnstr True) (Cnstr True) = do
   lift $ trace "converting bool (true)"
   pure (Cnstr True)
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