Add more program structure to type universes.

1 files changed, 20 insertions, 20 deletions

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