Add more program structure to normal forms.

12 files changed, 1114 insertions, 782 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 039f60e..4ef3f43 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -18,29 +18,45 @@ Context n = List (String, Fin n)
 bind : Context n -> String -> Context (S n)
 bind ctx str = (str, 0) :: map (mapSnd FS) ctx
 
-abstractSyntax : Context n -> Syntax -> Logging ann (Term n)
 abstractSyntaxBounds : Context n -> WithBounds Syntax -> Logging ann (WithBounds (Term n))
 
+abstractDecl : Context n -> DeclForm -> Logging ann (DeclForm n)
+abstractDecl ctx (MkDecl var type) = do
+  type <- abstractSyntaxBounds ctx type
+  pure (MkDecl var type)
+
+abstractLambda : Context n -> LambdaForm -> Logging ann (LambdaForm n)
+abstractLambda ctx (MkLambda var body) = do
+  body <- abstractSyntaxBounds (bind ctx var.val) body
+  pure (MkLambda var body)
+
+abstractSyntax : Context n -> Syntax -> Logging ann (Term n)
 abstractSyntax ctx (Var {var}) = do
   let Just i = lookup var ctx
     | Nothing => inScope "unbound variable" $ fatal var
   pure (Var {var, i})
 abstractSyntax ctx (Universe {s}) = pure (Universe {s})
-abstractSyntax ctx (Pi {var, domain, codomain}) = do
-  domain <- abstractSyntaxBounds ctx domain
-  codomain <- abstractSyntaxBounds (bind ctx var.val) codomain
-  pure (Pi {var, domain, codomain})
-abstractSyntax ctx (Lambda {var, body}) = do
-  body <- abstractSyntaxBounds (bind ctx var.val) body
-  pure (Lambda {var, body})
+abstractSyntax ctx (Pi {domain, codomain}) = do
+  domain <- abstractDecl ctx domain
+
+  let ctx = bind ctx domain.var.val
+  codomain <- abstractSyntaxBounds ctx codomain
+
+  pure (Pi {domain, codomain})
+abstractSyntax ctx (Lambda {body}) = do
+  body <- abstractLambda ctx body
+  pure (Lambda {body})
 abstractSyntax ctx (App {fun, arg}) = do
   fun <- abstractSyntaxBounds ctx fun
   arg <- abstractSyntaxBounds ctx arg
   pure (App {fun, arg})
-abstractSyntax ctx (Sigma {var, index, element}) = do
-  index <- abstractSyntaxBounds ctx index
-  element <- abstractSyntaxBounds (bind ctx var.val) element
-  pure (Sigma {var, index, element})
+abstractSyntax ctx (Sigma {index, element}) = do
+  index <- abstractDecl ctx index
+
+  let ctx = bind ctx index.var.val
+  element <- abstractSyntaxBounds ctx element
+
+  pure (Sigma {index, element})
 abstractSyntax ctx (Pair {first, second}) = do
   first <- abstractSyntaxBounds ctx first
   second <- abstractSyntaxBounds ctx second
@@ -54,12 +70,12 @@ abstractSyntax ctx (Second {arg}) = do
 abstractSyntax ctx Bool = pure Bool
 abstractSyntax ctx True = pure True
 abstractSyntax ctx False = pure False
-abstractSyntax ctx (If {var, returnType, discriminant, true, false}) = do
-  returnType <- abstractSyntaxBounds (bind ctx var.val) returnType
+abstractSyntax ctx (If {returnType, discriminant, true, false}) = do
+  returnType <- abstractLambda ctx returnType
   discriminant <- abstractSyntaxBounds ctx discriminant
   true <- abstractSyntaxBounds ctx true
   false <- abstractSyntaxBounds ctx false
-  pure (If {var, returnType, discriminant, true, false})
+  pure (If {returnType, discriminant, true, false})
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom
diff --git a/src/Obs/Logging.idr b/src/Obs/Logging.idr
index 5666001..07060e6 100644
--- a/src/Obs/Logging.idr
+++ b/src/Obs/Logging.idr
@@ -48,10 +48,10 @@ pretty msg =
   let leader =
     hsep $
       [ fill 6 (pretty (show msg.lvl) <+> colon) ] ++
-      [ Doc.pretty $ concat {t = List} $
-        case msg.bounds of
-          Nothing => []
-          Just bounds =>
+      (case msg.bounds of
+        Nothing => []
+        Just bounds =>
+          [ Doc.pretty $ concat {t = List} $
             [ show (1 + bounds.startLine)
             , ":"
             , show bounds.startCol
@@ -61,7 +61,7 @@ pretty msg =
             , show bounds.endCol
             , ":"
             ]
-      ] ++
+          ]) ++
       map (\s => pretty s <+> colon) msg.tags
   in group $ width (group leader <+> line) (\width => group $ indent (2 - width) msg.msg)
 
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index d660111..0b9d2b6 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -2,6 +2,7 @@ module Obs.NormalForm
 
 import Data.List.Elem
 
+import Obs.Pretty
 import Obs.Substitution
 import Obs.Universe
 
@@ -19,27 +20,31 @@ TypeNormalForm : Unsorted.Family Relevance
 TypeNormalForm = NormalForm Relevant
 
 public export
+record DeclForm (ctx : List Relevance) where
+  constructor MkDecl
+  var : Maybe String
+  type : TypeNormalForm ctx
+
+public export
 data Constructor : Unsorted.Family Relevance where
   Universe : (s : Universe) -> Constructor ctx
-  Pi : (s, s' : Universe)
-    -> (var : String)
-    -> (a : TypeNormalForm ctx)
-    -> (b : TypeNormalForm (relevance s :: ctx))
-    -> Constructor ctx
-  Lambda : (s : Universe)
-    -> (var : String)
-    -> NormalForm Relevant (relevance s :: ctx)
-    -> Constructor ctx
-  Sigma : (s, s' : Universe)
-    -> (var : String)
-    -> (a : TypeNormalForm ctx)
-    -> (b : TypeNormalForm (relevance s :: ctx))
-    -> Constructor ctx
-  Pair : (s, s' : Universe)
-    -> (prf : IsRelevant (max s s'))
-    -> NormalForm (relevance s) ctx
-    -> NormalForm (relevance s') ctx
-    -> Constructor ctx
+  Pi : (domainSort, codomainSort : Universe) ->
+    (domain : DeclForm ctx) ->
+    (codomain : TypeNormalForm (relevance domainSort :: ctx)) ->
+    Constructor ctx
+  Lambda : (domainRel : Relevance) ->
+    (var : Maybe String) ->
+    (body : NormalForm Relevant (domainRel :: ctx)) ->
+    Constructor ctx
+  Sigma : (indexSort, elementSort : Universe) ->
+    (index : DeclForm ctx) ->
+    (element : TypeNormalForm (relevance indexSort :: ctx)) ->
+    Constructor ctx
+  Pair : (indexRel, elementRel : Relevance) ->
+    (prf : IsRelevant (pair indexRel elementRel)) ->
+    (first : NormalForm indexRel ctx) ->
+    (second : NormalForm elementRel ctx) ->
+    Constructor ctx
   Bool : Constructor ctx
   True : Constructor ctx
   False : Constructor ctx
@@ -48,26 +53,27 @@ data Constructor : Unsorted.Family Relevance where
 
 public export
 data Neutral : Unsorted.Family Relevance where
-  Var : (var : String)
-    -> (sort : Universe)
-    -> (prf : IsRelevant sort)
-    -> (i : Elem Relevant ctx)
-    -> Neutral ctx
-  App : (r : Relevance) -> Neutral ctx -> NormalForm r ctx -> Neutral ctx
-  Fst : (r : Relevance) -> Neutral ctx -> Neutral ctx
-  Snd : (r : Relevance) -> Neutral ctx -> Neutral ctx
-  If : Neutral ctx -> (f, g : NormalForm Relevant ctx) -> Neutral ctx
+  Var : (var : String) -> (i : Elem Relevant ctx) -> Neutral ctx
+  App : (argRel : Relevance) -> (fun : Neutral ctx) -> (arg : NormalForm argRel ctx) -> Neutral ctx
+  First : (secondRel : Relevance) -> (arg : Neutral ctx) -> Neutral ctx
+  Second : (firstRel : Relevance) -> (arg : Neutral ctx) -> Neutral ctx
+  If : (discriminant : Neutral ctx) -> (true, false : NormalForm Relevant ctx) -> Neutral ctx
   Absurd : Neutral ctx
-  Equal : Neutral ctx -> NormalForm Relevant ctx -> NormalForm Relevant ctx -> Neutral ctx
-  EqualL : (a : Neutral ctx) -> (b : TypeNormalForm ctx) -> Neutral ctx
-  EqualR : (a : Constructor ctx) -> (b : Neutral ctx) -> Neutral ctx
-  EqualStuck : (a, b : Constructor ctx) -> Neutral ctx
-  CastL : (a : Neutral ctx) ->
-    (b : TypeNormalForm ctx) ->
-    NormalForm Relevant ctx ->
+  Equal : (type : Neutral ctx) -> (left, right : NormalForm Relevant ctx) -> Neutral ctx
+  EqualL : (left : Neutral ctx) -> (right : TypeNormalForm ctx) -> Neutral ctx
+  EqualR : (left : Constructor ctx) -> (right : Neutral ctx) -> Neutral ctx
+  EqualStuck : (left, right : Constructor ctx) -> Neutral ctx
+  CastL : (oldType : Neutral ctx) ->
+    (newType : TypeNormalForm ctx) ->
+    (value : NormalForm Relevant ctx) ->
+    Neutral ctx
+  CastR : (oldType : Constructor ctx) ->
+    (newType : Neutral ctx) ->
+    (value : NormalForm Relevant ctx) ->
+    Neutral ctx
+  CastStuck : (oldType, newType : Constructor ctx) ->
+    (value : NormalForm Relevant ctx) ->
     Neutral ctx
-  CastR : (a : Constructor ctx) -> (b : Neutral ctx) -> NormalForm Relevant ctx -> Neutral ctx
-  CastStuck : (a, b : Constructor ctx) -> NormalForm Relevant ctx -> Neutral ctx
 
 public export
 data NormalForm : Sorted.Family Relevance where
@@ -108,34 +114,19 @@ Cast Universe (NormalForm Relevant ctx) where
 
 prettyPrec : Prec -> NormalForm b ctx -> Doc ann
 
+prettyPrecDecl : DeclForm ctx -> Doc ann
+prettyPrecDecl (MkDecl var type) = prettyDecl var (prettyPrec Open type)
+
 prettyPrecCnstr : Prec -> Constructor ctx -> Doc ann
-prettyPrecCnstr d (Universe s) = prettyPrec d s
-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 $
-  lhs <++> pretty "->" <+> line <+> align (prettyPrec Open b)
-prettyPrecCnstr d (Lambda _ var t) =
-  parenthesise (d > Open) $
-  group $
-  backslash <+> pretty var <++>
-  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 $
-  lhs <++> pretty "**" <+> line <+> align (prettyPrec Open b)
-prettyPrecCnstr d (Pair s s' prf t u) =
-  angles $
-  group $
-  neutral <++> prettyPrec Open t <+> comma <+> line <+> prettyPrec Open u <++> neutral
+prettyPrecCnstr d (Universe {s}) = prettyPrec d s
+prettyPrecCnstr d (Pi {domainSort, codomainSort, domain, codomain}) =
+  prettyDeclForm d [prettyPrecDecl domain] "->" (prettyPrec Open codomain)
+prettyPrecCnstr d (Lambda {domainRel, var, body}) =
+  prettyLambda d (maybe "_" id var) (prettyPrec Open body)
+prettyPrecCnstr d (Sigma {indexSort, elementSort, index, element}) =
+  prettyDeclForm d [prettyPrecDecl index] "**" (prettyPrec Open element)
+prettyPrecCnstr d (Pair {indexRel, elementRel, prf, first, second}) =
+  prettyPair (prettyPrec Open first) (prettyPrec Open second)
 prettyPrecCnstr d Bool = pretty "Bool"
 prettyPrecCnstr d True = pretty "True"
 prettyPrecCnstr d False = pretty "False"
@@ -143,52 +134,34 @@ prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
 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 $
-  vsep [prettyPrecNtrl Open t, prettyPrec App u]
-prettyPrecNtrl d (Fst _ t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "fst", prettyPrecNtrl App t]
-prettyPrecNtrl d (Snd _ t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "snd", prettyPrecNtrl App t]
-prettyPrecNtrl d (If t f g) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "if", prettyPrecNtrl App t, prettyPrec App f, prettyPrec App g]
+prettyPrecNtrl d (Var {var, i}) = pretty "\{var}@\{show $ elemToNat i}"
+prettyPrecNtrl d (App {argRel, fun, arg}) =
+  prettyApp d (prettyPrecNtrl Open fun) [prettyPrec App arg]
+prettyPrecNtrl d (First {secondRel, arg}) =
+  prettyApp d (pretty "fst") [prettyPrecNtrl App arg]
+prettyPrecNtrl d (Second {firstRel, arg}) =
+  prettyApp d (pretty "snd") [prettyPrecNtrl App arg]
+prettyPrecNtrl d (If {discriminant, true, false}) =
+  prettyApp d (pretty "if") $
+  [prettyPrecNtrl App discriminant, prettyPrec App true, prettyPrec App false]
 prettyPrecNtrl d Absurd = pretty "absurd"
-prettyPrecNtrl d (Equal a t u) =
-  parenthesise (d >= Equal) $
-  group $
-  prettyPrec Equal t <++> pretty "~" <+> line <+> prettyPrec Equal u
-prettyPrecNtrl d (EqualL a b) =
-  parenthesise (d >= Equal) $
-  group $
-  prettyPrecNtrl Equal a <++> pretty "~" <+> line <+> prettyPrec Equal b
-prettyPrecNtrl d (EqualR a b) =
-  parenthesise (d >= Equal) $
-  group $
-  prettyPrecCnstr Equal a <++> pretty "~" <+> line <+> prettyPrecNtrl Equal b
-prettyPrecNtrl d (EqualStuck a b) =
-  parenthesise (d >= Equal) $
-  group $
-  prettyPrecCnstr Equal a <++> pretty "~" <+> line <+> prettyPrecCnstr Equal b
-prettyPrecNtrl d (CastL a b t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "cast", prettyPrecNtrl App a, prettyPrec App b, prettyPrec App t]
-prettyPrecNtrl d (CastR a b t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "cast", prettyPrecCnstr App a, prettyPrecNtrl App b, prettyPrec App t]
-prettyPrecNtrl d (CastStuck a b t) =
-  parenthesise (d >= App) $
-  group $
-  vsep [pretty "cast", prettyPrecCnstr App a, prettyPrecCnstr App b, prettyPrec App t]
+prettyPrecNtrl d (Equal {type, left, right}) =
+  prettyEqual d (prettyPrec Equal left) (prettyPrec Equal right)
+prettyPrecNtrl d (EqualL {left, right}) =
+  prettyEqual d (prettyPrecNtrl Equal left) (prettyPrec Equal right)
+prettyPrecNtrl d (EqualR {left, right}) =
+  prettyEqual d (prettyPrecCnstr Equal left) (prettyPrecNtrl Equal right)
+prettyPrecNtrl d (EqualStuck {left, right}) =
+  prettyEqual d (prettyPrecCnstr Equal left) (prettyPrecCnstr Equal right)
+prettyPrecNtrl d (CastL {oldType, newType, value}) =
+  prettyApp d (pretty "cast") $
+  [prettyPrecNtrl App oldType, prettyPrec App newType, prettyPrec App value]
+prettyPrecNtrl d (CastR {oldType, newType, value}) =
+  prettyApp d (pretty "cast") $
+  [prettyPrecCnstr App oldType, prettyPrecNtrl App newType, prettyPrec App value]
+prettyPrecNtrl d (CastStuck {oldType, newType, value}) =
+  prettyApp d (pretty "cast") $
+  [prettyPrecCnstr App oldType, prettyPrecCnstr App newType, prettyPrec App value]
 
 prettyPrec d (Ntrl t) = prettyPrecNtrl d t
 prettyPrec d (Cnstr t) = prettyPrecCnstr d t
@@ -210,13 +183,35 @@ Pretty (NormalForm b ctx) where
 
 rename : NormalForm ~|> Hom Elem NormalForm
 
+renameDecl : DeclForm ~|> Hom Elem DeclForm
+renameDecl (MkDecl var type) f = MkDecl var (rename type f)
+
 renameCnstr : Constructor ~|> Hom Elem Constructor
-renameCnstr (Universe s) f = Universe s
-renameCnstr (Pi s s' var a b) f = Pi s s' var (rename a f) (rename b (lift [(_ ** ())] f))
-renameCnstr (Lambda s var t) f = Lambda s var (rename t (lift [(_ ** ())] f))
-renameCnstr (Sigma s s' var a b) f =
-  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 (Universe {s}) f = Universe {s}
+renameCnstr (Pi {domainSort, codomainSort, domain, codomain}) f =
+  Pi
+    { domainSort
+    , codomainSort
+    , domain = renameDecl domain f
+    , codomain = rename codomain (lift [(_ ** ())] f)
+    }
+renameCnstr (Lambda {domainRel, var, body}) f =
+  Lambda {domainRel, var, body = rename body (lift [(_ ** ())] f)}
+renameCnstr (Sigma {indexSort, elementSort, index, element}) f =
+  Sigma
+    { indexSort
+    , elementSort
+    , index = renameDecl index f
+    , element = rename element (lift [(_ ** ())] f)
+    }
+renameCnstr (Pair {indexRel, elementRel, prf, first, second}) f =
+  Pair
+    { indexRel
+    , elementRel
+    , prf
+    , first = rename first f
+    , second = rename second f
+    }
 renameCnstr Bool f = Bool
 renameCnstr True f = True
 renameCnstr False f = False
@@ -224,19 +219,30 @@ renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom
 
 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 (Var {var, i}) f = Var {var, i = f i}
+renameNtrl (App {argRel, fun, arg}) f = App {argRel, fun = renameNtrl fun f, arg = rename arg f}
+renameNtrl (First {secondRel, arg}) f = First {secondRel, arg = renameNtrl arg f}
+renameNtrl (Second {firstRel, arg}) f = Second {firstRel, arg = renameNtrl arg f}
+renameNtrl (If {discriminant, true, false}) f =
+  If {discriminant = renameNtrl discriminant f, true = rename true f, false = rename false f}
 renameNtrl Absurd f = Absurd
-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)
+renameNtrl (Equal {type, left, right}) f =
+  Equal {type = renameNtrl type f, left = rename left f, right = rename right f}
+renameNtrl (EqualL {left, right}) f = EqualL {left = renameNtrl left f, right = rename right f}
+renameNtrl (EqualR {left, right}) f =
+  EqualR {left = renameCnstr left f, right = renameNtrl right f}
+renameNtrl (EqualStuck {left, right}) f =
+  EqualStuck {left = renameCnstr left f, right = renameCnstr right f}
+renameNtrl (CastL {oldType, newType, value}) f =
+ CastL {oldType = renameNtrl oldType f, newType = rename newType f, value = rename value f}
+renameNtrl (CastR {oldType, newType, value}) f =
+ CastR {oldType = renameCnstr oldType f, newType = renameNtrl newType f, value = rename value f}
+renameNtrl (CastStuck {oldType, newType, value}) f =
+ CastStuck
+   { oldType = renameCnstr oldType f
+   , newType = renameCnstr newType f
+   , value = rename value f
+   }
 
 rename (Ntrl t) f = Ntrl $ renameNtrl t f
 rename (Cnstr t) f = Cnstr $ renameCnstr t f
@@ -249,12 +255,13 @@ Unsorted.Rename Relevance Constructor where
 export
 Unsorted.Rename Relevance Neutral where
   rename = renameNtrl
-  
+
 export
 Sorted.Rename Relevance NormalForm where
   rename = NormalForm.rename
 
 export
-PointedRename Relevance (\r => (String, (s : Universe ** relevance s = r))) NormalForm where
+PointedRename Relevance (\r => Maybe String) NormalForm where
   point {s = Irrelevant} _ _ = Irrel
-  point {s = Relevant} (var, (s@(Set _) ** prf)) i = Ntrl (Var var s Set i)
+  point {s = Relevant} var i =
+    Ntrl (Var {var = maybe "" id var, i})
diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr
index ed06fa2..2ea6296 100644
--- a/src/Obs/NormalForm/Normalise.idr
+++ b/src/Obs/NormalForm/Normalise.idr
@@ -25,11 +25,15 @@ LogNormalForm : Type -> Sorted.Family Relevance
 LogNormalForm ann b ctx = Logging ann (NormalForm b ctx)
 
 0
+LogDeclForm : Type -> Unsorted.Family Relevance
+LogDeclForm ann ctx = Logging ann (DeclForm ctx)
+
+0
 LogNormalForm' : Type -> Sorted.Family Relevance
 LogNormalForm' ann b ctx = Either (Logging ann (NormalForm b ctx)) (Elem b ctx)
 
 -- Copied and specialised from Obs.Substitution
-lift : (ctx : List (r ** (String, (s ** relevance s = r))))
+lift : (ctx : List (r ** Maybe String))
   -> Map ctx' (LogNormalForm' ann) ctx''
   -> Map (map DPair.fst ctx ++ ctx') (LogNormalForm' ann) (map DPair.fst ctx ++ ctx'')
 lift [] f = f
@@ -42,202 +46,467 @@ lift ((s ** y) :: ctx) f = add (LogNormalForm' ann)
 subst' : NormalForm ~|> Hom (LogNormalForm' ann) (LogNormalForm ann)
 
 export
-doApp : {domain : _} ->
-  NormalForm (function domain codomain) ctx ->
-  NormalForm domain ctx ->
-  LogNormalForm ann codomain ctx
-doApp (Ntrl t) u = pure (Ntrl $ App _ t u)
-doApp (Cnstr (Lambda s var t)) u = inScope "doApp" $ do
-  trace $ pretty {ann} "substituting" <++> pretty u <+> softline <+> pretty "for \{var} in" <++> pretty t
-  let Yes Refl = decEq domain (relevance s)
+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)
+
+export
+map1 : {s' : _} ->
+  NormalForm s (s :: ctx) ->
+  NormalForm s' (s :: ctx) ->
+  LogNormalForm ann s' (s :: ctx)
+map1 t u = subst' u (add (LogNormalForm' ann) (Left $ pure t) (Right . There))
+
+export
+doApp : {domainRel : _} ->
+  (fun : NormalForm (function domainRel codomainRel) ctx) ->
+  (arg : NormalForm domainRel ctx) ->
+  LogNormalForm ann codomainRel ctx
+
+doApp (Ntrl fun) arg = pure $ Ntrl $ App {argRel = _, fun, arg}
+doApp (Cnstr (Lambda {domainRel = domainRel', var, body})) arg = do
+  let Yes Refl = decEq domainRel domainRel'
     | No _ => fatal "internal relevance mismatch"
-  subst' t (add (LogNormalForm' ann) (Left $ pure u) Right)
-doApp (Cnstr t) u = inScope "wrong constructor for apply" $ fatal t
-doApp Irrel u = pure Irrel
+
+  subst1 arg body
+doApp (Cnstr t) arg = inScope "wrong constructor for apply" $ fatal t
+doApp Irrel arg = pure Irrel
 
 export
-doFst : (fst, snd : _) -> NormalForm (pair fst snd) ctx -> LogNormalForm ann fst ctx
-doFst Irrelevant snd t = pure Irrel
-doFst Relevant snd (Ntrl t) = pure (Ntrl $ Fst snd t)
-doFst Relevant snd (Cnstr (Pair (Set _) s' prf t u)) = pure t
-doFst Relevant snd (Cnstr t) = inScope "wrong constructor for fst" $ fatal t
+doFst : (firstRel, secondRel : _) ->
+  (arg : NormalForm (pair firstRel secondRel) ctx) ->
+  LogNormalForm ann firstRel ctx
+
+doFst Irrelevant secondRel arg = pure Irrel
+doFst Relevant secondRel (Ntrl arg) = pure $ Ntrl $ First {secondRel, arg}
+doFst Relevant secondRel (Cnstr (Pair {indexRel = Relevant, elementRel, prf, first, second})) =
+  pure first
+doFst Relevant secondRel (Cnstr t) = inScope "wrong constructor for fst" $ fatal t
 
 export
-doSnd : (fst, snd : _) -> NormalForm (pair fst snd) ctx -> LogNormalForm ann snd ctx
-doSnd fst Irrelevant t = pure Irrel
-doSnd fst Relevant t =
-  let t' : NormalForm Relevant ctx
-      t' = rewrite sym $ pairRelevantRight fst in t
-  in case t' of
-  Ntrl t => pure (Ntrl $ Snd fst t)
-  Cnstr (Pair _ (Set _) prf t u) => pure u
+doSnd : (firstRel, secondRel : _) ->
+  (arg : NormalForm (pair firstRel secondRel) ctx) ->
+  LogNormalForm ann secondRel ctx
+
+doSnd firstRel Irrelevant arg = pure Irrel
+doSnd firstRel Relevant arg =
+  let arg' : NormalForm Relevant ctx
+      arg' = rewrite sym $ pairRelevantRight firstRel in arg
+  in case arg' of
+  Ntrl arg => pure $ Ntrl $ Second {firstRel, arg}
+  Cnstr (Pair {indexRel, elementRel = Relevant, prf, first, second}) => pure second
   Cnstr t => inScope "wrong constructor for snd" $ fatal t
 
 export
-doIf : {r : _} ->
-  NormalForm Relevant ctx ->
-  NormalForm r ctx ->
-  NormalForm r ctx ->
-  LogNormalForm ann r ctx
-doIf {r = Irrelevant} t u v = pure Irrel
-doIf {r = Relevant} (Ntrl t) u v = pure (Ntrl $ If t u v)
-doIf {r = Relevant} (Cnstr True) u v = pure u
-doIf {r = Relevant} (Cnstr False) u v = pure v
-doIf {r = Relevant} (Cnstr t) u v = inScope "wrong constructor for case" $ fatal t
+doIf : {rel : _} ->
+  (discriminant : NormalForm Relevant ctx) ->
+  (true, false : NormalForm rel ctx) ->
+  LogNormalForm ann rel ctx
+doIf {rel = Irrelevant} discriminant true false = pure Irrel
+doIf {rel = Relevant} (Ntrl discriminant) true false = pure $ Ntrl $ If {discriminant, true, false}
+doIf {rel = Relevant} (Cnstr True) true false = pure true
+doIf {rel = Relevant} (Cnstr False) true false = pure false
+doIf {rel = Relevant} (Cnstr t) true false = inScope "wrong constructor for if" $ fatal t
 
 export
-doAbsurd : (r : _) -> NormalForm r ctx
+doAbsurd : (rel : _) -> NormalForm rel ctx
 doAbsurd Irrelevant = Irrel
 doAbsurd Relevant = Ntrl Absurd
 
 export
-doCast : (r : _) -> (a, b : TypeNormalForm ctx) -> NormalForm r ctx -> LogNormalForm ann r ctx
+doCast : (rel : _) ->
+  (oldType, newType : TypeNormalForm ctx) ->
+  (value : NormalForm rel ctx) ->
+  LogNormalForm ann rel ctx
 
-doCastR : (a : Constructor ctx) ->
-  (b : TypeNormalForm ctx) ->
-  NormalForm Relevant ctx ->
+doCastHelper : (oldType, newType : Constructor ctx) ->
+  (value : NormalForm Relevant ctx) ->
   LogNormalForm ann Relevant ctx
-doCastR a (Ntrl b) t = pure (Ntrl $ CastR a b t)
-doCastR (Universe _) (Cnstr (Universe _)) t = pure t
-doCastR ty@(Pi s s'@(Set _) var a b) (Cnstr ty'@(Pi l l' _ a' b')) t =
-  let y : NormalForm (relevance s) (relevance s :: ctx)
-      y = point (var, (s ** Refl)) Here
+doCastHelper (Universe {s}) (Universe {s = s'}) value = pure value
+doCastHelper
+  oldType@(Pi {domainSort, codomainSort, domain, codomain})
+  newType@(Pi
+    { domainSort = domainSort'
+    , codomainSort = codomainSort'
+    , domain = domain'
+    , codomain = codomain'
+    })
+  value =
+  let y : NormalForm (relevance domainSort) (relevance domainSort :: ctx)
+      y = point domain.var Here
   in do
-  let Yes Refl = decEq (s, s') (l, l')
-    | No _ => pure (Ntrl $ CastStuck ty ty' t)
-  x <- assert_total (doCast (relevance s) (weaken [relevance s] a') (weaken [relevance s] a) y)
-  b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure x) (Right . There)))
-  b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure y) (Right . There)))
-  t <- assert_total (doApp (Sorted.weaken [relevance s] t) x)
-  t <- assert_total (doCast Relevant b b' t)
-  pure (Cnstr $ Lambda s var t)
-doCastR ty@(Sigma s@(Set k) s' var a b) (Cnstr ty'@(Sigma l l' _ a' b')) t = do
-  let Yes Refl = decEq (s, s') (l, l')
-    | No _ => pure (Ntrl $ CastStuck ty ty' t)
-  t1 <- doFst Relevant (relevance s') t
-  u1 <- assert_total (doCast Relevant a a' t)
-  b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t1) Right))
-  b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure u1) Right))
-  t2 <- doSnd Relevant (relevance s') t
-  u2 <- assert_total (doCast (relevance s') b b' t2)
-  pure (Cnstr $ Pair (Set k) s' Set u1 u2)
-doCastR ty@(Sigma Prop s'@(Set k) var a b) (Cnstr ty'@(Sigma Prop l' _ a' b')) t = do
-  let Yes Refl = decEq s' l'
-    | No _ => pure (Ntrl $ CastStuck ty ty' t)
-  b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure Irrel) Right))
-  b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure Irrel) Right))
-  t2 <- doSnd Irrelevant Relevant t
-  u2 <- assert_total (doCast Relevant b b' t2)
-  pure (Cnstr $ Pair Prop (Set k) Set Irrel u2)
-doCastR Bool (Cnstr Bool) t = pure t
-doCastR a (Cnstr b) t = pure (Ntrl $ CastStuck a b t)
-
-doCast Irrelevant a b t = pure Irrel
-doCast Relevant (Ntrl a) b t = pure (Ntrl $ CastL a b t)
-doCast Relevant (Cnstr a) b t = doCastR a b t
+
+  let Yes Refl = decEq (domainSort, codomainSort) (domainSort', codomainSort')
+    | No _ => pure $ Ntrl $ CastStuck {oldType, newType, value}
+
+  let domainType = weaken [relevance domainSort] domain.type
+  let domainType' = weaken [relevance domainSort] domain'.type
+
+  x <- doCast
+    { rel = relevance domainSort
+    , oldType = assert_smaller oldType domainType'
+    , newType = assert_smaller newType domainType
+    , value = y
+    }
+
+  codomainType <- map1 x codomain
+  codomainType' <- map1 y codomain'
+
+  call <- doApp (weaken [relevance domainSort] value) x
+  body <- doCast
+    { rel = Relevant
+    , oldType = assert_smaller oldType codomainType
+    , newType = assert_smaller newType codomainType'
+    , value = call
+    }
+
+  pure $ Cnstr $ Lambda {domainRel = relevance domainSort, var = Nothing, body}
+doCastHelper
+  oldType@(Sigma {indexSort = indexSort@(Set k), elementSort, index, element})
+  newType@(Sigma
+    { indexSort = indexSort'
+    , elementSort = elementSort'
+    , index = index'
+    , element = element'
+    })
+  value = do
+  let Yes Refl = decEq (indexSort, elementSort) (indexSort', elementSort')
+    | No _ => pure $ Ntrl $ CastStuck {oldType, newType, value}
+
+  first <- doFst Relevant (relevance elementSort) value
+  second <- doSnd Relevant (relevance elementSort) value
+
+  first' <- doCast
+    { rel = Relevant
+    , oldType = assert_smaller oldType index.type
+    , newType = assert_smaller newType index'.type
+    , value = first
+    }
+
+  elementType <- subst1 first element
+  elementType' <- subst1 first' element'
+
+  second' <- doCast
+    { rel = relevance elementSort
+    , oldType = assert_smaller oldType elementType
+    , newType = assert_smaller newType elementType'
+    , value = second
+    }
+
+  pure $ Cnstr $ Pair
+    { indexRel = Relevant
+    , elementRel = relevance elementSort
+    , prf = Relevant
+    , first = first'
+    , second = second'
+    }
+doCastHelper
+  oldType@(Sigma {indexSort = Prop, elementSort = elementSort@(Set k), index, element})
+  newType@(Sigma
+    { indexSort = Prop
+    , elementSort = elementSort'
+    , index = index'
+    , element = element'
+    })
+  value = do
+  let Yes Refl = decEq elementSort elementSort'
+    | No _ => pure $ Ntrl $ CastStuck {oldType, newType, value}
+
+  first <- doFst Irrelevant Relevant value
+  second <- doSnd Irrelevant Relevant value
+
+  first' <- doCast
+    { rel = Irrelevant
+    , oldType = assert_smaller oldType index.type
+    , newType = assert_smaller newType index'.type
+    , value = first
+    }
+
+  elementType <- subst1 first element
+  elementType' <- subst1 first' element'
+
+  second' <- doCast
+    { rel = Relevant
+    , oldType = assert_smaller oldType elementType
+    , newType = assert_smaller newType elementType'
+    , value = second
+    }
+
+  pure $ Cnstr $ Pair
+    { indexRel = Irrelevant
+    , elementRel = Relevant
+    , prf = Relevant
+    , first = first'
+    , second = second'
+    }
+doCastHelper Bool Bool value = pure value
+doCastHelper oldType newType value = pure $ Ntrl $ CastStuck {oldType, newType, value}
+
+doCast Irrelevant oldType newType value = pure Irrel
+doCast Relevant (Ntrl oldType) newType value = pure $ Ntrl $ CastL {oldType, newType, value}
+doCast Relevant (Cnstr oldType) (Ntrl newType) value =
+  pure $ Ntrl $ CastR {oldType, newType, value}
+doCast Relevant (Cnstr oldType) (Cnstr newType) value = doCastHelper oldType newType value
 
 export
-doEqual : (r : _) ->
-  (a : TypeNormalForm ctx) ->
-  NormalForm r ctx ->
-  NormalForm r ctx ->
+doEqual : (rel : _) ->
+  (type : TypeNormalForm ctx) ->
+  (left, right : NormalForm rel ctx) ->
   LogNormalForm ann Relevant ctx
 
--- Relies heavily on typing
-doEqualR : (a : Constructor ctx) -> (b : TypeNormalForm ctx) -> LogNormalForm ann Relevant ctx
-doEqualR a (Ntrl b) = pure (Ntrl $ EqualR a b)
-doEqualR (Universe _) (Cnstr (Universe s)) = pure (Cnstr Top)
-doEqualR ty@(Pi s s' var a b) (Cnstr ty'@(Pi l l' _ a' b')) =
-  let u : NormalForm (relevance s) (relevance s :: ctx)
-      u = point (var, (s ** Refl)) Here
+equalHelper : (left, right : Constructor ctx) -> LogNormalForm ann Relevant ctx
+equalHelper (Universe {s}) (Universe {s = s'}) = pure (Cnstr Top)
+equalHelper
+  left@(Pi {domainSort, codomainSort, domain, codomain})
+  right@(Pi
+    { domainSort = domainSort'
+    , codomainSort = codomainSort'
+    , domain = domain'
+    , codomain = codomain'
+    }) =
+  let y : NormalForm (relevance domainSort) (relevance domainSort :: Irrelevant :: ctx)
+      y = point domain.var Here
   in do
-  let Yes Refl = decEq (s, s') (l, l')
-    | No _ => pure (Ntrl $ EqualStuck ty ty')
-  eq1 <- assert_total (doEqual Relevant (cast s) a' a)
-  t <- doCast (relevance s) (weaken [relevance s] a') (weaken [relevance s] a) u
-  b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t) (Right . There)))
-  b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure u) (Right . There)))
-  eq2 <- assert_total (doEqual Relevant (cast s') b b')
-  pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [Irrelevant] $ Pi s Prop var a eq2))
-doEqualR ty@(Sigma s s' var a b) (Cnstr ty'@(Sigma l l' _ a' b')) =
-  let t : NormalForm (relevance s) (relevance s :: ctx)
-      t = point (var, (s ** Refl)) Here
+
+  let Yes Refl = decEq (domainSort, codomainSort) (domainSort', codomainSort')
+    | No _ => pure $ Ntrl $ EqualStuck {left, right}
+
+  domainEqual <- doEqual
+    { rel = Relevant
+    , type = cast domainSort
+    , left = assert_smaller right domain'.type
+    , right = assert_smaller left domain.type
+    }
+
+  let domainType = Sorted.weaken [relevance domainSort, Irrelevant] domain.type
+  let domainType' = Sorted.weaken [relevance domainSort, Irrelevant] domain'.type
+
+  x <- doCast
+    { rel = relevance domainSort
+    , oldType = domainType'
+    , newType = domainType
+    , value = y
+    }
+
+  codomainType <- map1 x (rename codomain (add Elem Here (There . There)))
+  codomainType' <- map1 y (rename codomain' (add Elem Here (There . There)))
+
+  codomainEqual <- doEqual
+    { rel = Relevant
+    , type = cast codomainSort
+    , left = assert_smaller left codomainType
+    , right = assert_smaller right codomainType'
+    }
+
+  let returnElement = Cnstr $ Pi
+       { domainSort = domainSort
+       , codomainSort = Prop
+       , domain = MkDecl Nothing (Sorted.weaken [Irrelevant] domain.type)
+       , codomain = codomainEqual
+       }
+
+  pure $ Cnstr $ Sigma
+    { indexSort = Prop
+    , elementSort = Prop
+    , index = MkDecl Nothing domainEqual
+    , element = returnElement
+    }
+equalHelper
+  left@(Sigma {indexSort, elementSort, index, element})
+  right@(Sigma
+    { indexSort = indexSort'
+    , elementSort = elementSort'
+    , index = index'
+    , element = element'
+    }) =
+  let x : NormalForm (relevance indexSort) (relevance indexSort :: Irrelevant :: ctx)
+      x = point index.var Here
   in do
-  let Yes Refl = decEq (s, s') (l, l')
-    | No _ => pure (Ntrl $ EqualStuck ty ty')
-  eq1 <- assert_total (doEqual Relevant (cast s) a a')
-  u <- doCast (relevance s) (weaken [relevance s] a) (weaken [relevance s] a') t
-  b <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t) (Right . There)))
-  b' <- assert_total (subst' b' (add (LogNormalForm' ann) (Left $ pure u) (Right . There)))
-  eq2 <- assert_total (doEqual Relevant (cast s') b b')
-  pure (Cnstr $ Sigma Prop Prop "_" eq1 (Cnstr $ Unsorted.weaken [Irrelevant] $ Pi s Prop var a eq2))
-doEqualR Bool (Cnstr Bool) = pure (Cnstr Top)
-doEqualR Top (Cnstr Top) = pure (Cnstr Top)
-doEqualR Bottom (Cnstr Bottom) = pure (Cnstr Top)
-doEqualR a (Cnstr b) = pure (Ntrl $ EqualStuck a b)
 
-export
-doEqualSet : (a, b : TypeNormalForm ctx) -> LogNormalForm ann Relevant ctx
-doEqualSet (Ntrl a) b = pure (Ntrl $ EqualL a b)
-doEqualSet (Cnstr a) b = doEqualR a b
-
-doEqual Irrelevant a t u = pure (Cnstr Top)
-doEqual Relevant (Ntrl a) t u = pure (Ntrl $ Equal a t u)
-doEqual Relevant (Cnstr (Universe Prop)) t u = do
-  pure (Cnstr $ Sigma Prop Prop ""
-    (Cnstr $ Pi Prop Prop "" t (Sorted.weaken [Irrelevant] u))
-    (Cnstr $ Unsorted.weaken [Irrelevant] $ Pi Prop Prop "" u (Sorted.weaken [Irrelevant] t)))
-doEqual Relevant (Cnstr (Universe (Set _))) t u = doEqualSet t u
-doEqual Relevant (Cnstr (Pi s (Set k) var a b)) t u =
-  let x : NormalForm (relevance s) (relevance s :: ctx)
-      x = point (var, (s ** Refl)) Here
+  let Yes Refl = decEq (indexSort, elementSort) (indexSort', elementSort')
+    | No _ => pure $ Ntrl $ EqualStuck {left, right}
+
+  indexEqual <- doEqual
+    { rel = Relevant
+    , type = cast indexSort
+    , left = assert_smaller left index.type
+    , right = assert_smaller right index'.type
+    }
+
+  let indexType = Sorted.weaken [relevance indexSort, Irrelevant] index.type
+  let indexType' = Sorted.weaken [relevance indexSort, Irrelevant] index'.type
+
+  y <- doCast
+    { rel = relevance indexSort
+    , oldType = indexType
+    , newType = indexType'
+    , value = x
+    }
+
+  elementType <- map1 x (rename element (add Elem Here (There . There)))
+  elementType' <- map1 y (rename element' (add Elem Here (There . There)))
+
+  elementEqual <- doEqual
+    { rel = Relevant
+    , type = cast elementSort
+    , left = assert_smaller left elementType
+    , right = assert_smaller right elementType'
+    }
+
+  let returnElement = Cnstr $ Pi
+       { domainSort = indexSort
+       , codomainSort = Prop
+       , domain = MkDecl Nothing (Sorted.weaken [Irrelevant] index.type)
+       , codomain = elementEqual
+       }
+
+  pure $ Cnstr $ Sigma
+    { indexSort = Prop
+    , elementSort = Prop
+    , index = MkDecl Nothing indexEqual
+    , element = returnElement
+    }
+equalHelper Bool Bool = pure (Cnstr Top)
+equalHelper left right = pure $ Ntrl $ EqualStuck {left, right}
+
+doEqualType : (left, right : TypeNormalForm ctx) -> LogNormalForm ann Relevant ctx
+doEqualType (Ntrl left) right = pure $ Ntrl $ EqualL {left, right}
+doEqualType (Cnstr left) (Ntrl right) = pure $ Ntrl $ EqualR {left, right}
+doEqualType (Cnstr left) (Cnstr right) = equalHelper left right
+
+doEqual Irrelevant type left right = pure $ Cnstr Top
+doEqual Relevant (Ntrl type) left right = pure $ Ntrl $ Equal {type, left, right}
+doEqual Relevant (Cnstr (Universe {s = Prop})) left right = do
+  let leftToRight = Cnstr $ Pi
+        { domainSort = Prop
+        , codomainSort = Prop
+        , domain = MkDecl Nothing left
+        , codomain = weaken [Irrelevant] right
+        }
+  let rightToLeft = Cnstr $ Pi
+        { domainSort = Prop
+        , codomainSort = Prop
+        , domain = MkDecl Nothing right
+        , codomain = weaken [Irrelevant] left
+        }
+  pure $ Cnstr $ Sigma
+    { indexSort = Prop
+    , elementSort = Prop
+    , index = MkDecl Nothing leftToRight
+    , element = Sorted.weaken [Irrelevant] rightToLeft
+    }
+doEqual Relevant (Cnstr (Universe {s = Set _})) left right = doEqualType left right
+doEqual Relevant (Cnstr (Pi {domainSort, codomainSort, domain, codomain})) left right =
+  let var : NormalForm (relevance domainSort) (relevance domainSort :: ctx)
+      var = point domain.var Here
   in do
-  t <- assert_total (doApp (weaken [relevance s] t) x)
-  u <- assert_total (doApp (weaken [relevance s] u) x)
-  eq <- doEqual Relevant b t u
-  pure (Cnstr $ Pi s Prop var a eq)
-doEqual Relevant (Cnstr (Sigma s@(Set _) s' var a b)) t u = do
-  t1 <- doFst Relevant (relevance s') t
-  u1 <- doFst Relevant (relevance s') u
-  t2 <- doSnd Relevant (relevance s') t
-  u2 <- doSnd Relevant (relevance s') u
-  eq1 <- doEqual Relevant a t1 u1
-  bt1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure t1) Right))
-  bu1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure u1) Right))
-  t2' <- doCast (relevance s') bt1 bu1 t2
-  eq2 <- doEqual (relevance s') (assert_smaller b bu1) t2' u2
-  pure (Cnstr $ Sigma Prop Prop "_" eq1 (Sorted.weaken [Irrelevant] eq2))
-doEqual Relevant (Cnstr (Sigma Prop (Set k) var a b)) t u = do
-  t2 <- doSnd Irrelevant Relevant t
-  u2 <- doSnd Irrelevant Relevant u
-  bt1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure $ Irrel) Right))
-  bu1 <- assert_total (subst' b (add (LogNormalForm' ann) (Left $ pure $ Irrel) Right))
-  t2' <- doCast Relevant bt1 bu1 t2
-  eq2 <- doEqual Relevant (assert_smaller b bu1) t2' u2
-  pure (Cnstr $ Sigma Prop Prop "_" (Cnstr Top) (Sorted.weaken [Irrelevant] eq2))
-doEqual Relevant (Cnstr Bool) t u = do
-  relevant <- doIf u (Cnstr Top) (Cnstr Bottom)
-  irrelevant <- doIf u (Cnstr Bottom) (Cnstr Top)
-  doIf t relevant irrelevant
-doEqual Relevant (Cnstr a) t u = inScope "wrong constructor for equal" $ fatal a
+
+  leftApp <- doApp (weaken [relevance domainSort] left) var
+  rightApp <- doApp (weaken [relevance domainSort] right) var
+
+  equality <- doEqual
+    { rel = Relevant
+    , type = codomain
+    , left = assert_smaller left leftApp
+    , right = assert_smaller right rightApp
+    }
+
+  pure $ Cnstr $ Pi {domainSort, codomainSort = Prop, domain, codomain = equality}
+doEqual
+  Relevant
+  (Cnstr (Sigma {indexSort = indexSort@(Set _), elementSort, index, element}))
+  left
+  right = do
+  leftFirst <- doFst Relevant (relevance elementSort) left
+  rightFirst <- doFst Relevant (relevance elementSort) right
+  leftSecond <- doSnd Relevant (relevance elementSort) left
+  rightSecond <- doSnd Relevant (relevance elementSort) right
+
+  leftEquality <- doEqual
+    { rel = Relevant
+    , type = index.type
+    , left = assert_smaller left leftFirst
+    , right = assert_smaller right rightFirst
+    }
+
+  leftElementType <- subst1 leftFirst element
+  rightElementType <- subst1 rightFirst element
+
+  leftSecond <- doCast (relevance elementSort) leftElementType rightElementType leftSecond
+
+  rightEquality <- doEqual
+    { rel = relevance elementSort
+    , type = rightElementType
+    , left = assert_smaller left leftSecond
+    , right = assert_smaller right rightSecond
+    }
+
+  pure $ Cnstr $ Sigma
+    { indexSort = Prop
+    , elementSort = Prop
+    , index = MkDecl Nothing leftEquality
+    , element = Sorted.weaken [Irrelevant] rightEquality
+    }
+doEqual
+  Relevant
+  (Cnstr (Sigma {indexSort = Prop, elementSort = elementSort@(Set _), index, element}))
+  left
+  right = do
+  leftFirst <- doFst Irrelevant Relevant left
+  rightFirst <- doFst Irrelevant Relevant right
+  leftSecond <- doSnd Irrelevant Relevant left
+  rightSecond <- doSnd Irrelevant Relevant right
+
+  leftEquality <- doEqual
+    { rel = Irrelevant
+    , type = index.type
+    , left = assert_smaller left leftFirst
+    , right = assert_smaller right rightFirst
+    }
+
+  leftElementType <- subst1 leftFirst element
+  rightElementType <- subst1 rightFirst element
+
+  leftSecond <- doCast Relevant leftElementType rightElementType leftSecond
+
+  rightEquality <- doEqual
+    { rel = Relevant
+    , type = rightElementType
+    , left = assert_smaller left leftSecond
+    , right = assert_smaller right rightSecond
+    }
+
+  pure $ Cnstr $ Sigma
+    { indexSort = Prop
+    , elementSort = Prop
+    , index = MkDecl Nothing leftEquality
+    , element = Sorted.weaken [Irrelevant] rightEquality
+    }
+doEqual Relevant (Cnstr Bool) left right = do
+  whenLeftTrue <- doIf right (Cnstr Top) (Cnstr Bottom)
+  whenLeftFalse <- doIf right (Cnstr Bottom) (Cnstr Top)
+  doIf left whenLeftTrue whenLeftFalse
+doEqual Relevant (Cnstr t) left right = inScope "wrong constructor for equal" $ fatal t
+
+substDecl : DeclForm ~|> Hom (LogNormalForm' ann) (LogDeclForm ann)
+substDecl (MkDecl var type) f = pure (MkDecl var !(subst' type f))
 
 substCnstr : Constructor ~|> Hom (LogNormalForm' ann) (LogConstructor ann)
-substCnstr (Universe s) f = pure (Universe s)
-substCnstr (Pi s s' var a b) f = do
-  a <- subst' a f
-  b <- subst' b (lift [(_ ** (var, (s ** Refl)))] f)
-  pure (Pi s s' var a b)
-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 (lift [(_ ** (var, (s ** Refl)))] f)
-  pure (Sigma s s' var a b)
-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 (Universe {s}) f = pure (Universe {s})
+substCnstr (Pi {domainSort, codomainSort, domain, codomain}) f = do
+  domain <- substDecl domain f
+  codomain <- subst' codomain (lift [(_ ** domain.var)] f)
+  pure (Pi {domainSort, codomainSort, domain, codomain})
+substCnstr (Lambda {domainRel, var, body}) f = do
+  body <- subst' body (lift [(_ ** var)] f)
+  pure (Lambda {domainRel, var, body})
+substCnstr (Sigma {indexSort, elementSort, index, element}) f = do
+  index <- substDecl index f
+  element <- subst' element (lift [(_ ** index.var)] f)
+  pure (Sigma {indexSort, elementSort, index, element})
+substCnstr (Pair {indexRel, elementRel, prf, first, second}) f = do
+  first <- subst' first f
+  second <- subst' second f
+  pure (Pair {indexRel, elementRel, prf, first, second})
 substCnstr Bool f = pure Bool
 substCnstr True f = pure True
 substCnstr False f = pure False
@@ -245,57 +514,58 @@ substCnstr Top f = pure Top
 substCnstr Bottom f = pure Bottom
 
 substNtrl : Neutral ~|> Hom (LogNormalForm' ann) (LogNormalForm ann Relevant)
-substNtrl (Var var sort prf i) f = case f i of
+substNtrl (Var {var, i}) f = case f i of
   Left t => t
-  Right j => pure (Ntrl $ Var var sort prf j)
-substNtrl (App r t u) f = do
-  t <- substNtrl t f
-  u <- subst' u f
-  assert_total (doApp t u)
-substNtrl (Fst r t) f = do
-  t <- substNtrl t f
-  doFst Relevant r t
-substNtrl (Snd r t) f = do
-  t <- substNtrl t f
-  doSnd r Relevant $ rewrite pairRelevantRight r in t
-substNtrl (If t u v) f = do
-  t <- substNtrl t f
-  u <- subst' u f
-  v <- subst' v f
-  doIf t u v
+  Right i => pure $ Ntrl $ Var {var, i}
+substNtrl (App {argRel, fun, arg}) f = do
+  fun <- substNtrl fun f
+  arg <- subst' arg f
+  assert_total (doApp fun arg)
+substNtrl (First {secondRel, arg}) f = do
+  arg <- substNtrl arg f
+  doFst Relevant secondRel arg
+substNtrl (Second {firstRel, arg}) f = do
+  arg <- substNtrl arg f
+  let arg = rewrite pairRelevantRight firstRel in arg
+  doSnd firstRel Relevant arg
+substNtrl (If {discriminant, true, false}) f = do
+  discriminant <- substNtrl discriminant f
+  true <- subst' true f
+  false <- subst' false f
+  doIf discriminant true false
 substNtrl Absurd f = pure (doAbsurd Relevant)
-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 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
-  doCast _ a b t
-substNtrl (CastR a b t) f = do
-  a <- substCnstr a f
-  b <- substNtrl b f
-  t <- subst' t f
-  doCastR a b t
-substNtrl (CastStuck a b t) f = do
-  a <- substCnstr a f
-  b <- substCnstr b f
-  t <- subst' t f
-  pure (Ntrl $ CastStuck a b t)
+substNtrl (Equal {type, left, right}) f = do
+  type <- substNtrl type f
+  left <- subst' left f
+  right <- subst' right f
+  assert_total (doEqual Relevant type left right)
+substNtrl (EqualL {left, right}) f = do
+  left <- substNtrl left f
+  right <- subst' right f
+  assert_total (doEqualType left right)
+substNtrl (EqualR {left, right}) f = do
+  left <- substCnstr left f
+  right <- substNtrl right f
+  assert_total (doEqualType (Cnstr left) right)
+substNtrl (EqualStuck {left, right}) f = do
+  left <- substCnstr left f
+  right <- substCnstr right f
+  assert_total (doEqualType (Cnstr left) (Cnstr right))
+substNtrl (CastL {oldType, newType, value}) f = do
+  oldType <- substNtrl oldType f
+  newType <- subst' newType f
+  value <- subst' value f
+  assert_total (doCast Relevant oldType newType value)
+substNtrl (CastR {oldType, newType, value}) f = do
+  oldType <- substCnstr oldType f
+  newType <- substNtrl newType f
+  value <- subst' value f
+  assert_total (doCast Relevant (Cnstr oldType) newType value)
+substNtrl (CastStuck {oldType, newType, value}) f = do
+  oldType <- substCnstr oldType f
+  newType <- substCnstr newType f
+  value <- subst' value f
+  assert_total (doCast Relevant (Cnstr oldType) (Cnstr newType) value)
 
 subst' (Ntrl t) f = substNtrl t f
 subst' (Cnstr t) f = pure $ Cnstr !(substCnstr t f)
@@ -304,9 +574,3 @@ subst' Irrel f = pure Irrel
 export
 subst : NormalForm ~|> Hom (LogNormalForm ann) (LogNormalForm ann)
 subst t f = subst' t (Left . f)
-
--- Utilities -------------------------------------------------------------------
-
-export
-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 68591ee..b00f5a8 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -29,11 +29,6 @@ data ObsTokenKind
   | OTTrue
   | OTFalse
   | OTIf
-  | OTContainer
-  | OTTag
-  | OTPosition
-  | OTNext
-  | OTSem
   | OTPoint
   | OTVoid
   | OTAbsurd
@@ -43,7 +38,6 @@ data ObsTokenKind
   | OTCastRefl
   -- Special symbols
   | OTUnit
-  | OTTriangle
   -- Grouping symbols
   | OTPOpen
   | OTPClose
@@ -59,7 +53,6 @@ data ObsTokenKind
   | OTTilde
   | OTEqual
   | OTColon
-  | OTPipe
 
 Eq ObsTokenKind where
   OTNewlines == OTNewlines = True
@@ -74,11 +67,6 @@ Eq ObsTokenKind where
   OTTrue == OTTrue = True
   OTFalse == OTFalse = True
   OTIf == OTIf = True
-  OTContainer == OTContainer = True
-  OTTag == OTTag = True
-  OTPosition == OTPosition = True
-  OTNext == OTNext = True
-  OTSem == OTSem = True
   OTPoint == OTPoint = True
   OTVoid == OTVoid = True
   OTAbsurd == OTAbsurd = True
@@ -87,7 +75,6 @@ Eq ObsTokenKind where
   OTCast == OTCast = True
   OTCastRefl == OTCastRefl = True
   OTUnit == OTUnit = True
-  OTTriangle == OTTriangle = True
   OTPOpen == OTPOpen = True
   OTPClose == OTPClose = True
   OTAOpen == OTAOpen = True
@@ -101,9 +88,43 @@ Eq ObsTokenKind where
   OTTilde == OTTilde = True
   OTEqual == OTEqual = True
   OTColon == OTColon = True
-  OTPipe == OTPipe = True
   _ == _ = False
 
+Show ObsTokenKind where
+  show OTNewlines = "\\n"
+  show OTSpaces = " "
+  show OTIdent = "ident"
+  show OTProp = "Prop"
+  show OTSet = "Set"
+  show OTNat = "nat"
+  show OTFst = "fst"
+  show OTSnd = "snd"
+  show OTBool = "Bool"
+  show OTTrue = "True"
+  show OTFalse = "False"
+  show OTIf = "if"
+  show OTPoint = "tt"
+  show OTVoid = "Void"
+  show OTAbsurd = "absurd"
+  show OTRefl = "refl"
+  show OTTransp = "transp"
+  show OTCast = "cast"
+  show OTCastRefl = "castRefl"
+  show OTUnit = "()"
+  show OTPOpen = "("
+  show OTPClose = ")"
+  show OTAOpen = "<"
+  show OTAClose = ">"
+  show OTBackslash = "\\"
+  show OTSlash = "/"
+  show OTThinArrow = "->"
+  show OTFatArrow = "=>"
+  show OTProduct = "**"
+  show OTComma = ","
+  show OTTilde = "~"
+  show OTEqual = "="
+  show OTColon = ":"
+
 TokenKind ObsTokenKind where
   TokType OTIdent = String
   TokType OTNat   = Nat
@@ -121,11 +142,6 @@ TokenKind ObsTokenKind where
   tokValue OTTrue s = ()
   tokValue OTFalse s = ()
   tokValue OTIf s = ()
-  tokValue OTContainer s = ()
-  tokValue OTTag s = ()
-  tokValue OTPosition s = ()
-  tokValue OTNext s = ()
-  tokValue OTSem s = ()
   tokValue OTPoint s = ()
   tokValue OTVoid s = ()
   tokValue OTAbsurd s = ()
@@ -134,7 +150,6 @@ TokenKind ObsTokenKind where
   tokValue OTCast s = ()
   tokValue OTCastRefl s = ()
   tokValue OTUnit s = ()
-  tokValue OTTriangle s = ()
   tokValue OTPOpen s = ()
   tokValue OTPClose s = ()
   tokValue OTAOpen s = ()
@@ -148,7 +163,6 @@ TokenKind ObsTokenKind where
   tokValue OTTilde s = ()
   tokValue OTEqual s = ()
   tokValue OTColon s = ()
-  tokValue OTPipe s = ()
 
 ObsToken : Type
 ObsToken = Token ObsTokenKind
@@ -166,11 +180,6 @@ Show ObsToken where
   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"
-  show (Tok OTNext s) = "next"
-  show (Tok OTSem s) = "sem"
   show (Tok OTPoint s) = "tt"
   show (Tok OTVoid s) = "Void"
   show (Tok OTAbsurd s) = "absurd"
@@ -179,7 +188,6 @@ Show ObsToken where
   show (Tok OTCast s) = "cast"
   show (Tok OTCastRefl s) = "castRefl"
   show (Tok OTUnit s) = "()"
-  show (Tok OTTriangle s) = "<|"
   show (Tok OTPOpen s) = "("
   show (Tok OTPClose s) = ")"
   show (Tok OTAOpen s) = "<"
@@ -193,7 +201,6 @@ Show ObsToken where
   show (Tok OTTilde s) = "~"
   show (Tok OTEqual s) = "="
   show (Tok OTColon s) = ":"
-  show (Tok OTPipe s) = "|"
 
 identifier : Lexer
 identifier = alpha <+> many alphaNum
@@ -208,11 +215,6 @@ keywords =
   , ("True", OTTrue)
   , ("False", OTFalse)
   , ("if", OTIf)
-  , ("Container", OTContainer)
-  , ("tag", OTTag)
-  , ("position", OTPosition)
-  , ("next", OTNext)
-  , ("sem", OTSem)
   , ("tt", OTPoint)
   , ("Void", OTVoid)
   , ("absurd", OTAbsurd)
@@ -243,7 +245,6 @@ obsTokenMap = toTokenMap [(newlines, OTNewlines), (spaces, OTSpaces)] ++
   , (exact "~", OTTilde)
   , (exact "=", OTEqual)
   , (exact ":", OTColon)
-  , (exact "|", OTPipe)
   ]
 
 op : Type -> Type -> Nat -> Type
@@ -264,66 +265,77 @@ termForms =
   , (OTUnit, Top)
   ]
 
-headForms : List (ObsTokenKind, (n ** (Vect (S n) (WithBounds Syntax) -> Syntax)))
+headForms : List (ObsTokenKind, (n ** op (WithBounds Syntax) Syntax (S n)))
 headForms =
-  [ (OTFst, (0 ** uncurry 1 First))
-  , (OTSnd, (0 ** uncurry 1 Second))
-  , (OTAbsurd, (0 ** uncurry 1 Absurd))
-  , (OTRefl, (0 ** uncurry 1 Refl))
-  , (OTTransp, (4 ** (uncurry 5 Transp)))
-  , (OTCast, (3 ** uncurry 4 Cast))
-  , (OTCastRefl, (0 ** uncurry 1 CastId))
+  [ (OTFst, (0 ** First))
+  , (OTSnd, (0 ** Second))
+  , (OTAbsurd, (0 ** Absurd))
+  , (OTRefl, (0 ** Refl))
+  , (OTTransp, (4 ** Transp))
+  , (OTCast, (3 ** Cast))
+  , (OTCastRefl, (0 ** CastId))
   ]
 
-headLambdaForms : List (ObsTokenKind, (n ** ((WithBounds String, WithBounds Syntax) -> Vect n (WithBounds Syntax) -> Syntax)))
-headLambdaForms =
-  [ (OTIf, (3 ** (uncurry 3 . uncurry If)))
-  ]
+headLambdaForms : List (ObsTokenKind, (n ** (LambdaForm -> op (WithBounds Syntax) Syntax n)))
+headLambdaForms = [(OTIf, (3 ** If))]
 
-declForms : List (ObsTokenKind, (WithBounds String -> op (WithBounds Syntax) Syntax 2))
-declForms = [(OTThinArrow, Pi), (OTProduct, Sigma)]
+declForms : List (ObsTokenKind, (n ** op DeclForm (WithBounds Syntax -> Syntax) (S n)))
+declForms =
+  [ (OTThinArrow, (0 ** Pi))
+  , (OTProduct, (0 ** Sigma))
+  ]
 
 count : (n : _) -> Grammar state tok True a -> Grammar state tok (isSucc n) (Vect n a)
 count 0     p = pure []
 count (S n) p = [| p :: count n p |]
 
+match' : (tok : ObsTokenKind) -> Grammar state ObsToken True (TokType tok)
+match' tok = do
+  pos <- position
+  token <- peek
+  let True = token.kind == tok
+    | False => failLoc pos "expected \{show tok}"
+  match tok
+
 ident : Grammar state ObsToken True (WithBounds String)
-ident = bounds $ match OTIdent
+ident = bounds $ match' OTIdent
 
 whitespace : Grammar state ObsToken True ()
-whitespace = map (\_ => ()) $ some (optional (match OTNewlines) *> match OTSpaces)
+whitespace = map (\_ => ()) $ some (optional (match' OTNewlines) *> match' OTSpaces)
 
 parens : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True a
-parens p = match OTPOpen *> optional whitespace *> p <* optional whitespace <* match OTPClose
+parens p = match' OTPOpen *> optional whitespace *> p <* optional whitespace <* match' OTPClose
 
 var : Grammar state ObsToken True (WithBounds Syntax)
 var = map (map Var) ident
 
 noArgUniverse : Grammar state ObsToken True (WithBounds Universe)
 noArgUniverse = bounds $
-  map (const Prop) (match OTProp <* commit) <|>
-  map (const (Set 0)) (match OTSet <* commit)
+  map (const Prop) (match' OTProp <* commit) <|>
+  map (const (Set 0)) (match' OTSet <* commit)
 
 universe : Grammar state ObsToken True (WithBounds Universe)
 universe = bounds $
-  map (const Prop) (match OTProp <* commit) <|>
-  map Set (match OTSet *> commit *> option 0 (match OTNat <* commit))
+  map (const Prop) (match' OTProp <* commit) <|>
+  map Set (match' OTSet *> commit *> option 0 (match' OTNat <* commit))
 
-decl : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (WithBounds String, a)
-decl p = [| MkPair (ident <* whitespace <* match OTColon <* whitespace) p |]
+decl : Lazy (Grammar state ObsToken True (WithBounds Syntax)) ->
+  Grammar state ObsToken True DeclForm
+decl p = [| MkDecl (ident <* whitespace <* match' OTColon <* whitespace) p |]
 
 pair : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (a, a)
 pair p =
-  match OTAOpen *> commit *>
+  match' OTAOpen *> commit *>
   [| MkPair
-      (optional whitespace *> p <* optional whitespace <* match OTComma <* commit)
+      (optional whitespace *> p <* optional whitespace <* match' OTComma <* commit)
       (optional whitespace *> p <* optional whitespace) |]
-  <* match OTAClose <* commit
+  <* match' OTAClose <* commit
 
-lambda : Lazy (Grammar state ObsToken True a) -> Grammar state ObsToken True (WithBounds String, a)
+lambda : Lazy (Grammar state ObsToken True (WithBounds Syntax)) ->
+  Grammar state ObsToken True LambdaForm
 lambda p =
-  match OTBackslash *> commit *>
-  [| MkPair (ident <* whitespace <* match OTFatArrow <* whitespace) p |]
+  match' OTBackslash *> commit *>
+  [| MkLambda (ident <* whitespace <* match' OTFatArrow <* whitespace) p |]
 
 partial
 noUniversesTerm : Grammar state ObsToken True (WithBounds Syntax)
@@ -334,8 +346,6 @@ head : Grammar state ObsToken True (WithBounds Syntax)
 partial
 spine : Grammar state ObsToken True (WithBounds Syntax)
 partial
-container : Grammar state ObsToken True (WithBounds Syntax)
-partial
 equals : Grammar state ObsToken True (WithBounds Syntax)
 partial
 exp : Grammar state ObsToken True (WithBounds Syntax)
@@ -344,7 +354,7 @@ noUniversesTerm =
   parens exp <|>
   var <|>
   bounds (map (uncurry Pair) (pair exp)) <|>
-  bounds (choiceMap (\(k, s) => map (const s) (match k)) termForms)
+  bounds (choiceMap (\(k, s) => map (const s) (match' k)) termForms)
 
 term = noUniversesTerm <|> map (map Universe) noArgUniverse
 
@@ -353,54 +363,52 @@ head =
   map (map Universe) universe <|>
   bounds
     (choiceMap
-      (\(hd, (n ** f)) => match hd *> commit *>
-        [| f (whitespace *> parens (lambda exp)) (count n (whitespace *> term))|])
+      (\(hd, (n ** f)) =>
+        match' hd *> commit *> whitespace *>
+        pure (uncurry n . f) <*> parens (lambda exp) <*> count n (whitespace *> term))
       headLambdaForms) <|>
   bounds
     (choiceMap
-      (\(hd, (n ** f)) => match hd *> commit *> [| f (count (S n) (whitespace *> term)) |])
+      (\(hd, (n ** f)) => match' hd *> commit *>
+        pure (uncurry (S n) 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 = 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)) |]
+  [| MkPair spine (optional (whitespace *> match' OTTilde *> commit *> whitespace *> spine)) |]
 
 exp =
   equals <|>
-  bounds (map (uncurry Lambda) $ lambda exp) <|>
+  bounds (map Lambda $ lambda exp) <|>
   bounds
-    (map (\((var, a), (b, f)) => f var a b) $
-     [| MkPair
-          (parens (decl exp) <* whitespace)
-          (choiceMap
-            (\(op, f) => match op *> commit *> whitespace *> [| MkPair exp (pure f) |])
-            declForms)
-     |])
+    (choiceMap
+      (\(sep, (n ** f)) =>
+        pure (uncurry (S n) f) <*>
+        count (S n) (parens (decl exp) <* whitespace <* match' sep <* commit <* whitespace) <*>
+        exp)
+      declForms)
 
 partial
 def : Grammar state ObsToken True (WithBounds String, WithBounds Syntax)
-def = [| MkPair (ident <* whitespace <* match OTEqual <* whitespace) exp |]
+def = [| MkPair (ident <* whitespace <* match' OTEqual <* whitespace) exp |]
 
 partial
 fullDef : Grammar state ObsToken True Definition
 fullDef =
   seq
-    [| MkPair (decl exp <* commit) (optional whitespace *> match OTNewlines *> def <* commit) |]
-    (\((name, ty), (name', tm)) =>
+    [| MkPair (decl exp <* commit) (optional whitespace *> match' OTNewlines *> def <* commit) |]
+    (\((MkDecl name ty), (name', tm)) =>
       if name.val == name'.val
         then pure (MkDefinition {name = name, ty, tm})
-        else fatalLoc name.bounds "name mismatch for declaration and definition")
+        else fatalLoc name.bounds "name mismatch' for declaration and definition")
 
 partial
 file : Grammar state ObsToken False (List Definition)
 file =
-  optional (whitespace *> match OTNewlines) *>
-  sepEndBy (optional whitespace *> match OTNewlines) (fullDef <* commit)
-  -- <* eof
+  optional (whitespace *> match' OTNewlines) *>
+  sepEndBy (optional whitespace *> match' OTNewlines) (fullDef <* commit)
 
 whitespaceIrrelevant : WithBounds ObsToken -> WithBounds ObsToken
 whitespaceIrrelevant a = case (a.val.kind) of
@@ -413,7 +421,6 @@ mergeToks : List (WithBounds ObsToken) -> List (WithBounds ObsToken)
 mergeToks (a :: tail@(b :: rest)) = case (a.val.kind, b.val.kind) of
   (OTSpaces, OTNat) => mergeBounds a b :: mergeToks rest
   (OTPOpen, OTPClose) => map (\_ => (Tok OTUnit "()")) (mergeBounds a b) :: mergeToks rest
-  (OTAOpen, OTPipe) => map (\_ => (Tok OTTriangle "<|")) (mergeBounds a b) :: mergeToks rest
   _ => a :: mergeToks tail
 mergeToks toks = toks
 
@@ -425,7 +432,7 @@ castErr (Right x) = pure x
 castErr (Left errs) = do
   for_ {b = ()} errs
     (\(Error msg bounds) =>
-      inBounds $ map error $ maybe (irrelevantBounds msg) (MkBounded msg True) bounds)
+      inBounds $ map error $ maybe (irrelevantBounds msg) (MkBounded msg False) bounds)
   abort
 
 partial
diff --git a/src/Obs/Pretty.idr b/src/Obs/Pretty.idr
index 52a358c..bd163ee 100644
--- a/src/Obs/Pretty.idr
+++ b/src/Obs/Pretty.idr
@@ -4,19 +4,22 @@ import public Text.PrettyPrint.Prettyprinter
 
 -- ty is rendered Open
 export
-prettyDecl : (name : String) -> (ty : Doc ann) -> Doc ann
-prettyDecl name ty = parens $ group (pretty name <++> colon <+> line <+> align ty)
+prettyDecl : (name : Maybe String) -> (ty : Doc ann) -> Doc ann
+prettyDecl Nothing ty = parens $ group $ align ty
+prettyDecl (Just name) ty = parens $ group (pretty name <++> colon <+> line <+> align ty)
 
--- ty and tail are rendered Open
+-- names are rendered Open
 export
 prettyDeclForm : (prec : Prec) ->
-  (name : String) ->
-  (ty : Doc ann) ->
+  (decls : List (Doc ann)) ->
   (sep : String) ->
   (tail : Doc ann) ->
   Doc ann
-prettyDeclForm d name ty sep tail =
-  parenthesise (d > Open) $ group $ vsep $ [prettyDecl name ty <++> pretty sep, align tail]
+prettyDeclForm d decls sep tail =
+  parenthesise (d > Open) $
+  group $
+  concatWith (\x, y => x <++> pretty sep <+> line <+> y) $
+  decls ++ [align tail]
 
 -- body is rendered Open
 export
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index a141d28..74e15c2 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -10,17 +10,31 @@ import Text.Bounded
 
 -- Definition ------------------------------------------------------------------
 
+data Syntax : Type
+
+public export
+record DeclForm where
+  constructor MkDecl
+  var : WithBounds String
+  type : WithBounds Syntax
+
+public export
+record LambdaForm where
+  constructor MkLambda
+  var : WithBounds String
+  body : WithBounds Syntax
+
 public export
 data Syntax : Type where
   Var : (var : String) -> Syntax
   -- Universes
   Universe : (s : Universe) -> Syntax
   -- Dependent Products
-  Pi : (var : WithBounds String) -> (domain, codomain : WithBounds Syntax) -> Syntax
-  Lambda : (var : WithBounds String) -> (body : WithBounds Syntax) -> Syntax
+  Pi : (domain : DeclForm) -> (codomain : WithBounds Syntax) -> Syntax
+  Lambda : (body : LambdaForm) -> Syntax
   App : (fun, arg : WithBounds Syntax) -> Syntax
   -- Dependent Sums
-  Sigma : (var : WithBounds String) -> (index, element : WithBounds Syntax) -> Syntax
+  Sigma : (index : DeclForm) -> (element : WithBounds Syntax) -> Syntax
   Pair : (first, second : WithBounds Syntax) -> Syntax
   First : (arg : WithBounds Syntax) -> Syntax
   Second : (arg : WithBounds Syntax) -> Syntax
@@ -28,9 +42,7 @@ data Syntax : Type where
   Bool : Syntax
   True : Syntax
   False : Syntax
-  If : (var : WithBounds String) ->
-    (returnType, discriminant, true, false : WithBounds Syntax) ->
-    Syntax
+  If : (returnType : LambdaForm) -> (discriminant, true, false : WithBounds Syntax) -> Syntax
   -- True
   Top : Syntax
   Point : Syntax
@@ -55,15 +67,21 @@ record Definition where
 
 prettyPrecBounds : Prec -> WithBounds Syntax -> Doc ann
 
+prettyPrecDecl : DeclForm -> Doc ann
+prettyPrecDecl (MkDecl var type) = prettyDecl (Just var.val) (prettyPrecBounds Open type)
+
+prettyPrecLambda : Prec -> LambdaForm -> Doc ann
+prettyPrecLambda d (MkLambda var body) = prettyLambda d var.val (prettyPrecBounds Open body)
+
 prettyPrec : Prec -> Syntax -> Doc ann
 prettyPrec d (Var {var}) = pretty var
 prettyPrec d (Universe {s}) = prettyPrec d s
-prettyPrec d (Pi {var, domain, codomain}) =
-  prettyDeclForm d var.val (prettyPrecBounds Open domain) "->" (prettyPrecBounds Open codomain)
-prettyPrec d (Lambda {var, body}) = prettyLambda d var.val (prettyPrecBounds Open body)
+prettyPrec d (Pi {domain, codomain}) =
+  prettyDeclForm d [prettyPrecDecl domain] "->" (prettyPrecBounds Open codomain)
+prettyPrec d (Lambda {body}) = prettyPrecLambda d body
 prettyPrec d (App {fun, arg}) = prettyApp d (prettyPrecBounds Open fun) [prettyPrecBounds App arg]
-prettyPrec d (Sigma {var, index, element}) =
-  prettyDeclForm d var.val (prettyPrecBounds Open index) "**" (prettyPrecBounds Open element)
+prettyPrec d (Sigma {index, element}) =
+  prettyDeclForm d [prettyPrecDecl index] "**" (prettyPrecBounds Open element)
 prettyPrec d (Pair {first, second}) =
   prettyPair (prettyPrecBounds Open first) (prettyPrecBounds Open second)
 prettyPrec d (First {arg}) = prettyApp d (pretty "fst") [prettyPrecBounds App arg]
@@ -71,9 +89,9 @@ prettyPrec d (Second {arg}) = prettyApp d (pretty "snd") [prettyPrecBounds App a
 prettyPrec d Bool = pretty "Bool"
 prettyPrec d True = pretty "True"
 prettyPrec d False = pretty "False"
-prettyPrec d (If {var, returnType, discriminant, true, false}) =
+prettyPrec d (If {returnType, discriminant, true, false}) =
   prettyApp d (pretty "if") $
-  [ prettyLambda App var.val (prettyPrecBounds Open returnType)
+  [ prettyPrecLambda App returnType
   , prettyPrecBounds App discriminant
   , prettyPrecBounds App true
   , prettyPrecBounds App false
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 95ed08b..8dad72c 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -12,21 +12,33 @@ import Text.Bounded
 
 -- Definition ------------------------------------------------------------------
 
+data Term : Nat -> Type
+
+public export
+record DeclForm (n : Nat) where
+  constructor MkDecl
+  var : WithBounds String
+  type : WithBounds (Term n)
+
+public export
+record LambdaForm (n : Nat) where
+  constructor MkLambda
+  var : WithBounds String
+  body : WithBounds (Term (S n))
+
 public export
 data Term : Nat -> Type where
   Var : (var : String) -> (i : Fin n) -> Term n
   -- Universes
   Universe : (s : Universe) -> Term n
   -- Dependent Product
-  Pi : (var : WithBounds String) ->
-    (domain : WithBounds (Term n)) ->
+  Pi : (domain : DeclForm n) ->
     (codomain : WithBounds (Term (S n))) ->
     Term n
-  Lambda : (var : WithBounds String) -> (body : WithBounds (Term (S n))) -> Term n
+  Lambda : (body : LambdaForm n) -> Term n
   App : (fun, arg : WithBounds (Term n)) -> Term n
   -- Dependent Sums
-  Sigma : (var : WithBounds String) ->
-    (index : WithBounds (Term n)) ->
+  Sigma : (index : DeclForm n) ->
     (element : WithBounds (Term (S n))) ->
     Term n
   Pair : (first, second : WithBounds (Term n)) -> Term n
@@ -36,8 +48,7 @@ data Term : Nat -> Type where
   Bool : Term n
   True : Term n
   False : Term n
-  If : (var : WithBounds String) ->
-    (returnType : WithBounds (Term (S n))) ->
+  If : (returnType : LambdaForm n) ->
     (discriminant, true, false : WithBounds (Term n)) ->
     Term n
   -- True
@@ -69,15 +80,21 @@ data Block : Nat -> Type where
 
 prettyPrecBounds : Prec -> WithBounds (Term n) -> Doc ann
 
+prettyPrecDecl : DeclForm n -> Doc ann
+prettyPrecDecl (MkDecl var type) = prettyDecl (Just var.val) (prettyPrecBounds Open type)
+
+prettyPrecLambda : Prec -> LambdaForm n -> Doc ann
+prettyPrecLambda d (MkLambda var body) = prettyLambda d var.val (prettyPrecBounds Open body)
+
 prettyPrec : Prec -> Term n -> Doc ann
 prettyPrec d (Var {var, i}) = pretty var
 prettyPrec d (Universe {s}) = prettyPrec d s
-prettyPrec d (Pi {var, domain, codomain}) =
-  prettyDeclForm d var.val (prettyPrecBounds Open domain) "->" (prettyPrecBounds Open codomain)
-prettyPrec d (Lambda {var, body}) = prettyLambda d var.val (prettyPrecBounds Open body)
+prettyPrec d (Pi {domain, codomain}) =
+  prettyDeclForm d [prettyPrecDecl domain] "->" (prettyPrecBounds Open codomain)
+prettyPrec d (Lambda {body}) = prettyPrecLambda d body
 prettyPrec d (App {fun, arg}) = prettyApp d (prettyPrecBounds Open fun) [prettyPrecBounds App arg]
-prettyPrec d (Sigma {var, index, element}) =
-  prettyDeclForm d var.val (prettyPrecBounds Open index) "**" (prettyPrecBounds Open element)
+prettyPrec d (Sigma {index, element}) =
+  prettyDeclForm d [prettyPrecDecl index] "**" (prettyPrecBounds Open element)
 prettyPrec d (Pair {first, second}) =
   prettyPair (prettyPrecBounds Open first) (prettyPrecBounds Open second)
 prettyPrec d (First {arg}) = prettyApp d (pretty "fst") [prettyPrecBounds App arg]
@@ -85,9 +102,9 @@ prettyPrec d (Second {arg}) = prettyApp d (pretty "snd") [prettyPrecBounds App a
 prettyPrec d Bool = pretty "Bool"
 prettyPrec d True = pretty "True"
 prettyPrec d False = pretty "False"
-prettyPrec d (If {var, returnType, discriminant, true, false}) =
+prettyPrec d (If {returnType, discriminant, true, false}) =
   prettyApp d (pretty "if") $
-  [ prettyLambda App var.val (prettyPrecBounds Open returnType)
+  [ prettyPrecLambda App returnType
   , prettyPrecBounds App discriminant
   , prettyPrecBounds App true
   , prettyPrecBounds App false
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index b3762cf..c3dcfbf 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -1,6 +1,6 @@
 module Obs.Typing
 
-import Control.Monad.Maybe
+import Control.Monad.Identity
 
 import Data.Nat
 
@@ -38,90 +38,99 @@ universeMismatch lhs rhs = inScope "universe mismatch" $ mismatch lhs rhs
 
 -- Utilities -------------------------------------------------------------------
 
-MkPair : (s, s' : Universe)
-  -> NormalForm (relevance s) ctx
-  -> NormalForm (relevance s') ctx
-  -> NormalForm (relevance (max s s')) ctx
-MkPair Prop Prop t u = u
-MkPair Prop s'@(Set _) t u = Cnstr $ Pair Prop s' Set t u
-MkPair s@(Set _) s' t u = Cnstr $ Pair s s' Set t u
+MkPair : (indexRel, elementRel : Relevance)
+  -> (first : NormalForm indexRel ctx)
+  -> (second : NormalForm elementRel ctx)
+  -> NormalForm (pair indexRel elementRel) ctx
+MkPair Irrelevant Irrelevant first second = Irrel
+MkPair Irrelevant Relevant first second =
+  Cnstr $ Pair {indexRel = Irrelevant, elementRel = Relevant, prf = Relevant, first, second}
+MkPair Relevant elementRel first second =
+  Cnstr $ Pair {indexRel = Relevant, elementRel, prf = Relevant, first, second}
 
 -- Checking and Inference ------------------------------------------------------
 
 check' : (tyCtx : TyContext ctx)
-  -> (s : Universe)
-  -> TypeNormalForm ctx
-  -> Term (length ctx)
-  -> Logging ann (NormalForm (relevance s) ctx)
+  -> (sort : Universe)
+  -> (type : TypeNormalForm ctx)
+  -> (term : Term (length ctx))
+  -> Logging ann (NormalForm (relevance sort) ctx)
 
 infer' : (tyCtx : TyContext ctx)
-  -> Term (length ctx)
-  -> Logging ann (s ** (TypeNormalForm ctx, NormalForm (relevance s) ctx))
+  -> (term : Term (length ctx))
+  -> Logging ann (sort : Universe ** (TypeNormalForm ctx, NormalForm (relevance sort) ctx))
 
-inferType' : {default typeMismatch tag : forall a . Doc ann -> Doc ann -> Logging ann a}
+inferType' : {default typeMismatch tag : forall a . (expected, actual : Doc ann) -> Logging ann a}
   -> (tyCtx : TyContext ctx)
-  -> Term (length ctx)
+  -> (term : Term (length ctx))
   -> Logging ann (Universe, TypeNormalForm ctx)
-inferType' ctx t = do
-  (Set _ ** (Cnstr (Universe s), a)) <- infer' ctx t
-    | (_ ** (type, a)) => tag (pretty "sort") (pretty type)
-  pure (s, a)
+inferType' ctx term = do
+  (Set _ ** (Cnstr (Universe sort), type)) <- infer' ctx term
+    | (_ ** (type, term)) => tag (pretty "sort") (pretty type)
+  pure (sort, type)
 
 check : (tyCtx : TyContext ctx)
-  -> (s : Universe)
-  -> TypeNormalForm ctx
-  -> WithBounds (Term (length ctx))
-  -> Logging ann (NormalForm (relevance s) ctx)
-check ctx s a (MkBounded t irrel bounds) = inBounds (MkBounded (check' ctx s a t) irrel bounds)
+  -> (sort : Universe)
+  -> (type : TypeNormalForm ctx)
+  -> (term : WithBounds (Term (length ctx)))
+  -> Logging ann (NormalForm (relevance sort) ctx)
+check ctx sort type (MkBounded term irrel bounds) =
+  inBounds (MkBounded (check' ctx sort type term) irrel bounds)
 
 checkType : (tyCtx : TyContext ctx)
-  -> (s : Universe)
-  -> WithBounds (Term (length ctx))
+  -> (sort : Universe)
+  -> (term : WithBounds (Term (length ctx)))
   -> Logging ann (TypeNormalForm ctx)
-checkType ctx s tm = check ctx (succ s) (cast s) tm
+checkType ctx sort term = check ctx (succ sort) (cast sort) term
 
 infer : (tyCtx : TyContext ctx)
-  -> WithBounds (Term (length ctx))
-  -> Logging ann (s ** (TypeNormalForm ctx, NormalForm (relevance s) ctx))
-infer ctx (MkBounded t irrel bounds) = inBounds (MkBounded (infer' ctx t) irrel bounds)
+  -> (term : WithBounds (Term (length ctx)))
+  -> Logging ann (sort : Universe ** (TypeNormalForm ctx, NormalForm (relevance sort) ctx))
+infer ctx (MkBounded term irrel bounds) = inBounds (MkBounded (infer' ctx term) irrel bounds)
 
 inferType : {default typeMismatch tag : forall a . Doc ann -> Doc ann -> Logging ann a}
   -> (tyCtx : TyContext ctx)
-  -> WithBounds (Term (length ctx))
+  -> (term : WithBounds (Term (length ctx)))
   -> Logging ann (Universe, TypeNormalForm ctx)
-inferType ctx (MkBounded t irrel bounds) = inBounds (MkBounded (inferType' ctx t) irrel bounds)
+inferType ctx (MkBounded term irrel bounds) =
+  inBounds (MkBounded (inferType' ctx term) irrel bounds)
 
-check' ctx sort (Cnstr (Pi domainSort codomainSort _ domain codomain)) (Lambda {var, body}) = do
+check' ctx sort
+  (Cnstr (Pi {domainSort, codomainSort, domain, codomain}))
+  (Lambda {body = MkLambda var body}) = do
   info "encountered lambda"
 
   let Yes Refl = decEq sort (domainSort ~> codomainSort)
     | No _ => fatal "internal universe mismatch"
 
-  let bodyCtx = ctx ::< MkFreeVar domainSort domain var.val
+  let bodyCtx = ctx ::< MkFreeVar domainSort domain.type var.val
 
   trace $ pretty {ann} "checking body has type" <++> pretty codomainSort
   body <- check bodyCtx codomainSort codomain body
 
   pure $ case codomainSort of
     Prop => Irrel
-    Set _ => Cnstr (Lambda domainSort var.val body)
+    Set _ => Cnstr (Lambda {domainRel = _, var = Just var.val, body})
 
-check' ctx sort type (Lambda {var, body}) = typeMismatch (pretty "function") (pretty type)
+check' ctx sort type (Lambda {body}) = typeMismatch (pretty "function") (pretty type)
 
-check' ctx sort (Cnstr (Sigma indexSort elementSort var index element)) (Pair {first, second}) = do
+check' ctx sort
+  (Cnstr (Sigma {indexSort, elementSort, index, element}))
+  (Pair {first, second}) = do
   info "encountered pair"
 
   let Yes Refl = decEq sort (max indexSort elementSort)
     | No _ => fatal "internal universe mismatch"
+  rewrite pairRelevance indexSort elementSort
 
-  trace $ pretty {ann} "checking first has type" <++> pretty index
-  first <- check ctx indexSort index first
+  trace $ pretty {ann} "checking first has type" <++> pretty index.type
+  first <- check ctx indexSort index.type first
 
   element <- subst1 first element
   trace $ pretty {ann} "checking second has type" <++> pretty element
   second <- check ctx elementSort element second
 
-  pure $ MkPair indexSort elementSort first second
+  pure $ MkPair {indexRel = _, elementRel = _, first, second}
 
 check' ctx sort type (Pair {first, second}) = typeMismatch (pretty "pair type") (pretty type)
 
@@ -145,8 +154,8 @@ check' ctx sort type t = do
   expandedType <- subst type (reduce ctx)
   expandedInferredType <- subst inferredType (reduce ctx)
 
-  Just _ <- inScope "convert" $ runMaybeT $ convert (succ sort) (cast sort) expandedType expandedInferredType
-  | Nothing => inScope "conversion failed" $ mismatch (pretty type) (pretty inferredType)
+  let True = runIdentity $ convert Relevant (cast sort) expandedType expandedInferredType
+    | False => inScope "conversion failed" $ mismatch (pretty type) (pretty inferredType)
 
   pure value
 
@@ -162,7 +171,7 @@ infer' ctx (Universe {s}) = do
 
     pure (succ (succ s) ** (cast (succ s), cast s))
 
-infer' ctx (Pi {var, domain, codomain}) = do
+infer' ctx (Pi {domain = MkDecl var domain, codomain}) = do
     info "encountered pi"
 
     (domainSort, domain) <- inferType ctx domain
@@ -175,10 +184,15 @@ infer' ctx (Pi {var, domain, codomain}) = do
     trace $ pretty {ann} "codomain type is" <++> pretty codomain
 
     let piSort = domainVar.sort ~> codomainSort
-    let term = Cnstr (Pi domainVar.sort codomainSort var.val domain codomain)
+    let term = Cnstr $ Pi
+          { domainSort = domainVar.sort
+          , codomainSort
+          , domain = MkDecl (Just var.val) domain
+          , codomain
+          }
     pure (succ piSort ** (cast piSort, term))
 
-infer' ctx (Lambda {var, body}) = fatal "cannot infer type of lambda"
+infer' ctx (Lambda {body}) = fatal "cannot infer type of lambda"
 
 infer' ctx (App {fun, arg}) = do
     info "encountered application"
@@ -186,7 +200,7 @@ infer' ctx (App {fun, arg}) = do
     (piSort ** (funType, funValue)) <- infer ctx fun
     trace $ pretty {ann} "function has type" <++> pretty funType
 
-    let Cnstr (Pi domainSort codomainSort _ domain codomain) = funType
+    let Cnstr (Pi {domainSort, codomainSort, domain, codomain}) = funType
       | _ => inBounds $ map (const $ typeMismatch (pretty "function") (pretty funType)) fun
 
     let Yes Refl = decEq piSort (domainSort ~> codomainSort)
@@ -194,8 +208,8 @@ infer' ctx (App {fun, arg}) = do
 
     let fun = funValue
 
-    trace $ pretty {ann} "checking argument has type" <++> pretty domain
-    arg <- check ctx domainSort domain arg
+    trace $ pretty {ann} "checking argument has type" <++> pretty domain.type
+    arg <- check ctx domainSort domain.type arg
     trace $ pretty {ann} "argument is well typed"
 
     returnType <- subst1 arg codomain
@@ -205,7 +219,7 @@ infer' ctx (App {fun, arg}) = do
 
     pure (codomainSort ** (returnType, returnValue))
 
-infer' ctx (Sigma {var, index, element}) = do
+infer' ctx (Sigma {index = MkDecl var index, element}) = do
     info "encountered sigma"
 
     (indexSort, index) <- inferType ctx index
@@ -218,7 +232,12 @@ infer' ctx (Sigma {var, index, element}) = do
     trace $ pretty {ann} "element type is" <++> pretty element
 
     let sigmaSort = max indexVar.sort elementSort
-    let term = Cnstr (Sigma indexVar.sort elementSort var.val index element)
+    let term = Cnstr $ Sigma
+          { indexSort = indexVar.sort
+          , elementSort
+          , index = MkDecl (Just var.val) index
+          , element
+          }
     pure (succ sigmaSort ** (cast sigmaSort, term))
 
 infer' ctx (Pair {first, second}) = fatal "cannot infer type of pair"
@@ -229,7 +248,7 @@ infer' ctx (First {arg}) = do
     (sigmaSort ** (argType, argValue)) <- infer ctx arg
     trace $ pretty {ann} "pair has type" <++> pretty argType
 
-    let Cnstr (Sigma indexSort elementSort _ index element) = argType
+    let Cnstr (Sigma {indexSort, elementSort, index, element}) = argType
       | _ => inBounds $ map (const $ typeMismatch (pretty "pair type") (pretty argType)) arg
 
     let Yes Refl = decEq sigmaSort (max indexSort elementSort)
@@ -237,7 +256,7 @@ infer' ctx (First {arg}) = do
 
     let argValue = rewrite sym $ pairRelevance indexSort elementSort in argValue
 
-    let returnType = index
+    let returnType = index.type
     returnValue <- doFst (relevance indexSort) (relevance elementSort) argValue
 
     pure (indexSort ** (returnType, returnValue))
@@ -248,7 +267,7 @@ infer' ctx (Second {arg}) = do
     (sigmaSort ** (argType, argValue)) <- infer ctx arg
     trace $ pretty {ann} "pair has type" <++> pretty argType
 
-    let Cnstr (Sigma indexSort elementSort _ index element) = argType
+    let Cnstr (Sigma {indexSort, elementSort, index, element}) = argType
       | _ => inBounds $ map (const $ typeMismatch (pretty "pair type") (pretty argType)) arg
 
     let Yes Refl = decEq sigmaSort (max indexSort elementSort)
@@ -274,7 +293,7 @@ infer' ctx False = do
     info "encountered false"
     pure (Set 0 ** (Cnstr Bool, Cnstr False))
 
-infer' ctx (If {var, returnType, discriminant, true, false}) = do
+infer' ctx (If {returnType = MkLambda var returnType, discriminant, true, false}) = do
     info "encountered if"
     trace "checking discriminant is bool"
 
@@ -348,7 +367,12 @@ infer' ctx (Transp {indexedType, oldIndex, value, newIndex, equality}) = do
     newIndex <- check ctx indexSort indexType newIndex
     trace "new index is well typed"
 
-    let indexedTypeShape = Cnstr $ Pi indexSort (Set 0) "" indexType (Cnstr (Universe Prop))
+    let indexedTypeShape = Cnstr $ Pi
+          { domainSort = indexSort
+          , codomainSort = Set 0
+          , domain = MkDecl Nothing indexType
+          , codomain = Cnstr (Universe Prop)
+          }
     indexedType <- check ctx (indexSort ~> Set 0) indexedTypeShape indexedType
     trace $ pretty {ann} "result is an index of type" <++> pretty indexedType
 
diff --git a/src/Obs/Typing/Context.idr b/src/Obs/Typing/Context.idr
index 4706dca..ad1d0a7 100644
--- a/src/Obs/Typing/Context.idr
+++ b/src/Obs/Typing/Context.idr
@@ -64,7 +64,7 @@ fromVar var = MkDefinition
   { name = var.name
   , sort = var.sort
   , ty = weaken [relevance var.sort] var.ty
-  , tm = point (var.name, (var.sort ** Refl)) Here
+  , tm = point (Just var.name) Here
   , correct = Refl
   }
 
@@ -104,5 +104,5 @@ 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)
+  (pure $ point (Just var.name) Here)
   (\i => pure $ weaken [_] $ !(reduce ctx i))
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr
index 766c21e..93812c1 100644
--- a/src/Obs/Typing/Conversion.idr
+++ b/src/Obs/Typing/Conversion.idr
@@ -1,7 +1,6 @@
 module Obs.Typing.Conversion
 
-import Control.Monad.Maybe
-import Control.Monad.Trans
+import Control.Monad.Identity
 
 import Data.Bool
 import Data.Nat
@@ -18,190 +17,193 @@ import Obs.Universe
 
 -- Conversion ------------------------------------------------------------------
 
+convertUntyped : (rel : Relevance) -> (left, right : NormalForm rel ctx) -> Identity Bool
+
 export
-convert : (s : Universe)
-  -> (a : TypeNormalForm ctx)
-  -> (t, u : NormalForm (relevance s) ctx)
-  -> MaybeT (Logging ann) (NormalForm (relevance s) ctx)
-
-untypedConvert : (t, u : NormalForm Relevant ctx) -> MaybeT (Logging ann) (NormalForm Relevant ctx)
--- Diagonals
-untypedConvert (Cnstr (Universe s)) (Cnstr (Universe s')) =
-  if s == s' then pure (Cnstr (Universe s)) else nothing
-untypedConvert (Cnstr (Pi s s' var a b)) (Cnstr (Pi l l' _ a' b')) = do
-  let Yes Refl = decEq s l
-    | No _ => nothing
-  lift $ trace "going back to type-directed conversion"
-  a <- assert_total (convert (succ s) (cast s) a a')
-  b <- assert_total (convert (succ s') (cast s') b b')
-  pure (Cnstr $ Pi s s' var a b)
-untypedConvert (Cnstr (Lambda s var t)) (Cnstr (Lambda s' _ u)) = do
-  let Yes Refl = decEq s s'
-    | 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 (succ s) (cast s) a a')
-  b <- assert_total (convert (succ s') (cast s') b b')
-  pure (Cnstr $ Sigma s s' var a b)
-untypedConvert (Cnstr (Pair s@(Set _) s'@(Set _) prf t u)) (Cnstr (Pair l l' prf' t' u')) = do
-  let Yes Refl = decEq (s, s') (l, l')
-    | No _ => nothing
-  lift $ trace "converting pair pointwise"
-  t <- untypedConvert t t'
-  u <- untypedConvert u u'
-  pure (Cnstr $ Pair l l' Set t u)
-untypedConvert (Cnstr (Pair s@(Set _) Prop prf t u)) (Cnstr (Pair l Prop prf' t' u')) = do
-  let Yes Refl = decEq s l
-    | No _ => nothing
-  lift $ trace "converting pair pointwise"
-  t <- untypedConvert t t'
-  pure (Cnstr $ Pair l Prop Set t Irrel)
-untypedConvert (Cnstr (Pair Prop s'@(Set _) prf t u)) (Cnstr (Pair Prop l' prf' t' u')) = do
-  let Yes Refl = decEq s' l'
-    | No _ => nothing
-  lift $ trace "converting pair pointwise"
-  u <- untypedConvert u u'
-  pure (Cnstr $ Pair Prop l' Set Irrel u)
-untypedConvert (Cnstr Bool) (Cnstr Bool) = pure (Cnstr Bool)
-untypedConvert (Cnstr True) (Cnstr True) = pure (Cnstr True)
-untypedConvert (Cnstr False) (Cnstr False) = pure (Cnstr False)
-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 r t u)) rhs@(Ntrl (App r' t' u')) = do
-  let Yes Refl = decEq r r'
-    | No _ => nothing
-  lift $ trace "checking parts of a spine"
-  t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
-  let Relevant = r'
-    | Irrelevant => lift $ doApp t Irrel
-  u <- untypedConvert u u'
-  lift $ doApp t u
-untypedConvert lhs@(Ntrl (Fst r t)) rhs@(Ntrl (Fst r' t')) = do
-  lift $ trace "checking full pair for fst"
-  t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
-  lift $ doFst Relevant r t
-untypedConvert lhs@(Ntrl (Snd r t)) rhs@(Ntrl (Snd r' t')) = do
-  lift $ trace "checking full pair for snd"
-  t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
-  lift $ doSnd r Relevant (rewrite pairRelevantRight r in t)
-untypedConvert lhs@(Ntrl (If t f g)) rhs@(Ntrl (If t' f' g')) = do
-  lift $ trace "checking all branches of if"
-  t <- untypedConvert (assert_smaller lhs (Ntrl t)) (assert_smaller rhs (Ntrl t'))
-  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 [relevance s] u) (point (var, (s ** Refl)) Here)
-  assert_total (untypedConvert t (Cnstr (Lambda s var u)))
-untypedConvert (Ntrl t) u@(Cnstr (Lambda s var _)) = do
-  t <- lift $ doApp (Ntrl $ weaken [relevance s] t) (point (var, (s ** Refl)) Here)
-  assert_total (untypedConvert (Cnstr (Lambda s var t)) u)
--- Sigma types
-untypedConvert t@(Cnstr (Pair s s' prf _ _)) t'@(Ntrl _) =
-  let t'' : NormalForm (pair (relevance s) (relevance s')) ctx
-      t'' = rewrite trans (sym $ pairRelevance s s') (forgetIsRelevant prf) in t'
-  in do
-  t' <- lift $ doFst (relevance s) (relevance s') t''
-  u' <- lift $ doSnd (relevance s) (relevance s') t''
-  assert_total (untypedConvert t (Cnstr (Pair s s' prf t' u')))
-untypedConvert t@(Ntrl _) t'@(Cnstr (Pair s s' prf _ _)) =
-  let t'' : NormalForm (pair (relevance s) (relevance s')) ctx
-      t'' = rewrite trans (sym $ pairRelevance s s') (forgetIsRelevant prf) in t
-  in do
-  t <- lift $ doFst (relevance s) (relevance s') t''
-  u <- lift $ doSnd (relevance s) (relevance s') t''
-  assert_total (untypedConvert (Cnstr (Pair s s' prf t u)) t')
--- Bools
--- no cases because diagonals complete
--- Fallback
-untypedConvert _ _ = nothing
-
-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 (Universe s)) t u = do
-  lift $ trace $ pretty {ann} "converting in type" <++> pretty s
-  untypedConvert t u
-convert (Set k) (Cnstr (Pi s s'@(Set _) var a b)) t u = do
-  -- s' must be Set, otherwise ty is in Prop
-  lift $ trace "converting pi type"
-  t' <- lift $ doApp (Sorted.weaken [relevance s] t) (point (var, (s ** Refl)) Here)
-  u' <- lift $ doApp (Sorted.weaken [relevance s] u) (point (var, (s ** Refl)) Here)
-  t <- convert s' b t' u'
-  pure (Cnstr $ Lambda s var t)
-convert (Set k) ty@(Cnstr (Sigma s@(Set j) s' var a b)) t u = do
-  lift $ trace "converting sigma type"
-  t1 <- lift $ doFst Relevant (relevance s') t
-  u1 <- lift $ doFst Relevant (relevance s') u
-  t1 <- convert s a t1 u1
-  t2 <- lift $ doSnd Relevant (relevance s') t
-  u2 <- lift $ doSnd Relevant (relevance s') u
-  b <- lift $ subst1 t1 b
-  t2 <- convert s' (assert_smaller ty b) t2 u2
-  pure (Cnstr $ Pair s s' Set t1 t2)
-convert (Set k) ty@(Cnstr (Sigma Prop s'@(Set _) var a b)) t u = do
-  lift $ trace "converting sigma type (snd only)"
-  t2 <- lift $ doSnd Irrelevant Relevant t
-  u2 <- lift $ doSnd Irrelevant Relevant u
-  b <- lift $ subst1 Irrel b
-  t2 <- convert s' (assert_smaller ty b) t2 u2
-  pure (Cnstr $ Pair Prop s' Set 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
+convert : (rel : Relevance)
+  -> (type : TypeNormalForm ctx)
+  -> (left, right : NormalForm rel ctx)
+  -> Identity Bool
+convert rel type left right = convertUntyped rel left right
+
+convertCnstr : (left, right : Constructor ctx) -> Identity Bool
+convertCnstr (Universe {s}) (Universe {s = s'}) = pure (s == s')
+convertCnstr
+  (Pi {domainSort, codomainSort, domain, codomain})
+  (Pi
+    { domainSort = domainSort'
+    , codomainSort = codomainSort'
+    , domain = domain'
+    , codomain = codomain'
+    }) = do
+  let Yes Refl = decEq (domainSort, codomainSort) (domainSort', codomainSort')
+    | No _ => pure False
+
+  convertDomain <- convert
+    { rel = Relevant
+    , type = cast domainSort
+    , left = assert_smaller domain domain.type
+    , right = assert_smaller domain' domain'.type
+    }
+
+  convertCodomain <- convert
+    { rel = Relevant
+    , type = cast codomainSort
+    , left = codomain
+    , right = codomain'
+    }
+
+  pure (convertDomain && convertCodomain)
+convertCnstr
+  (Lambda {domainRel, var = _, body})
+  (Lambda {domainRel = domainRel', var = _, body = body'}) = do
+  let Yes Refl = decEq domainRel domainRel'
+    | No _ => pure False
+
+  convertUntyped {rel = Relevant, left = body, right = body'}
+convertCnstr
+  (Sigma {indexSort, elementSort, index, element})
+  (Sigma
+    { indexSort = indexSort'
+    , elementSort = elementSort'
+    , index = index'
+    , element = element'
+    }) = do
+  let Yes Refl = decEq (indexSort, elementSort) (indexSort', elementSort')
+    | No _ => pure False
+
+  convertIndex <- convert
+    { rel = Relevant
+    , type = cast indexSort
+    , left = assert_smaller index index.type
+    , right = assert_smaller index' index'.type
+    }
+
+  convertElement <- convert
+    { rel = Relevant
+    , type = cast elementSort
+    , left = element
+    , right = element'
+    }
+
+  pure (convertIndex && convertElement)
+convertCnstr
+  left@(Pair {indexRel, elementRel, prf = _, first, second})
+  right@(Pair
+    { indexRel = indexRel'
+    , elementRel = elementRel'
+    , prf = _
+    , first = first'
+    , second = second'
+    }) = do
+  let Yes Refl = decEq (indexRel, elementRel) (indexRel', elementRel')
+    | No _ => pure False
+
+  convertFirst <- convertUntyped {rel = indexRel, left = first, right = first'}
+  convertSecond <- convertUntyped {rel = elementRel, left = second, right = second'}
+  pure (convertFirst && convertSecond)
+convertCnstr Bool Bool = pure True
+convertCnstr True True = pure True
+convertCnstr False False = pure True
+convertCnstr Top Top = pure True
+convertCnstr Bottom Bottom = pure True
+convertCnstr left right = pure False
+
+convertNtrl : (left, right : Neutral ctx) -> Identity Bool
+convertNtrl (Var {var = _, i}) (Var {var = _, i = j}) = pure (elemToNat i == elemToNat j)
+convertNtrl (App {argRel, fun, arg}) (App {argRel = argRel', fun = fun', arg = arg'}) = do
+  let Yes Refl = decEq argRel argRel'
+    | No _ => pure False
+
+  convertFun <- convertNtrl {left = fun, right = fun'}
+  convertArg <- convertUntyped {rel = argRel, left = arg, right = arg'}
+  pure (convertFun && convertArg)
+convertNtrl (First {secondRel = _, arg}) (First {secondRel = _, arg = arg'}) =
+  convertNtrl arg arg'
+convertNtrl (Second {firstRel = _, arg}) (Second {firstRel = _, arg = arg'}) =
+  convertNtrl arg arg'
+convertNtrl
+  (If {discriminant, true, false})
+  (If {discriminant = discriminant', true = true', false = false'}) =
+  do
+  convertDiscriminant <- convertNtrl {left = discriminant, right = discriminant}
+  convertTrue <- convertUntyped {rel = Relevant, left = true, right = true'}
+  convertFalse <- convertUntyped {rel = Relevant, left = false, right = false'}
+  pure (convertDiscriminant && convertTrue && convertFalse)
+convertNtrl Absurd Absurd = pure True
+convertNtrl
+  (Equal {type, left, right})
+  (Equal {type = type', left = left', right = right'}) =
+  do
+  convertType <- convertNtrl {left = type, right = type'}
+  convertLeft <- convertUntyped {rel = Relevant, left = left, right = left'}
+  convertRight <- convertUntyped {rel = Relevant, left = right, right = right'}
+  pure (convertType && convertLeft && convertRight)
+-- We don't need to check, e.g. EqualL and EqualR
+-- Assume (EqualL left right) ~~ (EqualR left' right')
+-- Then (Ntrl left) ~~ (Cnstr left')
+-- This means left' is either Lambda or Pair
+-- Lamda and Pair are not type constructors.
+-- Hence we have a contradiction, so we are done.
+convertNtrl (EqualL {left, right}) (EqualL {left = left', right = right'}) = do
+  convertLeft <- convertNtrl {left = left, right = left'}
+  convertRight <- convertUntyped {rel = Relevant, left = right, right = right'}
+  pure (convertLeft && convertRight)
+convertNtrl (EqualR {left, right}) (EqualR {left = left', right = right'}) = do
+  convertLeft <- convertCnstr {left = left, right = left'}
+  convertRight <- convertNtrl {left = right, right = right'}
+  pure (convertLeft && convertRight)
+convertNtrl (EqualStuck {left, right}) (EqualStuck {left = left', right = right'}) = do
+  convertLeft <- convertCnstr {left = left, right = left'}
+  convertRight <- convertCnstr {left = right, right = right'}
+  pure (convertLeft && convertRight)
+convertNtrl
+  (CastL {oldType, newType, value})
+  (CastL {oldType = oldType', newType = newType', value = value'}) =
+  do
+  convertOldType <- convertNtrl {left = oldType, right = oldType'}
+  convertNewType <- convertUntyped {rel = Relevant, left = newType, right = newType'}
+  convertValue <- convertUntyped {rel = Relevant, left = value, right = value'}
+  pure (convertOldType && convertNewType && convertValue)
+convertNtrl
+  (CastR {oldType, newType, value})
+  (CastR {oldType = oldType', newType = newType', value = value'}) =
+  do
+  convertOldType <- convertCnstr {left = oldType, right = oldType'}
+  convertNewType <- convertNtrl {left = newType, right = newType'}
+  convertValue <- convertUntyped {rel = Relevant, left = value, right = value'}
+  pure (convertOldType && convertNewType && convertValue)
+convertNtrl
+  (CastStuck {oldType, newType, value})
+  (CastStuck {oldType = oldType', newType = newType', value = value'}) =
+  do
+  convertOldType <- convertCnstr {left = oldType, right = oldType'}
+  convertNewType <- convertCnstr {left = newType, right = newType'}
+  convertValue <- convertUntyped {rel = Relevant, left = value, right = value'}
+  pure (convertOldType && convertNewType && convertValue)
+convertNtrl left right = pure False
+
+convertEta : (left : Constructor ctx) -> (right : Neutral ctx) -> Identity Bool
+convertEta (Lambda {domainRel, var, body}) right = do
+  let right = weaken [domainRel] right
+  let rightBody = App {argRel = domainRel, fun = right, arg = point Nothing Here}
+  convertUntyped {rel = Relevant, left = body, right = Ntrl rightBody}
+convertEta (Pair {indexRel = Relevant, elementRel = Relevant, prf, first, second}) right = do
+  let rightFirst = First {secondRel = Relevant, arg = right}
+  let rightSecond = Second {firstRel = Relevant, arg = right}
+  convertFirst <- convertUntyped {rel = Relevant, left = first, right = Ntrl rightFirst}
+  convertSecond <- convertUntyped {rel = Relevant, left = second, right = Ntrl rightSecond}
+  pure (convertFirst && convertSecond)
+convertEta (Pair {indexRel = Relevant, elementRel = Irrelevant, prf, first, second}) right = do
+  let rightFirst = First {secondRel = Relevant, arg = right}
+  convertUntyped {rel = Relevant, left = first, right = Ntrl rightFirst}
+convertEta (Pair {indexRel = Irrelevant, elementRel = Relevant, prf, first, second}) right = do
+  let rightSecond = Second {firstRel = Relevant, arg = right}
+  convertUntyped {rel = Relevant, left = second, right = Ntrl rightSecond}
+convertEta left right = pure False
+
+convertUntyped Irrelevant left right = pure True
+convertUntyped Relevant (Ntrl left) (Ntrl right) = convertNtrl left right
+convertUntyped Relevant (Ntrl left) (Cnstr right) = assert_total (convertEta right left)
+convertUntyped Relevant (Cnstr left) (Ntrl right) = convertEta left right
+convertUntyped Relevant (Cnstr left) (Cnstr right) = convertCnstr left right
diff --git a/src/Obs/Universe.idr b/src/Obs/Universe.idr
index 1517c4c..14cde14 100644
--- a/src/Obs/Universe.idr
+++ b/src/Obs/Universe.idr
@@ -127,16 +127,6 @@ relevance : Universe -> Relevance
 relevance Prop = Irrelevant
 relevance (Set k) = Relevant
 
-||| True if values in `s` are proof-irrelevant.
-public export
-isIrrelevant : (s : Universe) -> Bool
-isIrrelevant = (Irrelevant ==) . relevance
-
-||| True if values in `s` are proof-relevant.
-public export
-isRelevant : (s : Universe) -> Bool
-isRelevant = (Relevant ==) . relevance
-
 ||| Returns the smallest universe containing `s`
 ||| @ s the universe to contain
 public export
@@ -155,30 +145,30 @@ dom ~> (Set k) = max (Set k) dom
 
 namespace Predicates
   public export
-  data IsIrrelevant : Universe -> Type where
-    Prop : IsIrrelevant Prop
+  data IsIrrelevant : Relevance -> Type where
+    Irrelevant : IsIrrelevant Irrelevant
 
   public export
-  data IsRelevant : Universe -> Type where
-    Set : IsRelevant (Set k)
+  data IsRelevant : Relevance -> Type where
+    Relevant : IsRelevant Relevant
 
   export
-  Uninhabited (IsIrrelevant (Set k)) where
+  Uninhabited (IsIrrelevant Relevant) where
     uninhabited _ impossible
 
   export
-  Uninhabited (IsRelevant Prop) where
+  Uninhabited (IsRelevant Irrelevant) where
     uninhabited _ impossible
 
   export
-  isIrrelevant : (s : Universe) -> Dec (IsIrrelevant s)
-  isIrrelevant Prop = Yes Prop
-  isIrrelevant (Set k) = No absurd
+  isIrrelevant : (r : Relevance) -> Dec (IsIrrelevant r)
+  isIrrelevant Irrelevant = Yes Irrelevant
+  isIrrelevant Relevant = No absurd
 
   export
-  isRelevant : (s : Universe) -> Dec (IsRelevant s)
-  isRelevant Prop = No absurd
-  isRelevant (Set k) = Yes Set
+  isRelevant : (r : Relevance) -> Dec (IsRelevant r)
+  isRelevant Irrelevant = No absurd
+  isRelevant Relevant = Yes Relevant
 
 -- Properties ------------------------------------------------------------------
 
@@ -194,22 +184,6 @@ succContains (Set k) = eqToSo $ LteIslte k k reflexive
 succLeast : (s, s' : Universe) -> So (s < s') -> So (succ s <= s')
 succLeast s s' prf = prf
 
-irrelevantReflection : (s : Universe) -> Reflects (IsIrrelevant s) (isIrrelevant s)
-irrelevantReflection Prop = RTrue Prop
-irrelevantReflection (Set k) = RFalse absurd
-
-relevantReflection : (s : Universe) -> Reflects (IsRelevant s) (isRelevant s)
-relevantReflection Prop = RFalse absurd
-relevantReflection (Set k) = RTrue Set
-
-export
-forgetIsIrrelevant : IsIrrelevant s -> relevance s = Irrelevant
-forgetIsIrrelevant Prop = Refl
-
-export
-forgetIsRelevant : IsRelevant s -> relevance s = Relevant
-forgetIsRelevant Set = Refl
-
 export
 pairRelevance : (s, s' : Universe) -> relevance (max s s') = pair (relevance s) (relevance s')
 pairRelevance Prop s' = Refl