Index normal forms with relevance.

- Remove container types.
- Replace sum types with booleans.
- Remove type annotation from absurd.
- Add original type as argument to cast.
- Make if (was case) take a lambda for the return type.

13 files changed, 1299 insertions, 1377 deletions

diff --git a/obs.ipkg b/obs.ipkg
index 71451bb..7346579 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -19,4 +19,5 @@ modules
   , Obs.Syntax
   , Obs.Term
   , Obs.Typing
+  , Obs.Typing.Context
   , Obs.Typing.Conversion
diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 48709c1..b32af2d 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -51,54 +51,21 @@ abstractSyntax ctx (Fst t) = do
 abstractSyntax ctx (Snd t) = do
   t <- abstractSyntaxBounds ctx t
   pure (Snd t)
-abstractSyntax ctx (Sum a b) = do
-  a <- abstractSyntaxBounds ctx a
-  b <- abstractSyntaxBounds ctx b
-  pure (Sum a b)
-abstractSyntax ctx (Left t) = do
-  t <- abstractSyntaxBounds ctx t
-  pure (Left t)
-abstractSyntax ctx (Right t) = do
+abstractSyntax ctx Bool = pure Bool
+abstractSyntax ctx True = pure True
+abstractSyntax ctx False = pure False
+abstractSyntax ctx (If var a t f g) = do
+  a <- abstractSyntaxBounds (bind ctx var.val) a
   t <- abstractSyntaxBounds ctx t
-  pure (Right t)
-abstractSyntax ctx (Case t s b f g) = do
-  t <- abstractSyntaxBounds ctx t
-  s <- abstractSyntaxBounds ctx s
-  b <- abstractSyntaxBounds ctx b
   f <- abstractSyntaxBounds ctx f
   g <- abstractSyntaxBounds ctx g
-  pure (Case t s b f g)
-abstractSyntax ctx (Container a s s') = do
-  a <- abstractSyntaxBounds ctx a
-  s <- abstractSyntaxBounds ctx s
-  s' <- abstractSyntaxBounds ctx s'
-  pure (Container a s s')
-abstractSyntax ctx (MkContainer t p f) = do
-  t <- abstractSyntaxBounds ctx t
-  p <- abstractSyntaxBounds ctx p
-  f <- abstractSyntaxBounds ctx f
-  pure (MkContainer t p f)
-abstractSyntax ctx (Tag t) = do
-  t <- abstractSyntaxBounds ctx t
-  pure (Tag t)
-abstractSyntax ctx (Position t) = do
-  t <- abstractSyntaxBounds ctx t
-  pure (Position t)
-abstractSyntax ctx (Next t) = do
-  t <- abstractSyntaxBounds ctx t
-  pure (Next t)
-abstractSyntax ctx (Sem s a t) = do
-  s <- abstractSyntaxBounds ctx s
-  a <- abstractSyntaxBounds ctx a
-  t <- abstractSyntaxBounds ctx t
-  pure (Sem s a t)
+  pure (If var a t f g)
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom
-abstractSyntax ctx (Absurd a t) = do
-  a <- abstractSyntaxBounds ctx a
+abstractSyntax ctx (Absurd t) = do
   t <- abstractSyntaxBounds ctx t
-  pure (Absurd a t)
+  pure (Absurd t)
 abstractSyntax ctx (Equal t u) = do
   t <- abstractSyntaxBounds ctx t
   u <- abstractSyntaxBounds ctx u
@@ -106,18 +73,19 @@ abstractSyntax ctx (Equal t u) = do
 abstractSyntax ctx (Refl t) = do
   t <- abstractSyntaxBounds ctx t
   pure (Refl t)
-abstractSyntax ctx (Transp t b u t' e) = do
+abstractSyntax ctx (Transp a t u t' e) = do
+  a <- abstractSyntaxBounds ctx a
   t <- abstractSyntaxBounds ctx t
-  b <- abstractSyntaxBounds ctx b
   u <- abstractSyntaxBounds ctx u
   t' <- abstractSyntaxBounds ctx t'
   e <- abstractSyntaxBounds ctx e
-  pure (Transp t b u t' e)
-abstractSyntax ctx (Cast b e t) = do
+  pure (Transp a t u t' e)
+abstractSyntax ctx (Cast a b e t) = do
+  a <- abstractSyntaxBounds ctx a
   b <- abstractSyntaxBounds ctx b
   e <- abstractSyntaxBounds ctx e
   t <- abstractSyntaxBounds ctx t
-  pure (Cast b e t)
+  pure (Cast a b e t)
 abstractSyntax ctx (CastId t) = do
   t <- abstractSyntaxBounds ctx t
   pure (CastId t)
diff --git a/src/Obs/Logging.idr b/src/Obs/Logging.idr
index 0761775..ef0bae6 100644
--- a/src/Obs/Logging.idr
+++ b/src/Obs/Logging.idr
@@ -1,7 +1,5 @@
 module Obs.Logging
 
-import Data.List.Lazy
-
 import System
 
 import Text.Bounded
@@ -40,60 +38,96 @@ Ord Level where
 
 record Message (ann : Type) where
   constructor MkMessage
-  lvl  : Level
-  msg  : Doc ann
+  lvl : Level
+  msg : Doc ann
+  bounds : Maybe Bounds
   tags : List String
 
 pretty : Message ann -> Doc ann
 pretty msg =
-  hsep $
-  [ fill 6 (pretty (show msg.lvl) <+> colon) ] ++
-  reverse (map (\s => pretty s <+> colon) msg.tags) ++
-  [ align msg.msg ]
+  let leader =
+    hsep $
+      [ fill 6 (pretty (show msg.lvl) <+> colon) ] ++
+      [ Doc.pretty $ concat {t = List} $
+        case msg.bounds of
+          Nothing => []
+          Just bounds =>
+            [ show (1 + bounds.startLine)
+            , ":"
+            , show bounds.startCol
+            , "--"
+            , show (1 + bounds.endLine)
+            , ":"
+            , show bounds.endCol
+            , ":"
+            ]
+      ] ++
+      map (\s => pretty s <+> colon) msg.tags
+  in group $ width (group leader <+> line) (\width => group $ indent (2 - width) msg.msg)
 
 -- Logging Monad ---------------------------------------------------------------
 
 export
-record Logging (ann, t : Type) where
-  constructor MkLogging
-  out  : Maybe t
-  msgs : LazyList (Message ann)
+data Logging : (ann, t : Type) -> Type where
+  Cont : (msg : Message ann) -> (l : Lazy (Logging ann t)) -> Logging ann t
+  Abort : Logging ann t
+  End : (v : t) -> Logging ann t
+
+%name Logging l, l'
 
 export
 Functor (Logging ann) where
-  map f = {out $= map f}
+  map f (Cont msg l) = Cont msg (map f l)
+  map f Abort = Abort
+  map f (End v) = End (f v)
 
 export
 Applicative (Logging ann) where
-  pure v = MkLogging {out = pure v, msgs = []}
-  f <*> v = MkLogging {out = f.out <*> v.out, msgs = f.msgs ++ v.msgs}
+  pure = End
+  (Cont msg f) <*> v = Cont msg (f <*> v)
+  Abort <*> v = Abort
+  (End f) <*> (Cont msg v) = Cont msg (End f <*> v)
+  (End f) <*> Abort = Abort
+  (End f) <*> (End v) = End (f v)
 
 export
 Monad (Logging ann) where
-  (MkLogging Nothing  msgs) >>= f = MkLogging Nothing msgs
-  (MkLogging (Just v) msgs) >>= f = {msgs $= (msgs ++)} (f v)
+  join (Cont msg l) = Cont msg (join l)
+  join Abort = Abort
+  join (End v) = v
 
--- -- Eliminators -----------------------------------------------------------------
+-- Eliminators -----------------------------------------------------------------
 
 export
 discard : Logging ann a -> Maybe a
-discard = out
+discard (Cont msg l) = discard l
+discard Abort = Nothing
+discard (End v) = Just v
 
 export
 logToTerminal : Level -> Logging AnsiStyle a -> IO a
-logToTerminal lvl log = do
-  Lazy.for_ (filter (\msg => msg.lvl <= lvl) log.msgs) (putDoc . pretty)
-  case log.out of
-    Just v => pure v
-    Nothing => exitFailure
+logToTerminal lvl (Cont msg l) = do
+  () <- if msg.lvl <= lvl then putDoc (pretty msg) else pure ()
+  logToTerminal lvl l
+logToTerminal lvl Abort = exitFailure
+logToTerminal lvl (End v) = pure v
 
 export
 abort : Logging ann a
-abort = MkLogging Nothing []
+abort = Abort
+
+mapMsg : (Message ann -> Message ann') -> Logging ann a -> Logging ann' a
+mapMsg f (Cont msg l) = Cont (f msg) (mapMsg f l)
+mapMsg f Abort = Abort
+mapMsg f (End v) = End v
 
 export
 inScope : (tag : String) -> Logging ann a -> Logging ann a
-inScope tag = {msgs $= map {tags $= (tag ::)}}
+inScope tag = mapMsg {tags $= (tag ::)}
+
+export
+inBounds : Bounds -> Logging ann a -> Logging ann a
+inBounds bounds = mapMsg {bounds $= maybe (Just bounds) Just}
 
 public export
 interface Loggable (0 ann, ty : Type) where
@@ -122,27 +156,11 @@ error = log Error
 export
 fatal : Loggable ann ty => ty -> Logging ann a
 fatal msg = do error msg; abort
-  
+
 export
 Loggable ann (Doc ann) where
-  log lvl msg = MkLogging (pure ()) [MkMessage lvl msg []]
+  log lvl msg = Cont (MkMessage lvl msg Nothing []) $ End ()
 
 export
 Pretty x => Loggable ann x where
   log lvl msg = log lvl $ pretty {ann = ann} msg
-
-export
-Loggable ann x => Loggable ann (WithBounds x) where
-  log lvl msg =
-    let f : Logging ann () -> Logging ann ()
-        f = case msg.isIrrelevant of
-          True => id
-          False => inScope $
-            show (1 + msg.bounds.startLine) ++
-            ":" ++
-            show msg.bounds.startCol ++
-            "--" ++
-            show (1 + msg.bounds.endLine) ++
-            ":" ++
-            show msg.bounds.endCol
-    in f (log lvl msg.val)
diff --git a/src/Obs/Main.idr b/src/Obs/Main.idr
index fc7140a..4d7c856 100644
--- a/src/Obs/Main.idr
+++ b/src/Obs/Main.idr
@@ -54,7 +54,7 @@ main' : (input: String) -> Logging AnsiStyle (Exists NormalForm.Context)
 main' input = do
   defs <- parse input
   blk  <- abstractBlock defs
-  ctx  <- checkBlock blk
+  (_ ** (ctx, _)) <- checkBlock blk
   pure (Evidence _ ctx)
 
 partial
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index cf5bb61..a756728 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -1,6 +1,7 @@
 module Obs.NormalForm
 
-import Data.Fin
+import Data.List.Elem
+import Data.So
 
 import Obs.Sort
 import Obs.Substitution
@@ -12,328 +13,245 @@ import Text.PrettyPrint.Prettyprinter
 
 -- Definition ------------------------------------------------------------------
 
-data Constructor : Nat -> Type
-data Neutral     : Nat -> Type
-data NormalForm  : Nat -> Type
+data NormalForm  : Sorted.Family Bool
 
 public export
-data Constructor : Nat -> Type where
-  Sort   : Sort -> Constructor n
-  Pi     : Sort -> Sort -> String -> NormalForm n -> NormalForm (S n) -> Constructor n
-  Lambda : String -> NormalForm (S n) -> Constructor n
-  Sigma  : Sort -> Sort -> String -> NormalForm n -> NormalForm (S n) -> Constructor n
-  Pair   : NormalForm n -> NormalForm n -> Constructor n
-  Sum    : Sort -> Sort -> NormalForm n -> NormalForm n -> Constructor n
-  Left   : NormalForm n -> Constructor n
-  Right  : NormalForm n -> Constructor n
-  Container : Sort -> NormalForm n -> Sort -> Sort -> Constructor n
-  MkContainer : NormalForm n -> NormalForm n -> NormalForm n -> Constructor n
-  Top    : Constructor n
-  Bottom : Constructor n
+data Constructor : Unsorted.Family Bool where
+  Sort : (s : Sort) -> Constructor ctx
+  Pi : (s, s' : Sort)
+    -> (var : String)
+    -> (a : NormalForm True ctx)
+    -> (b : NormalForm True (isSet s :: ctx))
+    -> Constructor ctx
+  Lambda : (s : Sort)
+    -> (var : String)
+    -> NormalForm True (isSet s :: ctx)
+    -> Constructor ctx
+  Sigma : (s, s' : Sort)
+    -> (var : String)
+    -> (a : NormalForm True ctx)
+    -> (b : NormalForm True (isSet s :: ctx))
+    -> Constructor ctx
+  Pair : (s, s' : Sort)
+    -> (prf : So (isSet (max s s')))
+    -> NormalForm (isSet s) ctx
+    -> NormalForm (isSet s') ctx
+    -> Constructor ctx
+  Bool : Constructor ctx
+  True : Constructor ctx
+  False : Constructor ctx
+  Top : Constructor ctx
+  Bottom : Constructor ctx
 
 public export
-data Neutral : Nat -> Type where
-  Var    : String -> Fin n -> Neutral n
-  App    : Neutral n -> NormalForm n -> Neutral n
-  Fst    : Neutral n -> Neutral n
-  Snd    : Neutral n -> Neutral n
-  Case   : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
-  Tag    : Neutral n -> Neutral n
-  Position : Neutral n -> Neutral n
-  Next   : Neutral n -> Neutral n
-  Absurd : Neutral n
-  Equal  : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
-  EqualL : Nat -> Neutral n -> NormalForm n -> Neutral n
-  EqualR : Nat -> Constructor n -> Neutral n -> Neutral n
-  EqualU : Nat -> Constructor n -> Constructor n -> Neutral n
-  CastL  : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
-  CastR  : Constructor n -> Neutral n -> NormalForm n -> Neutral n
-  CastU  : Constructor n -> Constructor n -> NormalForm n -> Neutral n
+data Neutral : Unsorted.Family Bool where
+  Var : (var : String)
+    -> (sort : Sort)
+    -> (prf : So (isSet sort))
+    -> (i : Elem True 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
+  Absurd : Neutral ctx
+  Equal : Neutral ctx -> NormalForm True ctx -> NormalForm True ctx -> Neutral ctx
+  EqualL : (a : Neutral ctx) -> (b : NormalForm True 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 ->
+    Neutral ctx
+  CastR : (a : Constructor ctx) -> (b : Neutral ctx) -> NormalForm True ctx -> Neutral ctx
+  CastStuck : (a, b : Constructor ctx) -> NormalForm True ctx -> Neutral ctx
 
 public export
-data NormalForm : Nat -> Type where
-  Ntrl  : Neutral n -> NormalForm n
-  Cnstr : Constructor n -> NormalForm n
-  Irrel : NormalForm n
+data NormalForm : Sorted.Family Bool where
+  Ntrl : Neutral ~|> NormalForm True
+  Cnstr : Constructor ~|> NormalForm True
+  Irrel : NormalForm False ctx
+
+%name Constructor t, u, v
+%name Neutral t, u, v
+%name NormalForm t, u, v
 
 public export
-record Definition (n : Nat) where
+record Definition (ctx : List Bool) where
   constructor MkDefinition
-  name   : WithBounds String
-  sort   : Sort
-  ty     : NormalForm n
-  tm     : NormalForm n
+  name : WithBounds String
+  sort : Sort
+  ty   : NormalForm True ctx
+  tm   : NormalForm (isSet sort) ctx
 
 public export
-data Context : Nat -> Type where
-  Nil  : Context 0
-  (:<) : Context n -> Definition n -> Context (S n)
-
--- Interfaces ------------------------------------------------------------------
-
--- Naive equality tests
-eqCnstr : Constructor n -> Constructor n -> Bool
-eqNtrl  : Neutral n -> Neutral n -> Bool
-eqWhnf  : NormalForm n -> NormalForm n -> Bool
-
-eqCnstr (Sort s) (Sort s') = s == s'
-eqCnstr (Pi s s' _ a b) (Pi l l' _ a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
-eqCnstr (Lambda _ t) (Lambda _ u) = eqWhnf t u
-eqCnstr (Sigma s s' _ a b) (Sigma l l' _ a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
-eqCnstr (Pair t u) (Pair t' u') = eqWhnf t t' && eqWhnf u u'
-eqCnstr (Sum s s' a b) (Sum l l' a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
-eqCnstr (Left t) (Left t') = eqWhnf t t'
-eqCnstr (Right t) (Right t') = eqWhnf t t'
-eqCnstr (Container s a s' s'') (Container l a' l' l'') = s == l && eqWhnf a a' && s' == l' && s'' == l''
-eqCnstr (MkContainer t p f) (MkContainer t' p' f') = eqWhnf t t' && eqWhnf p p' && eqWhnf f f'
-eqCnstr Top Top = True
-eqCnstr Bottom Bottom = True
-eqCnstr _ _ = False
-
-eqNtrl (Var _ i) (Var _ j) = i == j
-eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u'
-eqNtrl (Fst t) (Fst t') = eqNtrl t t'
-eqNtrl (Snd t) (Snd t') = eqNtrl t t'
-eqNtrl (Case t f g) (Case t' f' g') = eqNtrl t t' && eqWhnf f f' && eqWhnf g g'
-eqNtrl (Tag t) (Tag t') = eqNtrl t t'
-eqNtrl (Position t) (Position t') = eqNtrl t t'
-eqNtrl (Next t) (Next t') = eqNtrl t t'
-eqNtrl Absurd Absurd = True
-eqNtrl (Equal a t u) (Equal a' t' u') = eqNtrl a a' && eqWhnf t t' && eqWhnf u u'
-eqNtrl (EqualL i t u) (EqualL j t' u') = i == j && eqNtrl t t' && eqWhnf u u'
-eqNtrl (EqualR i t u) (EqualR j t' u') = i == j && eqCnstr t t' && eqNtrl u u'
-eqNtrl (EqualU i t u) (EqualU j t' u') = i == j && eqCnstr t t' && eqCnstr u u'
-eqNtrl (CastL a b t) (CastL a' b' t') = eqNtrl a a' && eqWhnf b b' && eqWhnf t t'
-eqNtrl (CastR a b t) (CastR a' b' t') = eqCnstr a a' && eqNtrl b b' && eqWhnf t t'
-eqNtrl (CastU a b t) (CastU a' b' t') = eqCnstr a a' && eqCnstr b b' && eqWhnf t t'
-eqNtrl _ _ = False
-
-eqWhnf (Ntrl t)  (Ntrl u)  = eqNtrl t u
-eqWhnf (Cnstr t) (Cnstr u) = eqCnstr t u
-eqWhnf Irrel     Irrel     = True
-eqWhnf _ _ = False
-
-export
-Eq (Constructor n) where
-  t == u = eqCnstr t u
+data Context : List Bool -> Type where
+  Nil  : Context []
+  (:<) : Context ctx -> (def : Definition ctx) -> Context (isSet def.sort :: ctx)
 
-export
-Eq (Neutral n) where
-  t == u = eqNtrl t u
+%name Context ctx, ctx', ctx''
 
-export
-Eq (NormalForm n) where
-  t == u = eqWhnf t u
+-- Convenience Casts -----------------------------------------------------------
 
-export
-Cast Sort (Constructor n) where
-  cast = Sort
+public export
+Cast Sort (Constructor ctx) where
+  cast s = Sort s
 
-export
-Cast Sort (NormalForm n) where
-  cast = Cnstr . cast
+public export
+Cast Sort (NormalForm True ctx) where
+  cast s = Cnstr $ cast s
 
 -- Pretty Print ----------------------------------------------------------------
 
-prettyPrecCnstr : Prec -> Constructor n -> Doc ann
-prettyPrecNtrl  : Prec -> Neutral n -> Doc ann
-prettyPrecWhnf  : Prec -> NormalForm n -> Doc ann
+prettyPrec : Prec -> NormalForm b ctx -> Doc ann
 
+prettyPrecCnstr : Prec -> Constructor ctx -> Doc ann
 prettyPrecCnstr d (Sort s) = prettyPrec d s
-prettyPrecCnstr d (Pi _ _ var a b) =
+prettyPrecCnstr d (Pi s s' var a b) =
+  let lhs = case var of
+              "" => align (prettyPrec App a)
+              _ => parens (pretty var <++> colon <+> softline <+> align (prettyPrec Open a))
+  in
   parenthesise (d > Open) $
   group $
-  parens (pretty var <++> colon <+> softline <+> prettyPrecWhnf Open a) <++>
-  pretty "->" <+> softline <+>
-  prettyPrecWhnf Open b
-prettyPrecCnstr d (Lambda var t) =
+  lhs <++> pretty "->" <+> line <+> align (prettyPrec Open b)
+prettyPrecCnstr d (Lambda _ var t) =
   parenthesise (d > Open) $
   group $
   backslash <+> pretty var <++>
-  pretty "=>" <+> softline <+>
-  prettyPrecWhnf Open t
-prettyPrecCnstr d (Sigma _ _ var a b) =
+  pretty "=>" <+> line <+>
+  align (prettyPrec Open t)
+prettyPrecCnstr d (Sigma s s' var a b) =
+  let lhs = case var of
+              "" => align (prettyPrec App a)
+              _ => parens (pretty var <++> colon <+> softline <+> align (prettyPrec Open a))
+  in
   parenthesise (d > Open) $
   group $
-  parens (pretty var <++> colon <+> softline <+> prettyPrecWhnf Open a) <++>
-  pretty "**" <+> softline <+>
-  prettyPrecWhnf Open b
-prettyPrecCnstr d (Pair t u) =
+  lhs <++> pretty "**" <+> line <+> align (prettyPrec Open b)
+prettyPrecCnstr d (Pair s s' prf t u) =
   angles $
   group $
-  neutral <++> prettyPrecWhnf Open t <+> comma <+> softline <+> prettyPrecWhnf Open u <++> neutral
-prettyPrecCnstr d (Sum _ _ a b) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Either", prettyPrecWhnf App a, prettyPrecWhnf App b]
-prettyPrecCnstr d (Left t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Left", prettyPrecWhnf App t]
-prettyPrecCnstr d (Right t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Right", prettyPrecWhnf App t]
-prettyPrecCnstr d (Container s a s' s'') =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Container", prettyPrecWhnf App a, prettyPrec App s', prettyPrec App s'']
-prettyPrecCnstr d (MkContainer t p f) =
-  parenthesise (d >= User 0) $
-  group $
-  fillSep
-    [ prettyPrecWhnf (User 0) t <++> pretty "<|"
-    , prettyPrecWhnf (User 0) p <++> pretty "/"
-    , prettyPrecWhnf (User 0) f
-    ]
+  neutral <++> prettyPrec Open t <+> comma <+> line <+> prettyPrec Open u <++> neutral
+prettyPrecCnstr d Bool = pretty "Bool"
+prettyPrecCnstr d True = pretty "True"
+prettyPrecCnstr d False = pretty "False"
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
-prettyPrecNtrl d (Var var i) = pretty "\{show var}@\{show i}"
-prettyPrecNtrl d (App t u) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [prettyPrecNtrl Open t, prettyPrecWhnf App u]
-prettyPrecNtrl d (Fst t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "fst", prettyPrecNtrl App t]
-prettyPrecNtrl d (Snd t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "snd", prettyPrecNtrl App t]
-prettyPrecNtrl d (Case t f g) =
+prettyPrecNtrl : Prec -> Neutral ctx -> Doc ann
+prettyPrecNtrl d (Var var sort prf i) = pretty "\{var}@\{show $ elemToNat i}"
+prettyPrecNtrl d (App _ t u) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "case", prettyPrecNtrl App t, prettyPrecWhnf App f, prettyPrecWhnf App g]
-prettyPrecNtrl d (Tag t) =
+  vsep [prettyPrecNtrl Open t, prettyPrec App u]
+prettyPrecNtrl d (Fst _ t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "tag", prettyPrecNtrl App t]
-prettyPrecNtrl d (Position t) =
+  vsep [pretty "fst", prettyPrecNtrl App t]
+prettyPrecNtrl d (Snd _ t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "position", prettyPrecNtrl App t]
-prettyPrecNtrl d (Next t) =
+  vsep [pretty "snd", prettyPrecNtrl App t]
+prettyPrecNtrl d (If t f g) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "next", prettyPrecNtrl App t]
+  vsep [pretty "if", prettyPrecNtrl App t, prettyPrec App f, prettyPrec App g]
 prettyPrecNtrl d Absurd = pretty "absurd"
-prettyPrecNtrl d (Equal _ t u) =
+prettyPrecNtrl d (Equal a t u) =
   parenthesise (d >= Equal) $
   group $
-  prettyPrecWhnf Equal t <++> pretty "~" <+> softline <+> prettyPrecWhnf Equal u
-prettyPrecNtrl d (EqualL _ t u) =
+  prettyPrec Equal t <++> pretty "~" <+> line <+> prettyPrec Equal u
+prettyPrecNtrl d (EqualL a b) =
   parenthesise (d >= Equal) $
   group $
-  prettyPrecNtrl Equal t <++> pretty "~" <+> softline <+> prettyPrecWhnf Equal u
-prettyPrecNtrl d (EqualR _ t u) =
+  prettyPrecNtrl Equal a <++> pretty "~" <+> line <+> prettyPrec Equal b
+prettyPrecNtrl d (EqualR a b) =
   parenthesise (d >= Equal) $
   group $
-  prettyPrecCnstr Equal t <++> pretty "~" <+> softline <+> prettyPrecNtrl Equal u
-prettyPrecNtrl d (EqualU _ t u) =
+  prettyPrecCnstr Equal a <++> pretty "~" <+> line <+> prettyPrecNtrl Equal b
+prettyPrecNtrl d (EqualStuck a b) =
   parenthesise (d >= Equal) $
   group $
-  prettyPrecCnstr Equal t <++> pretty "~" <+> softline <+> prettyPrecCnstr Equal u
+  prettyPrecCnstr Equal a <++> pretty "~" <+> line <+> prettyPrecCnstr Equal b
 prettyPrecNtrl d (CastL a b t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "cast", prettyPrecNtrl App a, prettyPrecWhnf App b, prettyPrecWhnf App t]
+  vsep [pretty "cast", prettyPrecNtrl App a, prettyPrec App b, prettyPrec App t]
 prettyPrecNtrl d (CastR a b t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "cast", prettyPrecCnstr App a, prettyPrecNtrl App b, prettyPrecWhnf App t]
-prettyPrecNtrl d (CastU a b t) =
+  vsep [pretty "cast", prettyPrecCnstr App a, prettyPrecNtrl App b, prettyPrec App t]
+prettyPrecNtrl d (CastStuck a b t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "cast", prettyPrecCnstr App a, prettyPrecCnstr App b, prettyPrecWhnf App t]
+  vsep [pretty "cast", prettyPrecCnstr App a, prettyPrecCnstr App b, prettyPrec App t]
 
-prettyPrecWhnf d (Ntrl t)  = prettyPrecNtrl d t
-prettyPrecWhnf d (Cnstr t) = prettyPrecCnstr d t
-prettyPrecWhnf d Irrel     = pretty "_"
+prettyPrec d (Ntrl t) = prettyPrecNtrl d t
+prettyPrec d (Cnstr t) = prettyPrecCnstr d t
+prettyPrec d Irrel = pretty "_"
 
 export
-Pretty (Constructor n) where
+Pretty (Constructor ctx) where
   prettyPrec = prettyPrecCnstr
 
 export
-Pretty (Neutral n) where
+Pretty (Neutral ctx) where
   prettyPrec = prettyPrecNtrl
 
 export
-Pretty (NormalForm n) where
-  prettyPrec = prettyPrecWhnf
+Pretty (NormalForm b ctx) where
+  prettyPrec = NormalForm.prettyPrec
 
-export
-Pretty (Definition n) where
-  pretty def = group $
-    pretty def.name.val <++> colon <+> softline <+> pretty def.ty <+> softline <+> colon <++> pretty def.sort <+> hardline <+>
-    pretty def.name.val <++> equals <+> softline <+> pretty def.tm
-
-export
-Pretty (Context n) where
-  pretty []           = neutral
-  pretty ([] :< def)  = pretty def
-  pretty (ctx :< def) = pretty ctx <+> hardline <+> hardline <+> pretty def
-
--- Operations ------------------------------------------------------------------
+-- Renaming --------------------------------------------------------------------
 
--- Renaming
-
-renameCnstr : Constructor n -> (Fin n -> Fin m) -> Constructor m
-renameNtrl  : Neutral n -> (Fin n -> Fin m) -> Neutral m
-renameWhnf  : NormalForm n -> (Fin n -> Fin m) -> NormalForm m
+rename : NormalForm ~|> Hom Elem NormalForm
 
+renameCnstr : Constructor ~|> Hom Elem Constructor
 renameCnstr (Sort s) f = Sort s
-renameCnstr (Pi s s' var a b) f = Pi s s' var (renameWhnf a f) (renameWhnf b $ lift 1 f)
-renameCnstr (Lambda var t) f = Lambda var (renameWhnf t $ lift 1 f)
-renameCnstr (Sigma s s' var a b) f = Sigma s s' var (renameWhnf a f) (renameWhnf b $ lift 1 f)
-renameCnstr (Pair t u) f = Pair (renameWhnf t f) (renameWhnf u f)
-renameCnstr (Sum s s' a b) f = Sum s s' (renameWhnf a f) (renameWhnf b f)
-renameCnstr (Left t) f = Left (renameWhnf t f)
-renameCnstr (Right t) f = Right (renameWhnf t f)
-renameCnstr (Container s a s' s'') f = Container s (renameWhnf a f) s' s''
-renameCnstr (MkContainer t p u) f = MkContainer (renameWhnf t f) (renameWhnf p f) (renameWhnf u f)
+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 =
+  Sigma s s' var (rename a f) (rename b (lift [(_ ** ())] f))
+renameCnstr (Pair s s' prf t u) f = Pair s s' prf (rename t f) (rename u f)
+renameCnstr Bool f = Bool
+renameCnstr True f = True
+renameCnstr False f = False
 renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom
 
-renameNtrl (Var var i) f = Var var (f i)
-renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f)
-renameNtrl (Fst t) f = Fst (renameNtrl t f)
-renameNtrl (Snd t) f = Snd (renameNtrl t f)
-renameNtrl (Case t u t') f = Case (renameNtrl t f) (renameWhnf u f) (renameWhnf t' f)
-renameNtrl (Tag t) f = Tag (renameNtrl t f)
-renameNtrl (Position t) f = Position (renameNtrl t f)
-renameNtrl (Next t) f = Next (renameNtrl t f)
+renameNtrl : Neutral ~|> Hom Elem Neutral
+renameNtrl (Var var sort prf i) f = Var var sort prf (f i)
+renameNtrl (App b t u) f = App b (renameNtrl t f) (rename u f)
+renameNtrl (Fst b t) f = Fst b (renameNtrl t f)
+renameNtrl (Snd b t) f = Snd b (renameNtrl t f)
+renameNtrl (If t u v) f = If (renameNtrl t f) (rename u f) (rename v f)
 renameNtrl Absurd f = Absurd
-renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (renameWhnf t f) (renameWhnf u f)
-renameNtrl (EqualL i t u) f = EqualL i (renameNtrl t f) (renameWhnf u f)
-renameNtrl (EqualR i t u) f = EqualR i (renameCnstr t f) (renameNtrl u f)
-renameNtrl (EqualU i t u) f = EqualU i (renameCnstr t f) (renameCnstr u f)
-renameNtrl (CastL a b t) f = CastL (renameNtrl a f) (renameWhnf b f) (renameWhnf t f)
-renameNtrl (CastR a b t) f = CastR (renameCnstr a f) (renameNtrl b f) (renameWhnf t f)
-renameNtrl (CastU a b t) f = CastU (renameCnstr a f) (renameCnstr b f) (renameWhnf t f)
-
-renameWhnf (Ntrl t)  f = Ntrl $ renameNtrl t f
-renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f
-renameWhnf Irrel     f = Irrel
+renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (rename t f) (rename u f)
+renameNtrl (EqualL a b) f = EqualL (renameNtrl a f) (rename b f)
+renameNtrl (EqualR a b) f = EqualR (renameCnstr a f) (renameNtrl b f)
+renameNtrl (EqualStuck a b) f = EqualStuck (renameCnstr a f) (renameCnstr b f)
+renameNtrl (CastL a b t) f = CastL (renameNtrl a f) (rename b f) (rename t f)
+renameNtrl (CastR a b t) f = CastR (renameCnstr a f) (renameNtrl b f) (rename t f)
+renameNtrl (CastStuck a b t) f = CastStuck (renameCnstr a f) (renameCnstr b f) (rename t f)
+
+rename (Ntrl t) f = Ntrl $ renameNtrl t f
+rename (Cnstr t) f = Cnstr $ renameCnstr t f
+rename Irrel f = Irrel
 
 export
-Rename Constructor where
+Unsorted.Rename Bool Constructor where
   rename = renameCnstr
 
 export
-Rename Neutral where
+Unsorted.Rename Bool Neutral where
   rename = renameNtrl
-
-export
-Rename NormalForm where
-  rename = renameWhnf
-
+  
 export
-PointedRename Neutral where
-  point = Var ""
+Sorted.Rename Bool NormalForm where
+  rename = NormalForm.rename
 
 export
-PointedRename NormalForm where
-  point = Ntrl . point
+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)
diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr
index b50b520..82e84b9 100644
--- a/src/Obs/NormalForm/Normalise.idr
+++ b/src/Obs/NormalForm/Normalise.idr
@@ -1,400 +1,309 @@
 module Obs.NormalForm.Normalise
 
-import Data.Vect
+import Data.Bool
+import Data.So
+
+import Decidable.Equality
 
 import Obs.Logging
 import Obs.NormalForm
 import Obs.Sort
 import Obs.Substitution
 
--- Utilities -------------------------------------------------------------------
+import Text.PrettyPrint.Prettyprinter
+
+%default total
+
+-- Aliases ---------------------------------------------------------------------
+
+public export 0
+LogConstructor : Type -> Unsorted.Family Bool
+LogConstructor ann ctx = Logging ann (Constructor ctx)
+
+public export 0
+LogNormalForm : Type -> Sorted.Family Bool
+LogNormalForm ann b ctx = Logging ann (NormalForm b ctx)
+
+0
+LogNormalForm' : Type -> Sorted.Family Bool
+LogNormalForm' ann b ctx = Either (Logging ann (NormalForm b ctx)) (Elem b ctx)
 
-mergeName : String -> String -> String
-mergeName "" s' = s'
-mergeName "_" s' = s'
-mergeName s s' = s
+-- Copied and specialised from Obs.Substitution
+lift : (ctx : List (b ** (String, (s ** isSet s = b))))
+  -> Map ctx' (LogNormalForm' ann) ctx''
+  -> Map (map DPair.fst ctx ++ ctx') (LogNormalForm' ann) (map DPair.fst ctx ++ ctx'')
+lift [] f = f
+lift ((s ** y) :: ctx) f = add (LogNormalForm' ann)
+  (Left $ pure $ point y Here)
+  (\i => bimap (\t => pure (rename !t There)) There (lift ctx f i))
 
-wkn : Vect k String -> (Fin n -> Logging ann (NormalForm m)) -> Fin (k + n) -> Logging ann (NormalForm (k + m))
-wkn []            f = f
-wkn (var :: vars) f =
-  add
-    (Logging ann . NormalForm)
-    (pure $ Ntrl $ Var var FZ)
-    (\i => pure $ rename !(wkn vars f i) FS)
+-- Normalisation ---------------------------------------------------------------
+
+subst' : NormalForm ~|> Hom (LogNormalForm' ann) (LogNormalForm ann)
+
+export
+doApp : {b' : _} -> NormalForm b ctx -> NormalForm b' ctx -> LogNormalForm ann b 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"
+  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
-expandContainerTy : Sort -> NormalForm n -> Sort -> Sort -> Constructor n
-expandContainerTy s a s' s'' =
-  let tagTy : Constructor n
-      tagTy = Pi s (suc s') "i" a (cast s')
-  in
-  let posTy : Constructor (S n)
-      posTy =
-        Pi s (s' ~> suc s'') "i"
-          (weaken 1 a)
-          (Cnstr $ Pi s' (suc s'') "t"
-            (Ntrl $ App (Var "tag" 1) (Ntrl $ Var "i" 0))
-            (cast s''))
-  in
-  let nextTy : Constructor (2 + n)
-      nextTy =
-        Pi s (s' ~> suc s'' ~> s) "i"
-          (weaken 2 a)
-          (Cnstr $ Pi s' (suc s'' ~> s) "t"
-            (Ntrl $ App (Var "tag" 2) (Ntrl $ Var "i" 0))
-            (Cnstr $ Pi (suc s'') s "p"
-              (Ntrl $ App (App (Var "pos" 2) (Ntrl $ Var "i" 1)) (Ntrl $ Var "p" 0))
-              (weaken 5 a)))
-  in
-  Sigma (s ~> suc s') (lub (s ~> s' ~> suc s'') (s ~> s' ~> s'' ~> s)) "tag"
-    (Cnstr tagTy) $
-  Cnstr $ Sigma (s ~> s' ~> suc s'') (s ~> s' ~> s'' ~> s) "pos"
-    (Cnstr posTy)
-    (Cnstr nextTy)
+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
 
--- Substitution ----------------------------------------------------------------
+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
+  in case t' of
+  Ntrl t => pure (Ntrl $ Snd b t)
+  Cnstr (Pair _ (Set _) prf t u) => pure u
+  Cnstr t => inScope "wrong constructor for snd" $ fatal t
 
-partial
-substCnstr : Constructor n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (Constructor m)
-partial
-substNtrl  : Neutral n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m)
-partial export
-subst      : NormalForm n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m)
-partial export
-subst1     : NormalForm n -> NormalForm (S n) -> Logging ann (NormalForm n)
-partial export
-doApp      : NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-partial export
-doFst      : NormalForm n -> Logging ann (NormalForm n)
-partial export
-doSnd      : NormalForm n -> Logging ann (NormalForm n)
-partial export
-doCase     : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-partial export
-doTag      : NormalForm n -> Logging ann (NormalForm n)
-partial export
-doPosition : NormalForm n -> Logging ann (NormalForm n)
-partial export
-doNext     : NormalForm n -> Logging ann (NormalForm n)
-partial export
-doEqual    : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-partial
-doEqualL   : Nat -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-partial
-doEqualR   : Nat -> Constructor n -> NormalForm n -> Logging ann (NormalForm n)
-partial
-doEqualU   : Nat -> Constructor n -> Constructor n -> Logging ann (NormalForm n)
-partial export
-doCastL    : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-partial
-doCastR    : Constructor n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-partial
-doCastU    : Constructor n -> Constructor n -> NormalForm n -> Logging ann (NormalForm n)
-partial export
-expandContainer : NormalForm n -> Logging ann (Constructor n)
-partial export
-contractContainer : NormalForm n -> Logging ann (Constructor n)
+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
 
-substCnstr (Sort s) f = pure $ Sort s
+export
+doAbsurd : (b : _) -> NormalForm b ctx
+doAbsurd False = Irrel
+doAbsurd True = Ntrl Absurd
+
+export
+doCast : (b' : _) -> (a, b : NormalForm True ctx) -> NormalForm b' ctx -> LogNormalForm ann b' ctx
+
+doCastR : (a : Constructor ctx) ->
+  (b : NormalForm True ctx) ->
+  NormalForm True ctx ->
+  LogNormalForm ann True ctx
+doCastR a (Ntrl b) t = pure (Ntrl $ CastR a b t)
+doCastR (Sort _) (Cnstr (Sort _)) 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)
+      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)
+  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)
+  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)
+  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)
+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)
+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
+
+export
+doEqual : (b : _) ->
+  (a : NormalForm True ctx) ->
+  NormalForm b ctx ->
+  NormalForm b ctx ->
+  LogNormalForm ann True ctx
+
+-- Relies heavily on typing
+doEqualR : (a : Constructor ctx) -> (b : NormalForm True ctx) -> LogNormalForm ann True ctx
+doEqualR a (Ntrl b) = pure (Ntrl $ EqualR a b)
+doEqualR (Sort _) (Cnstr (Sort 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)
+      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
+  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))
+doEqualR ty@(Sigma s s' var a b) (Cnstr ty'@(Sigma l l' _ a' b')) =
+  let t : NormalForm (isSet s) (isSet 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
+  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))
+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 (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
+  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)
+      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
+  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
+  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
+  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
+
+substCnstr : Constructor ~|> Hom (LogNormalForm' ann) (LogConstructor ann)
+substCnstr (Sort s) f = pure (Sort s)
 substCnstr (Pi s s' var a b) f = do
-  a <- subst a f
-  b <- subst b (wkn [var] f)
+  a <- subst' a f
+  b <- subst' b (lift [(_ ** (var, (s ** Refl)))] f)
   pure (Pi s s' var a b)
-substCnstr (Lambda var t) f = do
-  t <- subst t (wkn [var] f)
-  pure (Lambda var t)
+substCnstr (Lambda s var t) f = do
+  t <- subst' t (lift [(_ ** (var, (s ** Refl)))] f)
+  pure (Lambda s var t)
 substCnstr (Sigma s s' var a b) f = do
-  a <- subst a f
-  b <- subst b (wkn [var] f)
+  a <- subst' a f
+  b <- subst' b (lift [(_ ** (var, (s ** Refl)))] f)
   pure (Sigma s s' var a b)
-substCnstr (Pair t u) f = do
-  t <- subst t f
-  u <- subst u f
-  pure (Pair t u)
-substCnstr (Sum s s' a b) f = do
-  a <- subst a f
-  b <- subst b f
-  pure (Sum s s' a b)
-substCnstr (Left t) f = do
-  t <- subst t f
-  pure (Left t)
-substCnstr (Right t) f = do
-  t <- subst t f
-  pure (Right t)
-substCnstr (Container s a s' s'') f = do
-  a <- subst a f
-  pure (Container s a s' s'')
-substCnstr (MkContainer t p u) f = do
-  t <- subst t f
-  p <- subst p f
-  u <- subst u f
-  pure (MkContainer t p u)
-substCnstr Top f = pure $ Top
-substCnstr Bottom  f = pure $ Bottom
-
-substNtrl (Var var i) f = do
-  Ntrl (Var var' j) <- f i
-    | t => pure t
-  pure (Ntrl (Var (mergeName var' var) j))
-substNtrl (App t u) f = do
-  t <- substNtrl t f
-  u <- subst u f
-  doApp t u
-substNtrl (Fst t) f = do
-  t <- substNtrl t f
-  doFst t
-substNtrl (Snd t) f = do
+substCnstr (Pair s s' prf t u) f = do
+  t <- subst' t f
+  u <- subst' u f
+  pure (Pair s s' prf t u)
+substCnstr Bool f = pure Bool
+substCnstr True f = pure True
+substCnstr False f = pure False
+substCnstr Top f = pure Top
+substCnstr Bottom f = pure Bottom
+
+substNtrl : Neutral ~|> Hom (LogNormalForm' ann) (LogNormalForm ann True)
+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
   t <- substNtrl t f
-  doSnd t
-substNtrl (Case t u t') f = do
+  u <- subst' u f
+  assert_total (doApp t u)
+substNtrl (Fst b t) f = do
   t <- substNtrl t f
-  u <- subst u f
-  t' <- subst t' f
-  doCase t u t'
-substNtrl (Tag t) f = do
+  doFst True b t
+substNtrl (Snd b t) f = do
   t <- substNtrl t f
-  doTag t
-substNtrl (Position t) f = do
+  doSnd b True $ rewrite orTrueTrue b in t
+substNtrl (If t u v) f = do
   t <- substNtrl t f
-  doPosition t
-substNtrl (Next t) f = do
-  t <- substNtrl t f
-  doNext t
-substNtrl Absurd f = pure $ Ntrl Absurd
+  u <- subst' u f
+  v <- subst' v f
+  doIf t u v
+substNtrl Absurd f = pure (doAbsurd True)
 substNtrl (Equal a t u) f = do
   a <- substNtrl a f
-  t <- subst t f
-  u <- subst u f
-  doEqual a t u
-substNtrl (EqualL i t u) f = do
-  t <- substNtrl t f
-  u <- subst u f
-  doEqualL i t u
-substNtrl (EqualR i t u) f = do
-  t <- substCnstr t f
-  u <- substNtrl u f
-  doEqualR i t u
-substNtrl (EqualU i t u) f = do
-  t <- substCnstr t f
-  u <- substCnstr u f
-  doEqualU i t u
+  t <- subst' t f
+  u <- subst' u f
+  doEqual _ a t u
+substNtrl (EqualL a b) f = do
+  a <- substNtrl a f
+  b <- subst' b f
+  doEqualSet a b
+substNtrl (EqualR a b) f = do
+  a <- substCnstr a f
+  b <- substNtrl b f
+  doEqualR a b
+substNtrl (EqualStuck a b) f = do
+  a <- substCnstr a f
+  b <- substCnstr b f
+  pure (Ntrl $ EqualStuck a b)
 substNtrl (CastL a b t) f = do
   a <- substNtrl a f
-  b <- subst b f
-  t <- subst t f
-  doCastL a b t
+  b <- subst' b f
+  t <- subst' t f
+  doCast _ a b t
 substNtrl (CastR a b t) f = do
   a <- substCnstr a f
   b <- substNtrl b f
-  t <- subst t f
+  t <- subst' t f
   doCastR a b t
-substNtrl (CastU a b t) f = do
+substNtrl (CastStuck a b t) f = do
   a <- substCnstr a f
   b <- substCnstr b f
-  t <- subst t f
-  doCastU a b t
-
-subst (Ntrl t)  f = substNtrl t f
-subst (Cnstr t) f = map Cnstr $ substCnstr t f
-subst Irrel     f = pure Irrel
-
-subst1 t u = subst u (add (Logging ann . NormalForm) (pure t) (pure . point))
-
-doApp (Ntrl t) u = pure $ Ntrl (App t u)
-doApp Irrel u = pure $ Irrel
-doApp (Cnstr (Lambda var t)) u = subst t (add (Logging ann . NormalForm) (pure u) (pure . point))
-doApp (Cnstr t) u = inScope "bug" $ inScope "wrong constructor in apply" $ fatal t
-
-doFst (Ntrl t) = pure $ Ntrl (Fst t)
-doFst Irrel = pure $ Irrel
-doFst (Cnstr (Pair t u)) = pure $ t
-doFst (Cnstr t) = inScope "bug" $ inScope "wrong constructor in fst" $ fatal t
-
-doSnd (Ntrl t) = pure $ Ntrl (Snd t)
-doSnd Irrel = pure $ Irrel
-doSnd (Cnstr (Pair t u)) = pure $ u
-doSnd (Cnstr t) = inScope "bug" $ inScope "wrong constructor in snd" $ fatal t
-
-doCase (Ntrl t) f g = pure $ Ntrl (Case t f g)
-doCase Irrel f g = inScope "bug" $ inScope "wrong constructor in case" $ fatal "Irrel"
-doCase (Cnstr (Left t)) f g = doApp f t
-doCase (Cnstr (Right t)) f g = doApp g t
-doCase (Cnstr t) f g = inScope "bug" $ inScope "wrong constructor in case" $ fatal t
-
-doTag (Ntrl t) = pure $ Ntrl (Tag t)
-doTag Irrel = pure $ Irrel
-doTag (Cnstr (MkContainer t p f)) = pure t
-doTag (Cnstr t) = inScope "bug" $ inScope "wrong constructor in tag" $ fatal t
-
-doPosition (Ntrl t) = pure $ Ntrl (Position t)
-doPosition Irrel = pure $ Irrel
-doPosition (Cnstr (MkContainer t p f)) = pure p
-doPosition (Cnstr t) = inScope "bug" $ inScope "wrong constructor in position" $ fatal t
+  t <- subst' t f
+  pure (Ntrl $ CastStuck a b t)
 
-doNext (Ntrl t) = pure $ Ntrl (Next t)
-doNext Irrel = pure $ Irrel
-doNext (Cnstr (MkContainer t p f)) = pure f
-doNext (Cnstr t) = inScope "bug" $ inScope "wrong constructor in next" $ fatal t
-
-doEqual (Ntrl a) t u = pure $ Ntrl (Equal a t u)
-doEqual Irrel t u = inScope "bug" $ inScope "wrong type over equal" $ fatal "Irrel"
-doEqual (Cnstr (Sort Prop)) t u =
-  pure $
-  Cnstr (Sigma Prop Prop "_"
-    (Cnstr $ Pi Prop Prop "_" t (weaken 1 u))
-    (weaken 1 $ Cnstr $ Pi Prop Prop "_" u (weaken 1 t)))
-doEqual (Cnstr (Sort (Set k))) t u = doEqualL k t u
-doEqual (Cnstr (Pi s s' var a b)) t u = do
-  eqLhs <- doApp (weaken 1 t) (Ntrl $ Var var FZ)
-  eqRhs <- doApp (weaken 1 u) (Ntrl $ Var var FZ)
-  eq <- doEqual b eqLhs eqRhs -- b in Set because Pi in Set.
-  pure $ Cnstr (Pi s Prop var a eq)
-doEqual (Cnstr (Sigma s s' var a b)) t u = do
-  t1 <- doFst t
-  u1 <- doFst u
-  eq1 <- case s of
-    Prop => pure $ Cnstr Top
-    (Set i) => doEqual a t1 u1
-  eq2 <- case s' of
-    Prop => pure $ Cnstr Top
-    (Set i) => do
-      bt <- subst1 t1 b
-      bu <- subst1 u1 b
-      t2 <- doSnd t
-      t2 <- doCastL bt bu t2
-      u2 <- doSnd u
-      doEqual bu t2 u2
-  pure $ Cnstr (Sigma Prop Prop "_" eq1 (weaken 1 eq2))
-doEqual (Cnstr (Sum s s' a b)) t u = do
-  let x = Ntrl $ Var "x" 1
-  let y = Ntrl $ Var "y" 0
-  ll <- doEqual (weaken 2 a) x y
-  lr <- pure $ Cnstr Bottom
-  rl <- pure $ Cnstr Bottom
-  rr <- doEqual (weaken 2 b) x y
-  fBody <- doCase (weaken 1 u) (Cnstr (Lambda "y" ll)) (Cnstr (Lambda "y" lr))
-  gBody <- doCase (weaken 1 u) (Cnstr (Lambda "y" rl)) (Cnstr (Lambda "y" rr))
-  doCase t (Cnstr (Lambda "x" fBody)) (Cnstr (Lambda "x" gBody))
-doEqual (Cnstr (Container s a s' s'')) t u = do
-  let containerTy = expandContainerTy s a s' s''
-  t <- expandContainer t
-  u <- expandContainer u
-  doEqual (Cnstr containerTy) (Cnstr t) (Cnstr u)
-doEqual (Cnstr Top) t u = pure $ Cnstr Top
-doEqual (Cnstr Bottom) t u = pure $ Cnstr Top
-doEqual (Cnstr a) t u = inScope "bug" $ inScope "wrong type under equal" $ fatal a
-
-doEqualL i (Ntrl t) u = pure $ Ntrl (EqualL i t u)
-doEqualL i Irrel u = inScope "bug" $ inScope "wrong type under equalL" $ fatal "Irrel"
-doEqualL i (Cnstr t) u = doEqualR i t u
-
-doEqualR i t (Ntrl u) = pure $ Ntrl (EqualR i t u)
-doEqualR i t Irrel = inScope "bug" $ inScope "wrong type under equalR" $ fatal "Irrel"
-doEqualR i t (Cnstr u) = doEqualU i t u
-
-doEqualU i (Sort s) (Sort s') = pure $ Cnstr Top -- have suc s = i = suc s', and suc injective
-doEqualU i (Pi s s' _ a b) (Pi l l' var a' b') = case (s == s' && l == l') of
-  False => pure $ Cnstr Bottom
-  True => do
-    eqLhs <- doEqual (cast s) a' a
-    let x = Ntrl $ Var var FZ
-    b <- subst b (add (Logging ann . NormalForm) (doCastL (weaken 1 a') (weaken 1 a) x) (pure . Ntrl . Var "" . FS))
-    eqRhs <- doEqual (cast s') b b'
-    pure $ Cnstr (Sigma Prop Prop "" eqLhs $ weaken 1 $ Cnstr (Pi s Prop var a' eqRhs))
-doEqualU i (Sigma s s' _ a b) (Sigma l l' var a' b') = case (s == s' && l == l') of
-  False => pure $ Cnstr Bottom
-  True => do
-    eqLhs <- doEqual (cast s) a' a
-    let x = Ntrl $ Var var FZ
-    b <- subst b (add (Logging ann . NormalForm) (doCastL (weaken 1 a') (weaken 1 a) x) (pure . Ntrl . Var "" . FS))
-    eqRhs <- doEqual (cast s') b b'
-    pure $ Cnstr (Sigma Prop Prop "" eqLhs $ weaken 1 $ Cnstr (Pi s Prop var a' eqRhs))
-doEqualU i (Sum s s' a b) (Sum l l' a' b') = case (s == l && s' == l') of
-  False => pure $ Cnstr Bottom
-  True => do
-    eqLhs <- doEqual (cast s) a a'
-    eqRhs <- doEqual (cast s) b b'
-    pure $ Cnstr (Sigma Prop Prop "" eqLhs (weaken 1 eqRhs))
-doEqualU i (Container s a s' s'') (Container l a' l' l'') = case (s == l && s' == l' && s'' == l'') of
-  False => pure $ Cnstr Bottom
-  True => doEqual (cast s) a a'
-doEqualU i t u = pure $ Ntrl (EqualU i t u) -- assumption: only logical values reach this far
-
-doCastL (Ntrl a) b t = pure $ Ntrl (CastL a b t)
-doCastL Irrel b t = inScope "bug" $ inScope "wrong type for cast" $ fatal "Irrel"
-doCastL (Cnstr a) b t = doCastR a b t
-
-doCastR a (Ntrl b) t = pure $ Ntrl (CastR a b t)
-doCastR a Irrel t = inScope "bug" $ inScope "wrong type for cast" $ fatal "Irrel"
-doCastR a (Cnstr b) t = doCastU a b t
-
-doCastU (Sort s) (Sort s') t = pure t
-doCastU (Pi s s' _ a b) (Pi l l' var a' b') t = do
-  let x' = Ntrl $ Var var FZ
-  let x = doCastL (weaken 1 a') (weaken 1 a) x'
-  b <- subst b (add (Logging ann . NormalForm) x (pure . Ntrl . Var "" . FS))
-  b' <- subst b' (add (Logging ann . NormalForm) (pure x') (pure . Ntrl . Var "" . FS))
-  fx <- doApp (weaken 1 t) !x
-  cast <- doCastL b b' fx
-  pure $ Cnstr (Lambda var cast)
-doCastU (Sigma s s' _ a b) (Sigma l l' var a' b') t = do
-  t1 <- doFst t
-  t2 <- doSnd t
-  t1' <- doCastL a a' t1
-  b <- subst1 t1 b
-  b' <- subst1 t1' b'
-  t2' <- doCastL b b' t2
-  pure $ Cnstr (Pair t1' t2')
-doCastU (Sum s s' a b) (Sum l l' a' b') t = do
-  let x = Ntrl $ Var "x" 0
-  castL <- doCastL (weaken 1 a) (weaken 1 a') x
-  castR <- doCastL (weaken 1 b) (weaken 1 b') x
-  doCase t (Cnstr (Lambda "x" (Cnstr (Left castL)))) (Cnstr (Lambda "x" (Cnstr (Right castR))))
-doCastU (Container s a s' s'') (Container l b l' l'') t = do
-  t <- expandContainer t
-  let a = expandContainerTy s a s' s''
-  let b = expandContainerTy l b l' l''
-  t <- doCastU a b (Cnstr t)
-  t <- contractContainer t
-  pure $ Cnstr t
-doCastU Top Top t = pure Irrel
-doCastU Bottom Bottom t = pure Irrel
-doCastU a b t = pure $ Ntrl (CastU a b t)
-
-expandContainer t = do
-  tag <- doTag t
-  pos <- doPosition t
-  next <- doNext t
-  pure $ Pair tag (Cnstr $ Pair pos next)
-
-contractContainer t = do
-  tag <- doFst t
-  t <- doSnd t
-  pos <- doFst t
-  next <- doSnd t
-  pure $ MkContainer tag pos next
-
--- More utilities --------------------------------------------------------------
+subst' (Ntrl t) f = substNtrl t f
+subst' (Cnstr t) f = pure $ Cnstr !(substCnstr t f)
+subst' Irrel f = pure Irrel
 
 export
-tagTy : Sort -> NormalForm n -> Sort -> Constructor n
-tagTy s a s' = Pi s (suc s') "i" a (cast s')
+subst : NormalForm ~|> Hom (LogNormalForm ann) (LogNormalForm ann)
+subst t f = subst' t (Left . f)
 
-export
-positionTy : Sort -> NormalForm n -> Sort -> NormalForm n -> Sort -> Logging ann (Constructor n)
-positionTy s a s' tag s'' = do
-  let i = Var "i" 0
-  tagI <- doApp (weaken 1 tag) (Ntrl i)
-  pure $ Pi s (s' ~> suc s'') "i" a (Cnstr $ Pi s' (suc s'') "t" tagI (cast s''))
+-- Utilities -------------------------------------------------------------------
 
 export
-nextTy : Sort -> NormalForm n -> Sort -> NormalForm n -> Sort -> NormalForm n -> Logging ann (Constructor n)
-nextTy s a s' tag s'' pos = do
-  let i = Var "i" 0
-  tagI <- doApp (weaken 1 tag) (Ntrl i)
-  let t = Var "t" 0
-  posI <- doApp (weaken 1 pos) (Ntrl i)
-  posIT <- doApp (weaken 1 posI) (Ntrl t)
-  pure $ Pi s (s' ~> s'' ~> s) "i" a $
-  Cnstr $ Pi s' (s'' ~> s) "t" tagI $
-  Cnstr $ Pi s'' s "p" posIT (weaken 3 a)
+subst1 : {s' : _} -> NormalForm s ctx -> NormalForm s' (s :: ctx) -> LogNormalForm ann s' ctx
+subst1 t u = subst' u (add (LogNormalForm' ann) (Left $ pure t) Right)
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 7ce31c4..758b019 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -25,10 +25,10 @@ data ObsTokenKind
   | OTNat
   | OTFst
   | OTSnd
-  | OTEither
-  | OTLeft
-  | OTRight
-  | OTCase
+  | OTBool
+  | OTTrue
+  | OTFalse
+  | OTIf
   | OTContainer
   | OTTag
   | OTPosition
@@ -70,10 +70,10 @@ Eq ObsTokenKind where
   OTNat == OTNat = True
   OTFst == OTFst = True
   OTSnd == OTSnd = True
-  OTEither == OTEither = True
-  OTLeft == OTLeft = True
-  OTRight == OTRight = True
-  OTCase == OTCase = True
+  OTBool == OTBool = True
+  OTTrue == OTTrue = True
+  OTFalse == OTFalse = True
+  OTIf == OTIf = True
   OTContainer == OTContainer = True
   OTTag == OTTag = True
   OTPosition == OTPosition = True
@@ -117,10 +117,10 @@ TokenKind ObsTokenKind where
   tokValue OTNat s = stringToNatOrZ s
   tokValue OTFst s = ()
   tokValue OTSnd s = ()
-  tokValue OTEither s = ()
-  tokValue OTLeft s = ()
-  tokValue OTRight s = ()
-  tokValue OTCase s = ()
+  tokValue OTBool s = ()
+  tokValue OTTrue s = ()
+  tokValue OTFalse s = ()
+  tokValue OTIf s = ()
   tokValue OTContainer s = ()
   tokValue OTTag s = ()
   tokValue OTPosition s = ()
@@ -162,10 +162,10 @@ Show ObsToken where
   show (Tok OTNat s) = s
   show (Tok OTFst s) = "fst"
   show (Tok OTSnd s) = "snd"
-  show (Tok OTEither s) = "Either"
-  show (Tok OTLeft s) = "Left"
-  show (Tok OTRight s) = "Right"
-  show (Tok OTCase s) = "case"
+  show (Tok OTBool s) = "Bool"
+  show (Tok OTTrue s) = "True"
+  show (Tok OTFalse s) = "False"
+  show (Tok OTIf s) = "if"
   show (Tok OTContainer s) = "Container"
   show (Tok OTTag s) = "tag"
   show (Tok OTPosition s) = "position"
@@ -204,10 +204,10 @@ keywords =
   , ("Prop", OTProp)
   , ("fst", OTFst)
   , ("snd", OTSnd)
-  , ("Either", OTEither)
-  , ("Left", OTLeft)
-  , ("Right", OTRight)
-  , ("case", OTCase)
+  , ("Bool", OTBool)
+  , ("True", OTTrue)
+  , ("False", OTFalse)
+  , ("if", OTIf)
   , ("Container", OTContainer)
   , ("tag", OTTag)
   , ("position", OTPosition)
@@ -256,7 +256,10 @@ uncurry (S n) f (x :: xs) = uncurry n (f x) xs
 
 termForms : List (ObsTokenKind, Syntax)
 termForms =
-  [ (OTPoint, Point)
+  [ (OTBool, Bool)
+  , (OTTrue, True)
+  , (OTFalse, False)
+  , (OTPoint, Point)
   , (OTVoid, Bottom)
   , (OTUnit, Top)
   ]
@@ -265,22 +268,18 @@ headForms : List (ObsTokenKind, (n ** (Vect (S n) (WithBounds Syntax) -> Syntax)
 headForms =
   [ (OTFst, (0 ** uncurry 1 Fst))
   , (OTSnd, (0 ** uncurry 1 Snd))
-  , (OTEither, (1 ** uncurry 2 Sum))
-  , (OTLeft, (0 ** uncurry 1 Left))
-  , (OTRight, (0 ** uncurry 1 Right))
-  , (OTCase, (4 ** uncurry 5 Case))
-  , (OTContainer, (2 ** uncurry 3 Container))
-  , (OTTag, (0 ** uncurry 1 Tag))
-  , (OTPosition, (0 ** uncurry 1 Position))
-  , (OTNext, (0 ** uncurry 1 Next))
-  , (OTSem, (2 ** uncurry 3 Sem))
-  , (OTAbsurd, (1 ** uncurry 2 Absurd))
+  , (OTAbsurd, (0 ** uncurry 1 Absurd))
   , (OTRefl, (0 ** uncurry 1 Refl))
-  , (OTTransp, (4 ** uncurry 5 Transp))
-  , (OTCast, (2 ** uncurry 3 Cast))
+  , (OTTransp, (4 ** (uncurry 5 Transp)))
+  , (OTCast, (3 ** uncurry 4 Cast))
   , (OTCastRefl, (0 ** uncurry 1 CastId))
   ]
 
+headLambdaForms : List (ObsTokenKind, (n ** ((WithBounds String, WithBounds Syntax) -> Vect n (WithBounds Syntax) -> Syntax)))
+headLambdaForms =
+  [ (OTIf, (3 ** (uncurry 3 . uncurry If)))
+  ]
+
 declForms : List (ObsTokenKind, (WithBounds String -> op (WithBounds Syntax) Syntax 2))
 declForms = [(OTThinArrow, Pi), (OTProduct, Sigma)]
 
@@ -321,6 +320,11 @@ pair p =
       (optional whitespace *> p <* optional whitespace) |]
   <* match OTAClose <* commit
 
+lambda : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (WithBounds String, a)
+lambda p =
+  match OTBackslash *> commit *>
+  [| MkPair (ident <* whitespace <* match OTFatArrow <* whitespace) p |]
+
 partial
 noSortsTerm : Grammar state ObsToken True (WithBounds Syntax)
 partial
@@ -349,30 +353,25 @@ head =
   map (map Sort) sort <|>
   bounds
     (choiceMap
+      (\(hd, (n ** f)) => match hd *> commit *>
+        [| f (whitespace *> parens (lambda exp)) (count n (whitespace *> term))|])
+      headLambdaForms) <|>
+  bounds
+    (choiceMap
       (\(hd, (n ** f)) => match hd *> commit *> [| f (count (S n) (whitespace *> term)) |])
       headForms)
 
 spine = map (uncurry $ foldl (\t, u => joinBounds (map (\_ => map (\_ => App t u) u) t))) $
   [| MkPair head (many (whitespace *> term)) |]
 
-container =
-  map (\bounds@(MkBounded (t, u) _ _) => case u of
-    Nothing => t
-    Just (p, f) => map (\_ => MkContainer t p f) bounds) $
-  bounds $
-  [| MkPair spine
-      (optional
-        [| MkPair
-            (whitespace *> match OTTriangle *> commit *> whitespace *> spine)
-            (whitespace *> match OTSlash *> commit *> whitespace *> spine)
-        |])
-  |]
+container = spine
 
 equals = map (\(t, u) => maybe t (\u => joinBounds (map (\_ => map (\_ => Equal t u) u) t)) u) $
   [| MkPair container (optional (whitespace *> match OTTilde *> commit *> whitespace *> container)) |]
 
 exp =
   equals <|>
+  bounds (map (uncurry Lambda) $ lambda exp) <|>
   bounds
     (map (\((var, a), (b, f)) => f var a b) $
      [| MkPair
@@ -380,11 +379,7 @@ exp =
           (choiceMap
             (\(op, f) => match op *> commit *> whitespace *> [| MkPair exp (pure f) |])
             declForms)
-     |]) <|>
-  bounds
-    (map (uncurry Lambda) $
-     match OTBackslash *> commit *>
-     [| MkPair (ident <* whitespace <* match OTFatArrow <* whitespace) exp |])
+     |])
 
 partial
 def : Grammar state ObsToken True (WithBounds String, WithBounds Syntax)
@@ -404,8 +399,8 @@ partial
 file : Grammar state ObsToken False (List Definition)
 file =
   optional (whitespace *> match OTNewlines) *>
-  sepEndBy (optional whitespace *> match OTNewlines) (fullDef <* commit) <*
-  eof
+  sepEndBy (optional whitespace *> match OTNewlines) (fullDef <* commit)
+  -- <* eof
 
 whitespaceIrrelevant : WithBounds ObsToken -> WithBounds ObsToken
 whitespaceIrrelevant a = case (a.val.kind) of
@@ -429,12 +424,7 @@ castErr : Either (List1 (ParsingError tok)) a -> Logging ann a
 castErr (Right x) = pure x
 castErr (Left errs) = do
   for_ {b = ()} errs
-    (\(Error msg bounds) =>
-      error $
-      maybe
-        (irrelevantBounds $ msg)
-        (\bounds => MkBounded msg False bounds) $
-      bounds)
+    (\(Error msg bounds) => maybe id inBounds bounds $ error msg)
   abort
 
 partial
@@ -442,8 +432,14 @@ export
 parse : String -> Logging ann (List Definition)
 parse str = do
   let (toks, _, _, "") = lex obsTokenMap str
-    | (_, l, c, rem) => inScope "lex" $ fatal "failed to lex input"
+    | (toks, l, c, rem) => inScope "lex" $ do
+      error "failed to lex input"
+      trace (map (\tok => show tok.val) toks)
+      trace (show rem)
+      abort
   let toks = preprocess toks
   (defs, []) <- inScope "parse" $ castErr $ parse file $ toks
-    | (_, ts) => inScope "parse" $ fatal "unparsed tokens"
+    | (_, ts) => inScope "parse" $ do
+      trace (map (show . val) ts)
+      fatal "unparsed tokens"
   pure defs
diff --git a/src/Obs/Substitution.idr b/src/Obs/Substitution.idr
index 340afff..22a7272 100644
--- a/src/Obs/Substitution.idr
+++ b/src/Obs/Substitution.idr
@@ -1,43 +1,83 @@
 module Obs.Substitution
 
-import Data.Fin
+import public Data.List.Elem
 
 %default total
 
-public export
-interface Rename (0 x : Nat -> Type) where
-  rename : forall m, n . x n -> (Fin n -> Fin m) -> x m
+infix 5 ~|>
 
-public export
-interface Rename x => PointedRename x where
-  point : forall n . Fin n -> x n
+namespace Sorted
+  public export 0
+  Family : Type -> Type
+  Family a = a -> List a -> Type
 
-public export
-interface Subst (0 x, y, z : Nat -> Type) where
-  subst : forall m, n . x n -> (Fin n -> y m) -> z m
+  public export 0
+  Map : List a -> Family a -> List a -> Type
+  Map ctx x ctx' = {s : a} -> Elem s ctx -> x s ctx'
 
-public export
-Rename x => Subst x Fin x where
-  subst = rename
+  public export 0
+  Hom : Family a -> Family a -> Family a
+  Hom x y s ctx = forall ctx' . Map ctx x ctx' -> y s ctx'
+
+  public export 0
+  (~|>) : Family a -> Family a -> Type
+  x ~|> y = forall ctx . {s : a} -> x s ctx -> y s ctx
+
+  public export
+  interface Rename (0 a : _) (0 x : Family a) | x where
+    rename : x ~|> Hom Elem x
+
+  public export
+  interface Rename a x => PointedRename a (0 b : a -> Type) x | x where
+    point : forall ctx . {s : a} -> b s -> Elem s ctx -> x s ctx
+
+namespace Unsorted
+  public export 0
+  Family : Type -> Type
+  Family a = List a -> Type
+
+  public export 0
+  Hom : Sorted.Family a -> Unsorted.Family a -> Unsorted.Family a
+  Hom x y ctx = forall ctx' . Map ctx x ctx' -> y ctx'
+
+  public export 0
+  (~|>) : Unsorted.Family a -> Unsorted.Family a -> Type
+  x ~|> y = forall ctx . x ctx -> y ctx
+
+  public export
+  interface Rename (0 a : _) (0 x : Unsorted.Family a) | x where
+    rename : x ~|> Hom Elem x
 
 public export
-Rename Fin where
+Sorted.Rename a Elem where
   rename i f = f i
 
 public export
-PointedRename Fin where
-  point = id
+PointedRename a (const ()) Elem where
+  point _ = id
 
 public export
-add : (0 x : _) -> x n -> (Fin m -> x n) -> Fin (S m) -> x n
-add x v f FZ     = v
-add x v f (FS i) = f i
+add : (0 x : Sorted.Family a) -> x s' ctx' -> Map ctx x ctx' -> Map (s' :: ctx) x ctx'
+add x v f Here      = v
+add x v f (There i) = f i
 
 public export
-lift : PointedRename x => (k : _) -> (Fin m -> x n) -> Fin (k + m) -> x (k + n)
-lift 0     f = f
-lift (S k) f = add x (point FZ) (\i => rename (lift k f i) FS)
+lift : PointedRename a b x => (ctx : List (s ** b s))
+  -> Map ctx' x ctx''
+  -> Map (map DPair.fst ctx ++ ctx') x (map DPair.fst ctx ++ ctx'')
+lift [] f = f
+lift ((s ** y) :: ctx) f = add x (point y Here) (\i => rename (lift ctx f i) There)
 
-public export
-weaken : Rename x => (m : _) -> x n -> x (m + n)
-weaken m t = rename t (shift m)
+elemAppRight : (xs : List a) -> (0 ys : List a) -> Elem x ys -> Elem.Elem x (xs ++ ys)
+elemAppRight [] _ = id
+elemAppRight (x :: xs) ys = There . elemAppRight xs ys
+
+namespace Sorted
+  export
+  weaken : Sorted.Rename a x => (ctx : _) -> x ~|> (\s, ctx' => x s (ctx ++ ctx'))
+  weaken ctx t = rename t (elemAppRight ctx _)
+
+namespace Unsorted
+  export
+  weaken : Unsorted.Rename a x => (ctx : _) -> x ~|> (\ctx' => x (ctx ++ ctx'))
+  weaken ctx t = rename t (elemAppRight ctx _)
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index d21569a..7bf4b61 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -2,6 +2,7 @@
 module Obs.Syntax
 
 import Obs.Sort
+
 import Text.Bounded
 import Text.PrettyPrint.Prettyprinter
 
@@ -11,41 +12,34 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Syntax : Type where
-  Var    : String -> Syntax
+  Var : String -> Syntax
   -- Sorts
-  Sort   : Sort -> Syntax
+  Sort : Sort -> Syntax
   -- Dependent Products
-  Pi     : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Pi : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
   Lambda : WithBounds String -> WithBounds Syntax -> Syntax
-  App    : WithBounds Syntax -> WithBounds Syntax -> Syntax
+  App : WithBounds Syntax -> WithBounds Syntax -> Syntax
   -- Dependent Sums
-  Sigma  : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
-  Pair   : WithBounds Syntax -> WithBounds Syntax -> Syntax
-  Fst    : WithBounds Syntax -> Syntax
-  Snd    : WithBounds Syntax -> Syntax
-  -- Disjoint Coproducts
-  Sum    : WithBounds Syntax -> WithBounds Syntax -> Syntax
-  Left   : WithBounds Syntax -> Syntax
-  Right  : WithBounds Syntax -> Syntax
-  Case   : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
-  -- Containers
-  Container : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
-  MkContainer : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
-  Tag : WithBounds Syntax -> Syntax
-  Position : WithBounds Syntax -> Syntax
-  Next : WithBounds Syntax -> Syntax
-  Sem : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Sigma : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Pair : WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Fst : WithBounds Syntax -> Syntax
+  Snd : WithBounds Syntax -> Syntax
+  -- Booleans
+  Bool : Syntax
+  True : Syntax
+  False : Syntax
+  If : WithBounds String -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
   -- True
-  Top    : Syntax
-  Point  : Syntax
+  Top : Syntax
+  Point : Syntax
   -- False
   Bottom : Syntax
-  Absurd : WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Absurd : WithBounds Syntax -> Syntax
   -- Equality
-  Equal  : WithBounds Syntax -> WithBounds Syntax -> Syntax
-  Refl   : WithBounds Syntax -> Syntax
+  Equal : WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Refl : WithBounds Syntax -> Syntax
   Transp : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
-  Cast   : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Cast : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
   CastId : WithBounds Syntax -> Syntax
 
 public export
@@ -65,115 +59,94 @@ prettyPrec d (Sort s) = prettyPrec d s
 prettyPrec d (Pi var a b) =
   parenthesise (d > Open) $
   group $
-  parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
-  pretty "->" <+> softline <+>
-  prettyPrecBounds Open b
+  parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++>
+  pretty "->" <+> line <+>
+  align (prettyPrecBounds Open b)
 prettyPrec d (Lambda var t) =
   parenthesise (d > Open) $
   group $
   backslash <+> pretty var.val <++>
-  pretty "=>" <+> softline <+>
-  prettyPrecBounds Open t
+  pretty "=>" <+> line <+>
+  align (prettyPrecBounds Open t)
 prettyPrec d (App t u) =
   parenthesise (d >= App) $
   group $
-  fillSep [prettyPrecBounds Open t, prettyPrecBounds App u]
+  vsep [prettyPrecBounds Open t, prettyPrecBounds App u]
 prettyPrec d (Sigma var a b) =
   parenthesise (d >= App) $
   group $
-  parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
-  pretty "**" <+> softline <+>
-  prettyPrecBounds Open b
+  parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++>
+  pretty "**" <+> line <+>
+  align (prettyPrecBounds Open b)
 prettyPrec d (Pair t u) =
   angles $
   group $
-  neutral <++> prettyPrecBounds Open t <+> comma <+> softline <+> prettyPrecBounds Open u <++> neutral
+  neutral <++> prettyPrecBounds Open t <+> comma <+> line <+> prettyPrecBounds Open u <++> neutral
 prettyPrec d (Fst t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "fst", prettyPrecBounds App t]
+  vsep [pretty "fst", prettyPrecBounds App t]
 prettyPrec d (Snd t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "snd", prettyPrecBounds App t]
-prettyPrec d (Sum a b) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Either", prettyPrecBounds App a, prettyPrecBounds App b]
-prettyPrec d (Left t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Left", prettyPrecBounds App t]
-prettyPrec d (Right t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Right", prettyPrecBounds App t]
-prettyPrec d (Case t s b f g) =
+  vsep [pretty "snd", prettyPrecBounds App t]
+prettyPrec d Bool = pretty "Bool"
+prettyPrec d True = pretty "True"
+prettyPrec d False = pretty "False"
+prettyPrec d (If var a t f g) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "case", prettyPrecBounds App t, prettyPrecBounds App s, prettyPrecBounds App b, prettyPrecBounds App f, prettyPrecBounds App g]
-prettyPrec d (Container a s s') =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Container", prettyPrecBounds App a, prettyPrecBounds App s, prettyPrecBounds App s']
-prettyPrec d (MkContainer t p f) =
-  parenthesise (d >= User 0) $
-  group $
-  fillSep
-    [ prettyPrecBounds (User 0) t <++> pretty "<|"
-    , prettyPrecBounds (User 0) p <++> pretty "/"
-    , prettyPrecBounds (User 0) f
-    ]
-prettyPrec d (Tag t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "tag", prettyPrecBounds App t]
-prettyPrec d (Position t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "position", prettyPrecBounds App t]
-prettyPrec d (Next t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "next", prettyPrecBounds App t]
-prettyPrec d (Sem s a t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "sem", prettyPrecBounds App s, prettyPrecBounds App a, prettyPrecBounds App t]
+  vsep $
+  [ pretty "if"
+  , parens $
+    group $
+    backslash <+> pretty var.val <++>
+    pretty "=>" <+> line <+>
+    align (prettyPrecBounds Open a)
+  , prettyPrecBounds App t
+  , prettyPrecBounds App f
+  , prettyPrecBounds App g
+  ]
 prettyPrec d Top = pretty "()"
 prettyPrec d Point = pretty "tt"
 prettyPrec d Bottom = pretty "Void"
-prettyPrec d (Absurd a t) =
+prettyPrec d (Absurd t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "absurd", prettyPrecBounds App a, prettyPrecBounds App t]
+  vsep [pretty "absurd", prettyPrecBounds App t]
 prettyPrec d (Equal t u) =
   parenthesise (d >= Equal) $
   group $
-  prettyPrecBounds Equal t <++> pretty "~" <+> softline <+> prettyPrecBounds Equal u
+  prettyPrecBounds Equal t <++> pretty "~" <+> line <+> prettyPrecBounds Equal u
 prettyPrec d (Refl t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "refl", prettyPrecBounds App t]
-prettyPrec d (Transp t b u t' e) =
+  vsep [pretty "refl", prettyPrecBounds App t]
+prettyPrec d (Transp a t u t' e) =
   parenthesise (d >= App) $
   group $
-  fillSep $
+  vsep $
   [ pretty "transp"
+  , prettyPrecBounds App a
   , prettyPrecBounds App t
-  , prettyPrecBounds App b
   , prettyPrecBounds App u
   , prettyPrecBounds App t'
   , prettyPrecBounds App e
   ]
-prettyPrec d (Cast b e t) =
+prettyPrec d (Cast a b e t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "cast", prettyPrecBounds App b, prettyPrecBounds App e, prettyPrecBounds App t]
+  vsep $
+  [ pretty "cast"
+  , prettyPrecBounds App a
+  , prettyPrecBounds App b
+  , prettyPrecBounds App e
+  , prettyPrecBounds App t
+  ]
 prettyPrec d (CastId t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "castRefl", prettyPrecBounds App t]
+  vsep [pretty "castRefl", prettyPrecBounds App t]
 
 prettyPrecBounds d (MkBounded val _ _) = prettyPrec d val
 
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 10f2129..422af87 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,41 +12,48 @@ import Text.PrettyPrint.Prettyprinter
 
 public export
 data Term : Nat -> Type where
-  Var    : String -> Fin n -> Term n
+  Var : String -> Fin n -> Term n
   -- Sorts
-  Sort   : Sort -> Term n
+  Sort : Sort -> Term n
   -- Dependent Product
-  Pi     : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
+  Pi : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
   Lambda : WithBounds String -> WithBounds (Term (S n)) -> Term n
-  App    : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  App : WithBounds (Term n) -> WithBounds (Term n) -> Term n
   -- Dependent Sums
-  Sigma  : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
-  Pair   : WithBounds (Term n) -> WithBounds (Term n) -> Term n
-  Fst    : WithBounds (Term n) -> Term n
-  Snd    : WithBounds (Term n) -> Term n
-  -- Disjoint Coproducts
-  Sum    : WithBounds (Term n) -> WithBounds (Term n) -> Term n
-  Left   : WithBounds (Term n) -> Term n
-  Right  : WithBounds (Term n) -> Term n
-  Case   : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
-  -- Containers
-  Container : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
-  MkContainer : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
-  Tag : WithBounds (Term n) -> Term n
-  Position : WithBounds (Term n) -> Term n
-  Next : WithBounds (Term n) -> Term n
-  Sem : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Sigma : WithBounds String -> WithBounds (Term n) -> WithBounds (Term (S n)) -> Term n
+  Pair : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Fst : WithBounds (Term n) -> Term n
+  Snd : WithBounds (Term n) -> Term n
+  -- Booleans
+  Bool : Term n
+  True : Term n
+  False : Term n
+  If : WithBounds String ->
+    WithBounds (Term (S n)) ->
+    WithBounds (Term n) ->
+    WithBounds (Term n) ->
+    WithBounds (Term n) ->
+    Term n
   -- True
-  Top    : Term n
-  Point  : Term n
+  Top : Term n
+  Point : Term n
   -- False
   Bottom : Term n
-  Absurd : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Absurd : WithBounds (Term n) -> Term n
   -- Equality
-  Equal  : WithBounds (Term n) -> WithBounds (Term n) -> Term n
-  Refl   : WithBounds (Term n) -> Term n
-  Transp : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
-  Cast   : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Equal : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Refl : WithBounds (Term n) -> Term n
+  Transp : WithBounds (Term n) ->
+    WithBounds (Term n) ->
+    WithBounds (Term n) ->
+    WithBounds (Term n) ->
+    WithBounds (Term n) ->
+    Term n
+  Cast : WithBounds (Term n) ->
+    WithBounds (Term n) ->
+    WithBounds (Term n) ->
+    WithBounds (Term n) ->
+    Term n
   CastId : WithBounds (Term n) -> Term n
 
 public export
@@ -71,115 +78,94 @@ prettyPrec d (Sort s) = prettyPrec d s
 prettyPrec d (Pi var a b) =
   parenthesise (d > Open) $
   group $
-  parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
-  pretty "->" <+> softline <+>
-  prettyPrecBounds Open b
+  parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++>
+  pretty "->" <+> line <+>
+  align (prettyPrecBounds Open b)
 prettyPrec d (Lambda var t) =
   parenthesise (d > Open) $
   group $
   backslash <+> pretty var.val <++>
-  pretty "=>" <+> softline <+>
-  prettyPrecBounds Open t
+  pretty "=>" <+> line <+>
+  align (prettyPrecBounds Open t)
 prettyPrec d (App t u) =
   parenthesise (d >= App) $
   group $
-  fillSep [prettyPrecBounds Open t, prettyPrecBounds App u]
+  vsep [prettyPrecBounds Open t, prettyPrecBounds App u]
 prettyPrec d (Sigma var a b) =
   parenthesise (d >= App) $
   group $
-  parens (pretty var.val <++> colon <+> softline <+> prettyPrecBounds Open a) <++>
-  pretty "**" <+> softline <+>
-  prettyPrecBounds Open b
+  parens (pretty var.val <++> colon <+> softline <+> align (prettyPrecBounds Open a)) <++>
+  pretty "**" <+> line <+>
+  align (prettyPrecBounds Open b)
 prettyPrec d (Pair t u) =
   angles $
   group $
-  neutral <++> prettyPrecBounds Open t <+> comma <+> softline <+> prettyPrecBounds Open u <++> neutral
+  neutral <++> prettyPrecBounds Open t <+> comma <+> line <+> prettyPrecBounds Open u <++> neutral
 prettyPrec d (Fst t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "fst", prettyPrecBounds App t]
+  vsep [pretty "fst", prettyPrecBounds App t]
 prettyPrec d (Snd t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "snd", prettyPrecBounds App t]
-prettyPrec d (Sum a b) =
+  vsep [pretty "snd", prettyPrecBounds App t]
+prettyPrec d Bool = pretty "Bool"
+prettyPrec d True = pretty "True"
+prettyPrec d False = pretty "False"
+prettyPrec d (If var a t f g) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "Either", prettyPrecBounds App a, prettyPrecBounds App b]
-prettyPrec d (Left t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Left", prettyPrecBounds App t]
-prettyPrec d (Right t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Right", prettyPrecBounds App t]
-prettyPrec d (Case t s b f g) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "case", prettyPrecBounds App t, prettyPrecBounds App s, prettyPrecBounds App b, prettyPrecBounds App f, prettyPrecBounds App g]
-prettyPrec d (Container a s s') =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "Container", prettyPrecBounds App a, prettyPrecBounds App s, prettyPrecBounds App s']
-prettyPrec d (MkContainer t p f) =
-  parenthesise (d >= User 0) $
-  group $
-  fillSep
-    [ prettyPrecBounds (User 0) t <++> pretty "<|"
-    , prettyPrecBounds (User 0) p <++> pretty "/"
-    , prettyPrecBounds (User 0) f
-    ]
-prettyPrec d (Tag t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "tag", prettyPrecBounds App t]
-prettyPrec d (Position t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "position", prettyPrecBounds App t]
-prettyPrec d (Next t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "next", prettyPrecBounds App t]
-prettyPrec d (Sem s a t) =
-  parenthesise (d >= App) $
-  group $
-  fillSep [pretty "sem", prettyPrecBounds App s, prettyPrecBounds App a, prettyPrecBounds App t]
+  vsep $
+  [ pretty "if"
+  , parens $
+    group $
+    backslash <+> pretty var.val <++>
+    pretty "=>" <+> line <+>
+    align (prettyPrecBounds Open a)
+  , prettyPrecBounds App t
+  , prettyPrecBounds App f
+  , prettyPrecBounds App g
+  ]
 prettyPrec d Top = pretty "()"
 prettyPrec d Point = pretty "tt"
 prettyPrec d Bottom = pretty "Void"
-prettyPrec d (Absurd a t) =
+prettyPrec d (Absurd t) =
   parenthesise (d > Open) $
   group $
-  fillSep [pretty "absurd", prettyPrecBounds App a, prettyPrecBounds App t]
+  vsep [pretty "absurd", prettyPrecBounds App t]
 prettyPrec d (Equal t u) =
   parenthesise (d >= Equal) $
   group $
-  prettyPrecBounds Equal t <++> pretty "~" <+> softline <+> prettyPrecBounds Equal u
+  prettyPrecBounds Equal t <++> pretty "~" <+> line <+> prettyPrecBounds Equal u
 prettyPrec d (Refl t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "refl", prettyPrecBounds App t]
-prettyPrec d (Transp t b u t' e) =
+  vsep [pretty "refl", prettyPrecBounds App t]
+prettyPrec d (Transp a t u t' e) =
   parenthesise (d >= App) $
   group $
-  fillSep $
+  vsep $
   [ pretty "transp"
+  , prettyPrecBounds App a
   , prettyPrecBounds App t
-  , prettyPrecBounds App b
   , prettyPrecBounds App u
   , prettyPrecBounds App t'
   , prettyPrecBounds App e
   ]
-prettyPrec d (Cast b e t) =
+prettyPrec d (Cast a b e t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "cast", prettyPrecBounds App b, prettyPrecBounds App e, prettyPrecBounds App t]
+  vsep $
+  [ pretty "cast"
+  , prettyPrecBounds App a
+  , prettyPrecBounds App b
+  , prettyPrecBounds App e
+  , prettyPrecBounds App t
+  ]
 prettyPrec d (CastId t) =
   parenthesise (d >= App) $
   group $
-  fillSep [pretty "castRefl", prettyPrecBounds App t]
+  vsep [pretty "castRefl", prettyPrecBounds App t]
 
 prettyPrecBounds d (MkBounded v _ _) = prettyPrec d v
 
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index f814f93..4cc6d8e 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -1,6 +1,10 @@
 module Obs.Typing
 
-import Data.Vect
+import Control.Monad.Maybe
+
+import Data.Nat
+
+import Decidable.Equality
 
 import Obs.Logging
 import Obs.NormalForm
@@ -8,6 +12,7 @@ import Obs.NormalForm.Normalise
 import Obs.Sort
 import Obs.Substitution
 import Obs.Term
+import Obs.Typing.Context
 import Obs.Typing.Conversion
 
 import System
@@ -20,384 +25,255 @@ import Text.PrettyPrint.Prettyprinter.Render.Terminal
 
 -- Loggings ----------------------------------------------------------------------
 
-Rename (Logging ann . NormalForm) where
-  rename t f = pure $ rename !t f
-
-mismatch : Bounds -> Doc ann -> Doc ann -> Logging ann a
-mismatch bounds lhs rhs = fatal $
-  MkBounded
-    (pretty "expected" <++> lhs <+> comma <+> softline <+> pretty "got" <++> rhs)
-    False
-    bounds
-
-typeMismatch : Bounds -> Doc ann -> Doc ann -> Logging ann a
-typeMismatch bounds lhs rhs = inScope "type mismatch" $ mismatch bounds lhs rhs
-
-sortMismatch : Bounds -> Doc ann -> Doc ann -> Logging ann a
-sortMismatch bounds lhs rhs = inScope "sort mismatch" $ mismatch bounds lhs rhs
+mismatch : (expected, got : Doc ann) -> Logging ann a
+mismatch lhs rhs = fatal $
+  hang 2 (pretty "expected" <+> line <+> lhs) <+> comma <+> line <+>
+  hang 2 (pretty "got" <+> line <+> align rhs)
 
--- Typing Contexts -------------------------------------------------------------
+typeMismatch : Doc ann -> Doc ann -> Logging ann a
+typeMismatch lhs rhs = inScope "type mismatch" $ mismatch lhs rhs
 
-infix 5 ::<
+sortMismatch : Doc ann -> Doc ann -> Logging ann a
+sortMismatch lhs rhs = inScope "sort mismatch" $ mismatch lhs rhs
 
-data TyContext : Nat -> Nat -> Type where
-  Nil   : TyContext 0 0
-  (:<)  : TyContext m n -> NormalForm.Definition n -> TyContext m (S n)
-  (::<) : TyContext m n -> (String, NormalForm n, Sort) -> TyContext (S m) (S n)
+-- Utilities -------------------------------------------------------------------
 
-fromContext : Context n -> TyContext 0 n
-fromContext []           = []
-fromContext (ctx :< def) = fromContext ctx :< def
+MkPair : (s, s' : Sort)
+  -> NormalForm (isSet s) ctx
+  -> NormalForm (isSet s') ctx
+  -> NormalForm (isSet (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
 
-countVars : TyContext m n -> Fin (S n)
-countVars []          = FZ
-countVars (ctx :< y)  = weaken $ countVars ctx
-countVars (ctx ::< y) = FS $ countVars ctx
+-- Checking and Inference ------------------------------------------------------
 
-index : TyContext m n -> Fin n -> (NormalForm n, NormalForm n, Sort)
-index (ctx :< def)              FZ     = (weaken 1 def.tm, weaken 1 def.ty, def.sort)
-index (ctx ::< (var, ty, Prop)) FZ     = (Irrel, weaken 1 ty, Prop)
-index (ctx ::< (var, ty, s))    FZ     = (Ntrl $ Var var FZ, weaken 1 ty, s)
-index (ctx :< _)                (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
-index (ctx ::< _)               (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
+check : (tyCtx : TyContext ctx)
+  -> (s : Sort)
+  -> NormalForm True ctx
+  -> WithBounds (Term (length ctx))
+  -> Logging ann (NormalForm (isSet s) ctx)
 
-partial
-asSubst : (ctx : TyContext m n) -> Fin n -> Logging ann (NormalForm m)
-asSubst (ctx :< def)             FZ     = subst def.tm (asSubst ctx)
-asSubst (ctx ::< (var, _, Prop)) FZ     = pure Irrel
-asSubst (ctx ::< (var, _, _))    FZ     = pure $ Ntrl (Var var FZ)
-asSubst (ctx :< def)             (FS i) = asSubst ctx i
-asSubst (ctx ::< _)              (FS i) = map (weaken 1) (asSubst ctx i)
+checkType : (tyCtx : TyContext ctx)
+  -> (s : Sort)
+  -> WithBounds (Term (length ctx))
+  -> Logging ann (NormalForm True ctx)
+checkType ctx s tm = check ctx (suc s) (cast s) tm
 
--- Checking and Inference ------------------------------------------------------
+infer : (tyCtx : TyContext ctx)
+  -> WithBounds (Term (length ctx))
+  -> Logging ann (s ** (NormalForm True ctx, NormalForm (isSet s) ctx))
 
-partial
-check : TyContext m n -> WithBounds (Term n) -> NormalForm n -> Sort -> Logging ann (NormalForm n)
-partial
-infer : TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, NormalForm n, Sort)
-partial
-inferType : {default typeMismatch tag : forall a . Bounds -> Doc ann -> Doc ann -> Logging ann a}
-  -> TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, Sort)
-partial
-inferSort : TyContext m n -> WithBounds (Term n) -> Logging ann Sort
+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)
+inferType ctx tm = inBounds tm.bounds $ do
+  (Set _ ** (Cnstr (Sort s), a)) <- infer ctx tm
+    | (_ ** (a, t)) => tag (pretty "sort") (pretty a)
+  pure (s, a)
 
-check ctx tm ty s = case (tm.val, ty) of
-  (Lambda _ t, Cnstr (Pi s s' var a b)) => do
-    inScope "check" $ trace $ map (\_ => pretty {ann} "checking under lambda with type" <++> pretty a) tm
-    inScope "check" $ trace $ map (\_ => "binding new variable to \{var}") tm
-    inScope "check" $ trace $ map (\_ => pretty {ann} "checking for type" <++> pretty b) tm
-    t <- check (ctx ::< (var, a, s)) t b s'
-    case s' of
-      Prop => pure Irrel
-      _ => pure (Cnstr $ Lambda var t)
-  (Lambda _ _, ty) => typeMismatch tm.bounds (pretty "pi") (pretty ty)
-  (Pair t u, Cnstr (Sigma s s' var a b)) => do
-    inScope "check" $ trace $ map (\_ => "checking pair") tm
-    inScope "check" $ trace $ map (\_ => pretty {ann} "checking first for type" <++> pretty a) tm
-    t <- check ctx t a s
+check ctx s ty tm = inBounds tm.bounds $ case (ty, tm.val) of
+  (Cnstr (Pi l l' _ a b), Lambda var t) => do
+    info "encountered lambda"
+    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"
+    pure $ case l' of
+      Prop => Irrel
+      Set _ => Cnstr (Lambda l var.val t)
+  (_, Lambda var t) => typeMismatch (pretty "function") (pretty ty)
+  (Cnstr (Sigma l l' var a b), Pair t u) => do
+    info "encountered pair"
+    trace $ pretty {ann} "checking first has type" <++> pretty a
+    t <- check ctx l a (assert_smaller tm t)
     b <- subst1 t b
-    inScope "check" $ trace $ map (\_ => pretty {ann} "checking second for type" <++> pretty b) tm
-    u <- check ctx u b s'
-    inScope "check" $ trace $ map (\_ => pretty {ann} "pair is well typed") tm
-    case (s, s') of
-      (Prop, Prop) => pure Irrel
-      _ => pure (Cnstr $ Pair t u)
-  (Pair _ _, ty) => typeMismatch tm.bounds (pretty "sigma") (pretty ty)
-  (Left t, Cnstr (Sum s s' a b)) => do
-    inScope "check" $ trace $ map (\_ => "checking left injection") tm
-    inScope "check" $ trace $ map (\_ => pretty {ann} "checking subterm for type" <++> pretty a) tm
-    t <- check ctx t a s
-    inScope "check" $ trace $ map (\_ => " subterm is well typed") tm
-    pure (Cnstr $ Left t)
-  (Left _, ty) => typeMismatch tm.bounds (pretty "sum") (pretty ty)
-  (Right t, Cnstr (Sum s s' a b)) => do
-    inScope "check" $ trace $ map (\_ => "checking right injection") tm
-    inScope "check" $ trace $ map (\_ => pretty {ann} "checking subterm for type" <++> pretty b) tm
-    t <- check ctx t b s'
-    inScope "check" $ trace $ map (\_ => " subterm is well typed") tm
-    pure (Cnstr $ Right t)
-  (Right _, ty) => typeMismatch tm.bounds (pretty "sum") (pretty ty)
-  (MkContainer t p f, Cnstr (Container s a s' s'')) => do
-    inScope "check" $ trace $ map (\_ => "checking container constructor") tm
-    let tagTy = tagTy s a s'
-    inScope "check" $ trace $ map (\_ => pretty {ann} "checking tag for type" <++> pretty tagTy) tm
-    t <- check ctx t (Cnstr tagTy) (s ~> suc s')
-    inScope "check" $ trace $ map (\_ => "tag is well typed") tm
-    positionTy <- positionTy s a s' t s''
-    inScope "check" $ trace $ map (\_ => pretty {ann} "checking position for type" <++> pretty positionTy) tm
-    p <- check ctx p (Cnstr positionTy) (s ~> s' ~> suc s'')
-    inScope "check" $ trace $ map (\_ => "position is well typed") tm
-    nextTy <- nextTy s a s' t s'' p
-    inScope "check" $ trace $ map (\_ => pretty {ann} "checking next for type" <++> pretty nextTy) tm
-    f <- check ctx f (Cnstr nextTy) (s ~> s' ~> s'' ~> s)
-    inScope "check" $ trace $ map (\_ => "next is well typed") tm
-    pure (Cnstr $ MkContainer t p f)
-  (MkContainer t p f, ty) => typeMismatch tm.bounds (pretty "container") (pretty ty)
-  (_, _) => do
-    inScope "check" $ trace $ map (\_ => "checking has fallen through") tm
-    (v, a, s') <- infer ctx tm
-    inScope "check" $ trace $ map (\_ => pretty {ann} "inferred type is" <++> pretty a) tm
-    let True = s == s'
-      | False => sortMismatch tm.bounds (pretty s) (pretty s')
-    True <- convert !(subst ty $ asSubst ctx) !(subst a $ asSubst ctx) (cast s) (suc s)
-      | False => typeMismatch tm.bounds (pretty ty) (pretty a)
-    inScope "check" $ trace $ map (\_ => pretty {ann} "converted" <++> pretty a <+> softline <+> pretty "to" <++> pretty ty) tm
-    pure v
+    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"
+    pure $ MkPair l l' t u
+  (_, Pair t u) => typeMismatch (pretty "pair type") (pretty ty)
+  (_, Absurd t) => do
+    info "encountered absurd"
+    trace "checking proof of contradiction"
+    Irrel <- check ctx Prop (Cnstr Bottom) (assert_smaller tm t)
+    pure $ doAbsurd _
+  (a, t) => do
+    info "falling through to inference"
+    (l ** (b, t)) <- infer ctx tm
+    trace $ pretty {ann} "inferred type is" <++> pretty b
+    let Yes Refl = decEq s l
+      | 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'
+    | Nothing => inScope "conversion failed" $ mismatch (pretty a) (pretty b)
+    pure t
 
-infer ctx tm = case tm.val of
+infer ctx tm = inBounds tm.bounds $ case tm.val of
   (Var var i) => do
-    inScope "infer" $ trace $ map (\_ => "encountered variable \{var}@\{show i}") tm
-    let (t, a, s) = index ctx i
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "variable has type" <++> pretty a) tm
-    pure (t, a, s)
-  (Sort s) => pure (cast s, cast (suc s), suc (suc s))
+    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))
   (Pi var a b) => do
-    inScope "infer" $ trace $ map (\_ => "encountered Pi type") tm
-    (a, s) <- inferType ctx a
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "argument has type" <++> pretty a) tm
-    (b, s') <- inferType (ctx ::< (var.val, a, s)) b
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "result has type" <++> pretty b <+> comma <+> softline <+> pretty "so Pi type has type" <++> pretty (s ~> s')) tm
-    pure (Cnstr (Pi s s' var.val a b), cast (s ~> s'), suc (s ~> s'))
-  (Lambda _ _) => inScope "cannot infer type" $ fatal tm
+    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)))
+  (Lambda var t) => fatal "cannot infer type of lambda"
   (App t u) => do
-    inScope "infer" $ trace $ map (\_ => "encountered application") tm
-    (t, ty@(Cnstr (Pi s s' _ a b)), _) <- infer ctx t
-      | (_, ty, _) => inScope "wrong type to apply" $ fatal (map (\_ => ty) tm)
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "function has type" <++> pretty ty) tm
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking argument has type" <++> pretty a) tm
-    u <- check ctx u a s
-    inScope "infer" $ trace $ map (\_ => "argument is well typed") tm
-    res <- doApp t u
+    info "encountered application"
+    (s ** (ty@(Cnstr (Pi l l' _ a b)), t)) <- infer ctx (assert_smaller tm t)
+      | (_ ** (ty, _)) => inBounds t.bounds $ typeMismatch (pretty "function") (pretty ty)
+    trace $ pretty {ann} "function has type" <++> pretty ty
+    trace $ pretty {ann} "checking argument has type" <++> pretty a
+    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"
     ty <- subst1 u b
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty ty) tm
-    pure (res, ty, s')
+    tm <- doApp t u
+    pure (l' ** (ty, rewrite sym $ impredicative l l' in tm))
   (Sigma var a b) => do
-    inScope "infer" $ trace $ map (\_ => "encountered Sigma type") tm
-    (a, s) <- inferType ctx a
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "first has type" <++> pretty a) tm
-    (b, s') <- inferType (ctx ::< (var.val, a, s)) b
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "second has type" <++> pretty b <+> comma <+> softline <+> pretty "so Sigma type has type" <++> pretty (lub s s')) tm
-    pure (Cnstr (Sigma s s' var.val a b), cast (lub s s'), suc (lub s s'))
-  (Pair _ _) => inScope "cannot infer type" $ fatal tm
+    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)))
+  (Pair t u) => fatal "cannot infer type of pair"
   (Fst t) => do
-    inScope "infer" $ trace $ map (\_ => "encountered first projection") tm
-    (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t
-      | (_, ty, _) => inScope "wrong type to fst" $ fatal (map (\_ => ty) tm)
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) tm
-    res <- doFst t
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty a) tm
-    pure (res, a, s)
+    info "encountered first"
+    (s ** (ty@(Cnstr (Sigma l l' _ a b)), t)) <- infer ctx (assert_smaller tm t)
+      | (_ ** (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 ty = a
+    tm <- doFst (isSet l) (isSet l') (rewrite sym $ maxIsSet l l' in t)
+    pure (l ** (ty, tm))
   (Snd t) => do
-    inScope "infer" $ trace $ map (\_ => "encountered first projection") tm
-    (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t
-      | (_, ty, _) => inScope "wrong type to snd" $ fatal (map (\_ => ty) tm)
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) tm
-    t1 <- doFst t
-    res <- doSnd t
-    b <- subst1 t1 b
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty b) tm
-    pure (res, b, s')
-  (Sum a b) => do
-    inScope "infer" $ trace $ map (\_ => "encountered sum type") tm
-    (a, s) <- inferType ctx a
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "left has type" <++> pretty a) tm
-    (b, s') <- inferType ctx b
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "right has type" <++> pretty b) tm
-    pure (Cnstr (Sum s s' a b), cast (ensureSet (lub s s')), suc (ensureSet (lub s s')))
-  (Left _) => inScope "cannot infer type" $ fatal tm
-  (Right _) => inScope "cannot infer type" $ fatal tm
-  (Case t l out f g) => do
-    inScope "infer" $ trace $ map (\_ => "encountered case") tm
-    (t, ty@(Cnstr (Sum s s' a b)), s'') <- infer ctx t
-      | (_, ty, _) => inScope "wrong type to case" $ fatal (map (\_ => ty) tm)
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "sum has type" <++> pretty ty) tm
-    l <- inferSort ctx l
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "output has sort" <++> pretty l) tm
-    let ty' = Cnstr (Pi s'' (suc l) "x" ty (cast l))
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking output has type" <++> pretty ty') tm
-    out <- check ctx out ty' (s'' ~> suc l)
-    inScope "infer" $ trace $ map (\_ => "output is well typed") tm
-    outL <- doApp (weaken 1 out) (Cnstr (Left (Ntrl (Var "x" 0))))
-    let fTy = Cnstr (Pi s l "x" a outL)
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking left branch has type" <++> pretty fTy) tm
-    f <- check ctx f fTy (s ~> l)
-    inScope "infer" $ trace $ map (\_ => "left branch is well typed") tm
-    outR <- doApp (weaken 1 out) (Cnstr (Right (Ntrl (Var "x" 0))))
-    let gTy = Cnstr (Pi s' l "x" b outR)
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking right branch has type" <++> pretty gTy) tm
-    g <- check ctx g gTy (s' ~> l)
-    inScope "infer" $ trace $ map (\_ => "right branch is well typed") tm
-    res <- doCase t f g
-    out <- doApp out t
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty out) tm
-    pure (res, out, l)
-  (Container a s' s'') => do
-    inScope "infer" $ trace $ map (\_ => "encountered container") tm
-    (a, s) <- inferType ctx a
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "index has type" <++> pretty a) tm
-    s' <- inferSort ctx s'
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "tag has sort" <++> pretty s') tm
-    s'' <- inferSort ctx s''
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "position has sort" <++> pretty s'') tm
-    pure (Cnstr (Container s a s' s''), cast (lub s (suc $ lub s' s'')), suc (lub s (suc $ lub s' s'')))
-  (MkContainer _ _ _) => inScope "cannot infer type" $ fatal tm
-  (Tag t) => do
-    inScope "infer" $ trace $ map (\_ => "encountered tag") tm
-    (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t
-      | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty)
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "deconstructing a container" <++> pretty ty) tm
-    tag <- doTag t
-    let out = tagTy s a s'
-    pure (tag, Cnstr out, s ~> suc s')
-  (Position t) => do
-    inScope "infer" $ trace $ map (\_ => "encountered position") tm
-    (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t
-      | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty)
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "deconstructing a container" <++> pretty ty) tm
-    tag <- doTag t
-    pos <- doPosition t
-    out <- positionTy s a s' tag s''
-    pure (pos, Cnstr out, s ~> s' ~> suc s'')
-  (Next t) => do
-    inScope "infer" $ trace $ map (\_ => "encountered next") tm
-    (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t
-      | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty)
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "deconstructing a container" <++> pretty ty) tm
-    tag <- doTag t
-    pos <- doPosition t
-    next <- doNext t
-    out <- nextTy s a s' tag s'' pos
-    pure (next, Cnstr out, s ~> s' ~> s'' ~> s)
-  (Sem l b t) => do
-    inScope "infer" $ trace $ map (\_ => "encountered sem") tm
-    (t, ty@(Cnstr (Container s a s' s'')), _) <- infer ctx t
-      | (_, ty, _) => typeMismatch t.bounds (pretty "container") (pretty ty)
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "interpretting a container" <++> pretty ty) tm
-    l <- inferSort ctx l
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "output has sort" <++> pretty l) tm
-    let outTy = Cnstr (Pi s (suc l) "i" a (cast l))
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking output has type" <++> pretty outTy) tm
-    b <- check ctx b outTy (s ~> suc l)
-    inScope "infer" $ trace $ map (\_ => "output is well typed") tm
-    tag <- doTag t
-    pos <- doPosition t
-    next <- doNext t
-    let i = Ntrl (Var "i" 0)
-    tag <- doApp (weaken 1 tag) i
-    pos <- doApp (weaken 1 pos) i
-    next <- doApp (weaken 1 next) i
-    let t = Ntrl (Var "t" 0)
-    pos <- doApp (weaken 1 pos) t
-    next <- doApp (weaken 1 next) t
-    let p = Ntrl (Var "p" 0)
-    next <- doApp (weaken 1 next) p
-    out <- doApp (weaken 3 b) next
-    let out = Cnstr $ Lambda "i" $
-              Cnstr $ Sigma s' (s'' ~> l) "t" tag $
-              Cnstr $ Pi s'' l "p" pos out
-    let ty = Cnstr $ Pi s (suc (lub s' (s'' ~> l))) "i" a (cast (lub s' (s'' ~> l)))
-    pure (out, ty, suc (s ~> suc (lub s' (s'' ~> l))))
-  Top => pure $ (Cnstr Top, cast Prop, Set 0)
-  Point => pure $ (Irrel, Cnstr Top, Prop)
-  Bottom  => pure $ (Cnstr Bottom, cast Prop, Set 0)
-  (Absurd a t) => do
-    inScope "infer" $ trace $ map (\_ => "encountered absurd") tm
-    (a, s) <- inferType ctx a
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "will fudge to type" <++> pretty a) tm
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking for proof of false") tm
-    _ <- check ctx t (Cnstr Bottom) Prop
-    inScope "infer" $ trace $ map (\_ => "proof of false is well typed") tm
-    pure (Ntrl Absurd, a, s)
+    info "encountered second"
+    (s ** (ty@(Cnstr (Sigma l l' _ a b)), t)) <- infer ctx (assert_smaller tm t)
+      | (_ ** (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
+    ty <- subst1 fst b
+    tm <- doSnd (isSet l) (isSet l') t
+    pure (l' ** (ty, tm))
+  Bool => do
+    info "encountered bool"
+    pure (Set 1 ** (cast (Set 0), Cnstr Bool))
+  True => do
+    info "encountered true"
+    pure (Set 0 ** (Cnstr Bool, Cnstr True))
+  False => do
+    info "encountered false"
+    pure (Set 0 ** (Cnstr Bool, Cnstr False))
+  (If var a t u v) => do
+    info "encountered if"
+    trace "checking discriminant is bool"
+    t <- check ctx (Set 0) (Cnstr Bool) (assert_smaller tm t)
+    trace "discriminant is well typed"
+    (s, a) <- inferType (ctx ::< MkFreeVar (Set 0) (Cnstr Bool) var.val) (assert_smaller tm a)
+    ty <- subst1 (Cnstr True) a
+    trace $ pretty {ann} "checking true branch has type" <++> pretty ty
+    u <- check ctx s ty (assert_smaller tm u)
+    ty <- subst1 (Cnstr False) a
+    trace $ pretty {ann} "checking false branch has type" <++> pretty ty
+    v <- check ctx s ty (assert_smaller tm v)
+    ty <- subst1 t a
+    tm <- doIf t u v
+    pure (s ** (ty, tm))
+  Top => do
+    info "encountered top"
+    pure (Set 0 ** (cast 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))
+  (Absurd t) => fatal "cannot infer type of absurd"
   (Equal t u) => do
-    inScope "infer" $ trace $ map (\_ => "encountered equal") tm
-    (t, a, s) <- infer ctx t
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "lhs has type" <++> pretty a) tm
-    inScope "infer" $ trace $ map (\_ => "checking rhs has same type") tm
-    u <- check ctx u a s
-    inScope "infer" $ trace $ map (\_ => "rhs is well typed") tm
-    res <- doEqual a t u
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "equality computes to" <++> pretty res) tm
-    pure (res, cast Prop, Set 0)
+    info "encountered equal"
+    (s ** (a, t)) <- infer ctx (assert_smaller tm t)
+    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))
   (Refl t) => do
-    inScope "infer" $ trace $ map (\_ => "encountered refl") tm
-    (t, a, s) <- infer ctx t
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "term has type" <++> pretty a) tm
-    ty <- doEqual a t t
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "equality computes to" <++> pretty ty) tm
-    pure (Irrel, ty, Prop)
-  (Transp t b u t' e) => do
-    inScope "infer" $ trace $ map (\_ => "encountered transp") tm
-    (t, a, s) <- infer ctx t
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "start index has type" <++> pretty a) tm
-    inScope "infer" $ trace $ map (\_ => "checking end index has same type") tm
-    t' <- check ctx t' a s
-    inScope "infer" $ trace $ map (\_ => "end index is well typed") tm
-    let ty = Cnstr (Pi s (Set 0) "_" a (cast Prop))
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "checkout output is in" <++> pretty ty) tm
-    b <- check ctx b ty s
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "output is well typed") tm
-    inScope "infer" $ trace $ map (\_ => "checking equality type") tm
-    eq <- doEqual a t t'
-    _ <- check ctx e eq Prop
-    inScope "infer" $ trace $ map (\_ => "equality is well typed") tm
-    inScope "infer" $ trace $ map (\_ => "checking transformed value") tm
-    inTy <- doApp b t
-    _ <- check ctx u inTy Prop
-    inScope "infer" $ trace $ map (\_ => "transformed value is well typed") tm
-    outTy <- doApp b t'
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "producing value of type" <++> pretty outTy) tm
-    pure (Irrel, outTy, Prop)
-  (Cast b e t) => do
-    inScope "infer" $ trace $ map (\_ => "encountered cast") tm
-    (t, a, s) <- infer ctx t
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "input has type" <++> pretty a) tm
-    inScope "infer" $ trace $ map (\_ => "checking output has same sort") tm
-    b <- check ctx b (cast s) (suc s)
-    inScope "infer" $ trace $ map (\_ => "output is well sorted") tm
-    inScope "infer" $ trace $ map (\_ => "checking equality type") tm
-    eq <- doEqual (cast s) a b
-    _ <- check ctx e eq Prop
-    inScope "infer" $ trace $ map (\_ => "equality is well typed") tm
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "producing value of type" <++> pretty b) tm
-    res <- doCastL a b t
-    pure (res, b, s)
+    info "encountered refl"
+    (s ** (a, t)) <- infer ctx (assert_smaller tm t)
+    trace "argument is well typed"
+    eq <- doEqual (isSet s) a t t
+    pure (Prop ** (eq, Irrel))
+  (Transp b t u t' e) => do
+    info "encountered transp"
+    (s ** (a, t)) <- infer ctx (assert_smaller tm t)
+    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)
+    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'
+    trace $ pretty {ann} "checking equality has type" <++> pretty eq
+    e <- check ctx Prop eq (assert_smaller tm e)
+    trace "equality is well typed"
+    newB <- doApp b t'
+    pure (Prop ** (newB, Irrel))
+  (Cast a b e t) => do
+    info "encountered cast"
+    (s, a) <- inferType ctx (assert_smaller tm a)
+    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
+    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
+    pure (s ** (b, tm))
   (CastId t) => do
-    inScope "infer" $ trace $ map (\_ => "encountered cast identity proof") tm
-    (t, a, s) <- infer ctx t
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "term has type" <++> pretty a) tm
-    cast <- doCastL a a t
-    eq <- doEqual a cast t
-    inScope "infer" $ trace $ map (\_ => pretty {ann} "producing equality type" <++> pretty eq) tm
-    pure (Irrel, eq, Prop)
-
-inferType ctx a = do
-  (a, Cnstr (Sort s), _) <- infer ctx a
-    | (_, ty, _) => tag a.bounds (pretty "sort") (pretty ty)
-  pure (a, s)
-
-inferSort ctx a = do
-  (Cnstr (Sort s), _, _) <- infer ctx a
-    | (t, _, _) => inScope "infer" $ typeMismatch a.bounds (pretty "sort") (pretty t)
-  pure s
+    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
+    pure (Prop ** (ret, Irrel))
 
 -- Checking Definitions and Blocks ---------------------------------------------
 
-partial
-checkDef : Context n -> Term.Definition n -> Logging ann (NormalForm.Definition n)
-checkDef ctx def = do
-  (ty, sort) <-
-    inferType {tag = \bounds, lhs, rhs => inScope "invalid declaration" $ mismatch bounds lhs rhs}
+checkDef : Context ctx -> Term.Definition (length ctx) -> Logging ann (NormalForm.Definition ctx)
+checkDef ctx def = inBounds def.name.bounds $ inScope "check" $ do
+  debug $ "inferring type of \{def.name.val}"
+  (sort, ty) <-
+    inferType {tag = \lhs, rhs => inScope "invalid declaration" $ mismatch lhs rhs}
       (fromContext ctx) def.ty
-  inScope "check" $ debug $ map (\name => pretty {ann} "\{name} has type" <++> pretty ty) def.name
-  tm <- check (fromContext ctx) def.tm ty sort
-  inScope "check" $ debug $ map (\name => pretty {ann} "\{name} is well typed with value" <++> pretty tm) def.name
+  debug $ pretty {ann} "\{def.name.val} has type" <++> pretty ty
+  tm <- check (fromContext ctx) sort ty def.tm
+  debug $ pretty {ann} "\{def.name.val} is well typed with value" <++> pretty tm
   pure $ MkDefinition {name = def.name, ty, tm, sort}
 
-partial
 export
-checkBlock : Block n -> Logging ann (Context n)
-checkBlock [] = pure []
+checkBlock : Block n -> Logging ann (ctx ** (Context ctx, length ctx = n))
+checkBlock [] = pure ([] ** ([], Refl))
 checkBlock (blk :< def) = do
-  ctx <- checkBlock blk
+  (_ ** (ctx, Refl)) <- checkBlock blk
   def <- checkDef ctx def
-  pure (ctx :< def)
+  pure (_ ** (ctx :< def, Refl))
diff --git a/src/Obs/Typing/Context.idr b/src/Obs/Typing/Context.idr
new file mode 100644
index 0000000..636c9f2
--- /dev/null
+++ b/src/Obs/Typing/Context.idr
@@ -0,0 +1,108 @@
+module Obs.Typing.Context
+
+import Data.Fin
+import public Data.List
+import Data.List.Elem
+
+import Obs.Logging
+import Obs.NormalForm
+import Obs.NormalForm.Normalise
+import Obs.Substitution
+import Obs.Sort
+
+import Text.Bounded
+
+-- Definitions -----------------------------------------------------------------
+
+infix 5 ::<
+
+public export
+record FreeVar (ctx : List Bool) where
+  constructor MkFreeVar
+  sort : Sort
+  ty : NormalForm True ctx
+  name : String
+
+public export
+record TyDef (b : Bool) (ctx : List Bool) where
+  constructor MkDefinition
+  name : String
+  sort : Sort
+  ty : NormalForm True ctx
+  tm : NormalForm (isSet sort) ctx
+  correct : isSet sort = b
+
+public export
+data TyContext : Unsorted.Family Bool where
+  Nil   : TyContext []
+  (:<)  : TyContext ctx -> (def : Definition ctx) -> TyContext (isSet def.sort :: ctx)
+  (::<) : TyContext ctx -> (var : FreeVar ctx) -> TyContext (isSet var.sort :: ctx)
+
+-- Properties ------------------------------------------------------------------
+
+freeVars : TyContext ctx -> List Bool
+freeVars [] = []
+freeVars (ctx :< def) = freeVars ctx
+freeVars (ctx ::< var) = isSet var.sort :: freeVars ctx
+
+Sorted.Rename Bool 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 = MkDefinition
+  { name = def.name.val
+  , sort = def.sort
+  , ty = def.ty
+  , tm = def.tm
+  , correct = Refl
+  }
+
+fromVar : (var : FreeVar ctx) -> TyDef (isSet var.sort) (isSet var.sort :: ctx)
+fromVar var = MkDefinition
+  { name = var.name
+  , sort = var.sort
+  , ty = weaken [isSet var.sort] var.ty
+  , tm = point (var.name, (var.sort ** Refl)) Here
+  , correct = Refl
+  }
+
+export
+fromContext : Context ctx -> TyContext ctx
+fromContext []           = []
+fromContext (ctx :< def) = fromContext ctx :< def
+
+-- Destruction -----------------------------------------------------------------
+
+export
+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)
+getContext (ctx ::< var) =
+  let (ctx' ** prf) = getContext ctx in
+  (isSet var.sort :: ctx' ** cong (isSet var.sort ::) prf)
+
+export
+index : TyContext ctx -> Map ctx TyDef ctx
+index [] = absurd
+index (ctx :< def) = weaken [_] . add TyDef (fromDef def) (index ctx)
+index (ctx ::< var) = add TyDef (fromVar var) (weaken [_] . index ctx)
+
+finToElem : {xs : List a} -> (i : Fin (length xs)) -> Elem (index' xs i) xs
+finToElem {xs = (x :: xs)} FZ = Here
+finToElem {xs = (x :: xs)} (FS i) = There (finToElem i)
+
+export
+index' : TyContext ctx -> (i : Fin (length ctx)) -> TyDef (index' ctx i) ctx
+index' ctx i = let (ctx' ** Refl) = getContext ctx in index ctx (finToElem i)
+
+export
+reduce : (tyCtx : TyContext ctx) -> Map ctx (LogNormalForm ann) (freeVars tyCtx)
+reduce [] = absurd
+reduce (ctx :< def) = add (LogNormalForm ann) (subst def.tm (reduce ctx)) (reduce ctx)
+reduce (ctx ::< var) = add (LogNormalForm ann)
+  (pure $ point (var.name, (var.sort ** Refl)) Here)
+  (\i => pure $ weaken [_] $ !(reduce ctx i))
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr
index 37bdf67..d5dc86a 100644
--- a/src/Obs/Typing/Conversion.idr
+++ b/src/Obs/Typing/Conversion.idr
@@ -1,6 +1,12 @@
 module Obs.Typing.Conversion
 
-import Data.Fin
+import Control.Monad.Maybe
+import Control.Monad.Trans
+
+import Data.Bool
+import Data.So
+
+import Decidable.Equality
 
 import Obs.Logging
 import Obs.NormalForm
@@ -8,71 +14,194 @@ import Obs.NormalForm.Normalise
 import Obs.Sort
 import Obs.Substitution
 
--- Conversion ------------------------------------------------------------------
+%default total
 
--- invariant: all definitions fully expanded
--- invariant: m |- t, u <- a : s
-partial export
-convert : (t, u, a : NormalForm n) -> Sort -> Logging ann Bool
-partial
-convertSet : (t, u : NormalForm n) -> Logging ann Bool
-partial
-convertSum : (t, u : NormalForm n) -> (s, s' : Sort) -> (a, b : NormalForm n) -> Logging ann Bool
+-- Conversion ------------------------------------------------------------------
 
--- In sort Prop
-convert Irrel Irrel a Prop = pure True
--- In unknown type in set
-convert t u (Ntrl _) (Set k) = pure $ t == u
--- In type Set
-convert t u (Cnstr (Sort _)) (Set _) = convertSet t u
--- In type Pi
-convert t u (Cnstr (Pi s s' var a b)) (Set k) = do
-  t <- doApp (weaken 1 t) (Ntrl $ Var var FZ)
-  u <- doApp (weaken 1 u) (Ntrl $ Var var FZ)
-  convert t u b s'
--- In type Sigma
-convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do
-  t1 <- doFst t
-  u1 <- doFst t
-  True <- convert t1 u1 a s
-    | False => pure False
-  b <- subst1 t1 b
-  t2 <- doSnd t
-  u2 <- doSnd t
-  convert t2 u2 b s'
--- In type Sum (manually expanding definition of doCase)
-convert t u (Cnstr (Sum s s' a b)) (Set _) = convertSum t u s s' a b
--- In type Container
-convert t u (Cnstr (Container s a s' s'')) (Set l) = do
-  t <- expandContainer t
-  u <- expandContainer u
-  convert (Cnstr t) (Cnstr u) (Cnstr (expandContainerTy s a s' s'')) (Set l)
--- Default
-convert t u a s =
-  inScope "invalid conversion" $ fatal $
-  fillSep {ann} [prettyPrec App t, prettyPrec App u, prettyPrec App a, prettyPrec App s]
+export
+convert : (s : Sort)
+  -> (a : NormalForm True ctx)
+  -> (t, u : NormalForm (isSet s) ctx)
+  -> MaybeT (Logging ann) (NormalForm (isSet s) ctx)
 
-convertSet (Cnstr (Sort s')) (Cnstr (Sort s'')) = pure $ s' == s''
-convertSet (Cnstr (Pi s s' _ a b)) (Cnstr (Pi l l' _ a' b')) =
-  pure $
-  s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
-convertSet (Cnstr (Sigma s s' _ a b)) (Cnstr (Sigma l l' _ a' b')) =
-  pure $
-  s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
-convertSet (Cnstr (Sum s s' a b)) (Cnstr (Sum l l' a' b')) =
-  pure $
-  s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
-convertSet (Cnstr (Container s a s' s'')) (Cnstr (Container l a' l' l'')) =
-  pure $
-  s == l && s' == l' && s'' == l'' && !(convertSet a a')
-convertSet (Cnstr Top) (Cnstr Top) = pure True
-convertSet (Cnstr Bottom) (Cnstr Bottom) = pure True
-convertSet (Ntrl t) u = pure (Ntrl t == u)
-convertSet t (Ntrl u) = pure (t == Ntrl u)
-convertSet t u = pure $ False
+untypedConvert : (t, u : NormalForm True ctx) -> MaybeT (Logging ann) (NormalForm True ctx)
+-- Diagonals
+untypedConvert (Cnstr (Sort s)) (Cnstr (Sort s')) =
+  if s == s' then pure (Cnstr (Sort 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')
+  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'
+    | No _ => nothing
+  lift $ trace "converting under lambda"
+  t <- untypedConvert t u
+  pure (Cnstr $ Lambda s var t)
+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')
+  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')
+    | No _ => nothing
+  lift $ trace "converting pair pointwise"
+  t <- untypedConvert t t'
+  u <- untypedConvert u u'
+  pure (Cnstr $ Pair l l' Oh 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)
+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)
+untypedConvert (Cnstr Bool) (Cnstr Bool) = pure (Cnstr Bool)
+untypedConvert (Cnstr True) (Cnstr True) = pure (Cnstr True)
+untypedConvert (Cnstr False) (Cnstr False) = pure (Cnstr False)
+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'
+    | 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
+  u <- untypedConvert u u'
+  lift $ doApp t u
+untypedConvert lhs@(Ntrl (Fst b t)) rhs@(Ntrl (Fst b' 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 $ 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)
+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'))
+  f <- untypedConvert f f'
+  g <- untypedConvert g g'
+  lift $ doIf t f g
+untypedConvert (Ntrl Absurd) (Ntrl Absurd) = pure (Ntrl Absurd)
+untypedConvert lhs@(Ntrl (Equal a t u)) rhs@(Ntrl (Equal a' t' u')) = do
+  lift $ trace "checking equal (stuck on type)"
+  a <- untypedConvert (assert_smaller lhs (Ntrl a)) (assert_smaller rhs (Ntrl a'))
+  t <- untypedConvert t t'
+  u <- untypedConvert u u'
+  lift $ doEqual _ a t u
+untypedConvert lhs@(Ntrl (EqualL t u)) rhs@(Ntrl (EqualL t' u')) = do
+  lift $ trace "checking equal (stuck on left)"
+  t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
+  u <- untypedConvert u u'
+  lift $ doEqualSet t u
+untypedConvert lhs@(Ntrl (EqualR t u)) rhs@(Ntrl (EqualR t' u')) = do
+  lift $ trace "checking equal (stuck on right)"
+  t <- untypedConvert (assert_smaller lhs (Cnstr t)) (assert_smaller rhs (Cnstr t'))
+  u <- untypedConvert (assert_smaller lhs (Ntrl u)) (assert_smaller rhs (Ntrl u'))
+  lift $ doEqualSet t u
+untypedConvert lhs@(Ntrl (EqualStuck t u)) rhs@(Ntrl (EqualStuck t' u')) = do
+  lift $ trace "checking equal (head mismatch)"
+  t <- untypedConvert (assert_smaller lhs (Cnstr t)) (assert_smaller rhs (Cnstr t'))
+  u <- untypedConvert (assert_smaller lhs (Cnstr u)) (assert_smaller rhs (Cnstr u'))
+  lift $ doEqualSet t u
+untypedConvert lhs@(Ntrl (CastL a b t)) rhs@(Ntrl (CastL a' b' t')) = do
+  lift $ trace "checking cast (stuck on left)"
+  a <- untypedConvert (assert_smaller lhs (Ntrl a)) (assert_smaller rhs (Ntrl a'))
+  b <- untypedConvert b b'
+  t <- untypedConvert t t'
+  lift $ doCast _ a b t
+untypedConvert lhs@(Ntrl (CastR a b t)) rhs@(Ntrl (CastR a' b' t')) = do
+  lift $ trace "checking cast (stuck on right)"
+  a <- untypedConvert (assert_smaller lhs (Cnstr a)) (assert_smaller rhs (Cnstr a'))
+  b <- untypedConvert (assert_smaller lhs (Ntrl b)) (assert_smaller rhs (Ntrl b'))
+  t <- untypedConvert t t'
+  lift $ doCast _ a b t
+untypedConvert lhs@(Ntrl (CastStuck a b t)) rhs@(Ntrl (CastStuck a' b' t')) = do
+  lift $ trace "checking cast (stuck on left)"
+  a <- untypedConvert (assert_smaller lhs (Cnstr a)) (assert_smaller rhs (Cnstr a'))
+  b <- untypedConvert (assert_smaller lhs (Cnstr b)) (assert_smaller rhs (Cnstr b'))
+  t <- untypedConvert t t'
+  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)
+  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)
+  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'
+  in do
+  t' <- lift $ doFst (isSet s) (isSet s') t''
+  u' <- lift $ doSnd (isSet s) (isSet 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
+  in do
+  t <- lift $ doFst (isSet s) (isSet s') t''
+  u <- lift $ doSnd (isSet s) (isSet s') t''
+  assert_total (untypedConvert (Cnstr (Pair s s' prf t u)) t')
+-- Bools
+-- no cases because diagonals complete
+-- Fallback
+untypedConvert _ _ = nothing
 
-convertSum (Cnstr (Left t)) (Cnstr (Left u)) s s' a b = convert t u a s
-convertSum (Cnstr (Right t)) (Cnstr (Right u)) s s' a b = convert t u b s'
-convertSum (Ntrl t) u s s' a b = pure (Ntrl t == u)
-convertSum t (Ntrl u) s s' a b = pure (t == Ntrl u)
-convertSum t u s s' a b = pure False
+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
+  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 <- 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 <- convert s a t1 u1
+  t2 <- lift $ doSnd True (isSet s') t
+  u2 <- lift $ doSnd True (isSet s') u
+  b <- lift $ subst1 t1 b
+  t2 <- convert s' (assert_smaller ty b) t2 u2
+  pure (Cnstr $ Pair s s' Oh 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
+  b <- lift $ subst1 Irrel b
+  t2 <- convert s' (assert_smaller ty b) t2 u2
+  pure (Cnstr $ Pair Prop s' Oh Irrel t2)
+convert (Set 0) (Cnstr Bool) (Cnstr True) (Cnstr True) = do
+  lift $ trace "converting bool (true)"
+  pure (Cnstr True)
+convert (Set 0) (Cnstr Bool) (Cnstr False) (Cnstr False) = do
+  lift $ trace "converting bool (false)"
+  pure (Cnstr False)
+convert (Set k) (Cnstr Bool) t@(Ntrl _) u@(Ntrl _) = do
+  lift $ trace "converting bool (neutral)"
+  untypedConvert t u
+convert (Set k) (Cnstr a) t u = lift $ inScope "bad type constructor" $ fatal a