Add sum types.

10 files changed, 538 insertions, 287 deletions

diff --git a/obs.ipkg b/obs.ipkg
index bee4872..71451bb 100644
--- a/obs.ipkg
+++ b/obs.ipkg
@@ -12,9 +12,11 @@ modules
   , Obs.Logging
   , Obs.Main
   , Obs.NormalForm
+  , Obs.NormalForm.Normalise
   , Obs.Parser
   , Obs.Sort
   , Obs.Substitution
   , Obs.Syntax
   , Obs.Term
   , Obs.Typing
+  , Obs.Typing.Conversion
diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index b8fca7b..03367dc 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -51,6 +51,23 @@ abstractSyntax ctx (Fst t) = do
 abstractSyntax ctx (Snd t) = do
   t <- abstractSyntaxBounds ctx t
   pure (Snd t)
+abstractSyntax ctx (Sum a b) = do
+  a <- abstractSyntaxBounds ctx a
+  b <- abstractSyntaxBounds ctx b
+  pure (Sum a b)
+abstractSyntax ctx (Left t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Left t)
+abstractSyntax ctx (Right t) = do
+  t <- abstractSyntaxBounds ctx t
+  pure (Right t)
+abstractSyntax ctx (Case t s b f g) = do
+  t <- abstractSyntaxBounds ctx t
+  s <- abstractSyntaxBounds ctx s
+  b <- abstractSyntaxBounds ctx b
+  f <- abstractSyntaxBounds ctx f
+  g <- abstractSyntaxBounds ctx g
+  pure (Case t s b f g)
 abstractSyntax ctx Top = pure Top
 abstractSyntax ctx Point = pure Point
 abstractSyntax ctx Bottom = pure Bottom
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index fd3a814..71b554c 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -23,6 +23,9 @@ data Constructor : Nat -> Type where
   Lambda : String -> NormalForm (S n) -> Constructor n
   Sigma  : Sort -> Sort -> String -> NormalForm n -> NormalForm (S n) -> Constructor n
   Pair   : NormalForm n -> NormalForm n -> Constructor n
+  Sum    : Sort -> Sort -> NormalForm n -> NormalForm n -> Constructor n
+  Left   : NormalForm n -> Constructor n
+  Right  : NormalForm n -> Constructor n
   Top    : Constructor n
   Bottom : Constructor n
 
@@ -32,6 +35,7 @@ data Neutral : Nat -> Type where
   App    : Neutral n -> NormalForm n -> Neutral n
   Fst    : Neutral n -> Neutral n
   Snd    : Neutral n -> Neutral n
+  Case   : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
   Absurd : Neutral n
   Equal  : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
   EqualL : Nat -> Neutral n -> NormalForm n -> Neutral n
@@ -72,6 +76,9 @@ eqCnstr (Pi s s' _ a b) (Pi l l' _ a' b') = s == l && s' == l' && eqWhnf a a' &&
 eqCnstr (Lambda _ t) (Lambda _ u) = eqWhnf t u
 eqCnstr (Sigma s s' _ a b) (Sigma l l' _ a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
 eqCnstr (Pair t u) (Pair t' u') = eqWhnf t t' && eqWhnf u u'
+eqCnstr (Sum s s' a b) (Sum l l' a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
+eqCnstr (Left t) (Left t') = eqWhnf t t'
+eqCnstr (Right t) (Right t') = eqWhnf t t'
 eqCnstr Top Top = True
 eqCnstr Bottom Bottom = True
 eqCnstr _ _ = False
@@ -80,6 +87,7 @@ eqNtrl (Var _ i) (Var _ j) = i == j
 eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u'
 eqNtrl (Fst t) (Fst t') = eqNtrl t t'
 eqNtrl (Snd t) (Snd t') = eqNtrl t t'
+eqNtrl (Case t f g) (Case t' f' g') = eqNtrl t t' && eqWhnf f f' && eqWhnf g g'
 eqNtrl Absurd Absurd = True
 eqNtrl (Equal a t u) (Equal a' t' u') = eqNtrl a a' && eqWhnf t t' && eqWhnf u u'
 eqNtrl (EqualL i t u) (EqualL j t' u') = i == j && eqNtrl t t' && eqWhnf u u'
@@ -144,6 +152,18 @@ prettyPrecCnstr d (Pair t u) =
   angles $
   group $
   neutral <++> prettyPrecWhnf Open t <+> comma <+> softline <+> prettyPrecWhnf Open u <++> neutral
+prettyPrecCnstr d (Sum _ _ a b) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Either", prettyPrecWhnf App a, prettyPrecWhnf App b]
+prettyPrecCnstr d (Left t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Left", prettyPrecWhnf App t]
+prettyPrecCnstr d (Right t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Right", prettyPrecWhnf App t]
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
@@ -160,6 +180,10 @@ prettyPrecNtrl d (Snd t) =
   parenthesise (d >= App) $
   group $
   fillSep [pretty "snd", prettyPrecNtrl App t]
+prettyPrecNtrl d (Case t f g) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "case", prettyPrecNtrl App t, prettyPrecWhnf App f, prettyPrecWhnf App g]
 prettyPrecNtrl d Absurd = pretty "absurd"
 prettyPrecNtrl d (Equal _ t u) =
   parenthesise (d >= Equal) $
@@ -231,6 +255,9 @@ renameCnstr (Pi s s' var a b) f = Pi s s' var (renameWhnf a f) (renameWhnf b $ l
 renameCnstr (Lambda var t) f = Lambda var (renameWhnf t $ lift 1 f)
 renameCnstr (Sigma s s' var a b) f = Sigma s s' var (renameWhnf a f) (renameWhnf b $ lift 1 f)
 renameCnstr (Pair t u) f = Pair (renameWhnf t f) (renameWhnf u f)
+renameCnstr (Sum s s' a b) f = Sum s s' (renameWhnf a f) (renameWhnf b f)
+renameCnstr (Left t) f = Left (renameWhnf t f)
+renameCnstr (Right t) f = Right (renameWhnf t f)
 renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom
 
@@ -238,6 +265,7 @@ renameNtrl (Var var i) f = Var var (f i)
 renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f)
 renameNtrl (Fst t) f = Fst (renameNtrl t f)
 renameNtrl (Snd t) f = Snd (renameNtrl t f)
+renameNtrl (Case t u t') f = Case (renameNtrl t f) (renameWhnf u f) (renameWhnf t' f)
 renameNtrl Absurd f = Absurd
 renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (renameWhnf t f) (renameWhnf u f)
 renameNtrl (EqualL i t u) f = EqualL i (renameNtrl t f) (renameWhnf u f)
diff --git a/src/Obs/NormalForm/Normalise.idr b/src/Obs/NormalForm/Normalise.idr
new file mode 100644
index 0000000..919067e
--- /dev/null
+++ b/src/Obs/NormalForm/Normalise.idr
@@ -0,0 +1,272 @@
+module Obs.NormalForm.Normalise
+
+import Data.Vect
+
+import Obs.Logging
+import Obs.NormalForm
+import Obs.Sort
+import Obs.Substitution
+
+-- Substitution ----------------------------------------------------------------
+
+mergeName : String -> String -> String
+mergeName "" s' = s'
+mergeName "_" s' = s'
+mergeName s s' = s
+
+wkn : Vect k String -> (Fin n -> Logging ann (NormalForm m)) -> Fin (k + n) -> Logging ann (NormalForm (k + m))
+wkn []            f = f
+wkn (var :: vars) f =
+  add
+    (Logging ann . NormalForm)
+    (pure $ Ntrl $ Var var FZ)
+    (\i => pure $ rename !(wkn vars f i) FS)
+
+partial
+substCnstr : Constructor n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (Constructor m)
+partial
+substNtrl  : Neutral n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m)
+partial export
+subst      : NormalForm n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m)
+partial export
+subst1     : NormalForm n -> NormalForm (S n) -> Logging ann (NormalForm n)
+partial export
+doApp      : NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
+partial export
+doFst      : NormalForm n -> Logging ann (NormalForm n)
+partial export
+doSnd      : NormalForm n -> Logging ann (NormalForm n)
+partial export
+doCase     : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
+partial export
+doEqual    : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
+partial
+doEqualL   : Nat -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
+partial
+doEqualR   : Nat -> Constructor n -> NormalForm n -> Logging ann (NormalForm n)
+partial
+doEqualU   : Nat -> Constructor n -> Constructor n -> Logging ann (NormalForm n)
+partial export
+doCastL    : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
+partial
+doCastR    : Constructor n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
+partial
+doCastU    : Constructor n -> Constructor n -> NormalForm n -> Logging ann (NormalForm n)
+
+substCnstr (Sort s) f = pure $ Sort s
+substCnstr (Pi s s' var a b) f = do
+  a <- subst a f
+  b <- subst b (wkn [var] f)
+  pure (Pi s s' var a b)
+substCnstr (Lambda var t) f = do
+  t <- subst t (wkn [var] f)
+  pure (Lambda var t)
+substCnstr (Sigma s s' var a b) f = do
+  a <- subst a f
+  b <- subst b (wkn [var] f)
+  pure (Sigma s s' var a b)
+substCnstr (Pair t u) f = do
+  t <- subst t f
+  u <- subst u f
+  pure (Pair t u)
+substCnstr (Sum s s' a b) f = do
+  a <- subst a f
+  b <- subst b f
+  pure (Sum s s' a b)
+substCnstr (Left t) f = do
+  t <- subst t f
+  pure (Left t)
+substCnstr (Right t) f = do
+  t <- subst t f
+  pure (Right t)
+substCnstr Top f = pure $ Top
+substCnstr Bottom  f = pure $ Bottom
+
+substNtrl (Var var i) f = do
+  Ntrl (Var var' j) <- f i
+    | t => pure t
+  pure (Ntrl (Var (mergeName var' var) j))
+substNtrl (App t u) f = do
+  t <- substNtrl t f
+  u <- subst u f
+  doApp t u
+substNtrl (Fst t) f = do
+  t <- substNtrl t f
+  doFst t
+substNtrl (Snd t) f = do
+  t <- substNtrl t f
+  doSnd t
+substNtrl (Case t u t') f = do
+  t <- substNtrl t f
+  u <- subst u f
+  t' <- subst t' f
+  doCase t u t'
+substNtrl Absurd f = pure $ Ntrl Absurd
+substNtrl (Equal a t u) f = do
+  a <- substNtrl a f
+  t <- subst t f
+  u <- subst u f
+  doEqual a t u
+substNtrl (EqualL i t u) f = do
+  t <- substNtrl t f
+  u <- subst u f
+  doEqualL i t u
+substNtrl (EqualR i t u) f = do
+  t <- substCnstr t f
+  u <- substNtrl u f
+  doEqualR i t u
+substNtrl (EqualU i t u) f = do
+  t <- substCnstr t f
+  u <- substCnstr u f
+  doEqualU i t u
+substNtrl (CastL a b t) f = do
+  a <- substNtrl a f
+  b <- subst b f
+  t <- subst t f
+  doCastL 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 (CastU a b t) f = do
+  a <- substCnstr a f
+  b <- substCnstr b f
+  t <- subst t f
+  doCastU a b t
+
+subst (Ntrl t)  f = substNtrl t f
+subst (Cnstr t) f = map Cnstr $ substCnstr t f
+subst Irrel     f = pure Irrel
+
+subst1 t u = subst u (add (Logging ann . NormalForm) (pure t) (pure . point))
+
+doApp (Ntrl t) u = pure $ Ntrl (App t u)
+doApp Irrel u = pure $ Irrel
+doApp (Cnstr (Lambda var t)) u = subst t (add (Logging ann . NormalForm) (pure u) (pure . point))
+doApp (Cnstr t) u = inScope "bug" $ inScope "wrong constructor in apply" $ fatal t
+
+doFst (Ntrl t) = pure $ Ntrl (Fst t)
+doFst Irrel = pure $ Irrel
+doFst (Cnstr (Pair t u)) = pure $ t
+doFst (Cnstr t) = inScope "bug" $ inScope "wrong constructor in fst" $ fatal t
+
+doSnd (Ntrl t) = pure $ Ntrl (Snd t)
+doSnd Irrel = pure $ Irrel
+doSnd (Cnstr (Pair t u)) = pure $ u
+doSnd (Cnstr t) = inScope "bug" $ inScope "wrong constructor in snd" $ fatal t
+
+doCase (Ntrl t) f g = pure $ Ntrl (Case t f g)
+doCase Irrel f g = inScope "bug" $ inScope "wrong constructor in case" $ fatal "Irrel"
+doCase (Cnstr (Left t)) f g = doApp f t
+doCase (Cnstr (Right t)) f g = doApp g t
+doCase (Cnstr t) f g = inScope "bug" $ inScope "wrong constructor in case" $ fatal t
+
+doEqual (Ntrl a) t u = pure $ Ntrl (Equal a t u)
+doEqual Irrel t u = inScope "bug" $ inScope "wrong type over equal" $ fatal "Irrel"
+doEqual (Cnstr (Sort Prop)) t u =
+  pure $
+  Cnstr (Sigma Prop Prop "_"
+    (Cnstr $ Pi Prop Prop "_" t (weaken 1 u))
+    (weaken 1 $ Cnstr $ Pi Prop Prop "_" u (weaken 1 t)))
+doEqual (Cnstr (Sort (Set k))) t u = doEqualL k t u
+doEqual (Cnstr (Pi s s' var a b)) t u = do
+  eqLhs <- doApp (weaken 1 t) (Ntrl $ Var var FZ)
+  eqRhs <- doApp (weaken 1 u) (Ntrl $ Var var FZ)
+  eq <- doEqual b eqLhs eqRhs -- b in Set because Pi in Set.
+  pure $ Cnstr (Pi s Prop var a eq)
+doEqual (Cnstr (Sigma s s' var a b)) t u = do
+  t1 <- doFst t
+  u1 <- doFst u
+  eq1 <- case s of
+    Prop => pure $ Cnstr Top
+    (Set i) => doEqual a t1 u1
+  eq2 <- case s' of
+    Prop => pure $ Cnstr Top
+    (Set i) => do
+      bt <- subst1 t1 b
+      bu <- subst1 u1 b
+      t2 <- doSnd t
+      t2 <- doCastL bt bu t2
+      u2 <- doSnd u
+      doEqual bu t2 u2
+  pure $ Cnstr (Sigma Prop Prop "_" eq1 (weaken 1 eq2))
+doEqual (Cnstr (Sum s s' a b)) t u = do
+  let x = Ntrl $ Var "x" 1
+  let y = Ntrl $ Var "y" 0
+  ll <- doEqual (weaken 2 a) x y
+  lr <- pure $ Cnstr Bottom
+  rl <- pure $ Cnstr Bottom
+  rr <- doEqual (weaken 2 b) x y
+  fBody <- doCase (weaken 1 u) (Cnstr (Lambda "y" ll)) (Cnstr (Lambda "y" lr))
+  gBody <- doCase (weaken 1 u) (Cnstr (Lambda "y" rl)) (Cnstr (Lambda "y" rr))
+  doCase t (Cnstr (Lambda "x" fBody)) (Cnstr (Lambda "x" gBody))
+doEqual (Cnstr Top) t u = pure $ Cnstr Top
+doEqual (Cnstr Bottom) t u = pure $ Cnstr Top
+
+doEqualL i (Ntrl t) u = pure $ Ntrl (EqualL i t u)
+doEqualL i Irrel u = inScope "bug" $ inScope "wrong type under equalL" $ fatal "Irrel"
+doEqualL i (Cnstr t) u = doEqualR i t u
+
+doEqualR i t (Ntrl u) = pure $ Ntrl (EqualR i t u)
+doEqualR i t Irrel = inScope "bug" $ inScope "wrong type under equalR" $ fatal "Irrel"
+doEqualR i t (Cnstr u) = doEqualU i t u
+
+doEqualU i (Sort s) (Sort s') = pure $ Cnstr Top -- have suc s = i = suc s', and suc injective
+doEqualU i (Pi s s' _ a b) (Pi l l' var a' b') = case (s == s' && l == l') of
+  False => pure $ Cnstr Bottom
+  True => do
+    eqLhs <- doEqual (cast s) a' a
+    let x = Ntrl $ Var var FZ
+    b <- subst b (add (Logging ann . NormalForm) (doCastL (weaken 1 a') (weaken 1 a) x) (pure . Ntrl . Var "" . FS))
+    eqRhs <- doEqual (cast s') b b'
+    pure $ Cnstr (Sigma Prop Prop "" eqLhs $ weaken 1 $ Cnstr (Pi s Prop var a' eqRhs))
+doEqualU i (Sigma s s' _ a b) (Sigma l l' var a' b') = case (s == s' && l == l') of
+  False => pure $ Cnstr Bottom
+  True => do
+    eqLhs <- doEqual (cast s) a' a
+    let x = Ntrl $ Var var FZ
+    b <- subst b (add (Logging ann . NormalForm) (doCastL (weaken 1 a') (weaken 1 a) x) (pure . Ntrl . Var "" . FS))
+    eqRhs <- doEqual (cast s') b b'
+    pure $ Cnstr (Sigma Prop Prop "" eqLhs $ weaken 1 $ Cnstr (Pi s Prop var a' eqRhs))
+doEqualU i (Sum s s' a b) (Sum l l' a' b') = case (s == s' && l == l') of
+  False => pure $ Cnstr Bottom
+  True => do
+    eqLhs <- doEqual (cast s) a a'
+    eqRhs <- doEqual (cast s) b b'
+    pure $ Cnstr (Sigma Prop Prop "" eqLhs (weaken 1 eqRhs))
+doEqualU i t u = pure $ Ntrl (EqualU i t u) -- assumption: only logical values reach this far
+
+doCastL (Ntrl a) b t = pure $ Ntrl (CastL a b t)
+doCastL Irrel b t = inScope "bug" $ inScope "wrong type for cast" $ fatal "Irrel"
+doCastL (Cnstr a) b t = doCastR a b t
+
+doCastR a (Ntrl b) t = pure $ Ntrl (CastR a b t)
+doCastR a Irrel t = inScope "bug" $ inScope "wrong type for cast" $ fatal "Irrel"
+doCastR a (Cnstr b) t = doCastU a b t
+
+doCastU (Sort s) (Sort s') t = pure t
+doCastU (Pi s s' _ a b) (Pi l l' var a' b') t = do
+  let x' = Ntrl $ Var var FZ
+  let x = doCastL (weaken 1 a') (weaken 1 a) x'
+  b <- subst b (add (Logging ann . NormalForm) x (pure . Ntrl . Var "" . FS))
+  b' <- subst b' (add (Logging ann . NormalForm) (pure x') (pure . Ntrl . Var "" . FS))
+  fx <- doApp (weaken 1 t) !x
+  cast <- doCastL b b' fx
+  pure $ Cnstr (Lambda var cast)
+doCastU (Sigma s s' _ a b) (Sigma l l' var a' b') t = do
+  t1 <- doFst t
+  t2 <- doSnd t
+  t1' <- doCastL a a' t1
+  b <- subst1 t1 b
+  b' <- subst1 t1' b'
+  t2' <- doCastL b b' t2
+  pure $ Cnstr (Pair t1' t2')
+doCastU (Sum s s' a b) (Sum l l' a' b') t = do
+  let x = Ntrl $ Var "x" 0
+  castL <- doCastL (weaken 1 a) (weaken 1 a') x
+  castR <- doCastL (weaken 1 b) (weaken 1 b') x
+  doCase t (Cnstr (Lambda "x" (Cnstr (Left castL)))) (Cnstr (Lambda "x" (Cnstr (Right castR))))
+doCastU Top Top t = pure Irrel
+doCastU Bottom Bottom t = pure Irrel
+doCastU a b t = pure $ Ntrl (CastU a b t)
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index 0ccba86..acb1360 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -25,6 +25,10 @@ data ObsTokenKind
   | OTNat
   | OTFst
   | OTSnd
+  | OTEither
+  | OTLeft
+  | OTRight
+  | OTCase
   | OTPoint
   | OTVoid
   | OTAbsurd
@@ -58,6 +62,10 @@ Eq ObsTokenKind where
   OTNat == OTNat = True
   OTFst == OTFst = True
   OTSnd == OTSnd = True
+  OTEither == OTEither = True
+  OTLeft == OTLeft = True
+  OTRight == OTRight = True
+  OTCase == OTCase = True
   OTPoint == OTPoint = True
   OTVoid == OTVoid = True
   OTAbsurd == OTAbsurd = True
@@ -93,6 +101,10 @@ TokenKind ObsTokenKind where
   tokValue OTNat s = stringToNatOrZ s
   tokValue OTFst s = ()
   tokValue OTSnd s = ()
+  tokValue OTEither s = ()
+  tokValue OTLeft s = ()
+  tokValue OTRight s = ()
+  tokValue OTCase s = ()
   tokValue OTPoint s = ()
   tokValue OTVoid s = ()
   tokValue OTAbsurd s = ()
@@ -126,6 +138,10 @@ Show ObsToken where
   show (Tok OTNat s) = s
   show (Tok OTFst s) = "fst"
   show (Tok OTSnd s) = "snd"
+  show (Tok OTEither s) = "Either"
+  show (Tok OTLeft s) = "Left"
+  show (Tok OTRight s) = "Right"
+  show (Tok OTCase s) = "case"
   show (Tok OTPoint s) = "tt"
   show (Tok OTVoid s) = "Void"
   show (Tok OTAbsurd s) = "absurd"
@@ -156,6 +172,10 @@ keywords =
   , ("Prop", OTProp)
   , ("fst", OTFst)
   , ("snd", OTSnd)
+  , ("Either", OTEither)
+  , ("Left", OTLeft)
+  , ("Right", OTRight)
+  , ("case", OTCase)
   , ("tt", OTPoint)
   , ("Void", OTVoid)
   , ("absurd", OTAbsurd)
@@ -195,18 +215,26 @@ uncurry : (n : _) -> op a b n -> Vect n a -> b
 uncurry 0     f []        = f
 uncurry (S n) f (x :: xs) = uncurry n (f x) xs
 
-headForms : List (ObsTokenKind, (n ** (Vect n (WithBounds Syntax) -> Syntax)))
+termForms : List (ObsTokenKind, Syntax)
+termForms =
+  [ (OTPoint, Point)
+  , (OTVoid, Bottom)
+  , (OTUnit, Top)
+  ]
+
+headForms : List (ObsTokenKind, (n ** (Vect (S n) (WithBounds Syntax) -> Syntax)))
 headForms =
-  [ (OTFst, (1 ** uncurry 1 Fst))
-  , (OTSnd, (1 ** uncurry 1 Snd))
-  , (OTPoint, (0 ** uncurry 0 Point))
-  , (OTVoid, (0 ** uncurry 0 Bottom))
-  , (OTAbsurd, (2 ** uncurry 2 Absurd))
-  , (OTRefl, (1 ** uncurry 1 Refl))
-  , (OTTransp, (5 ** uncurry 5 Transp))
-  , (OTCast, (3 ** uncurry 3 Cast))
-  , (OTCastRefl, (1 ** uncurry 1 CastId))
-  , (OTUnit, (0 ** uncurry 0 Top))
+  [ (OTFst, (0 ** uncurry 1 Fst))
+  , (OTSnd, (0 ** uncurry 1 Snd))
+  , (OTEither, (1 ** uncurry 2 Sum))
+  , (OTLeft, (0 ** uncurry 1 Left))
+  , (OTRight, (0 ** uncurry 1 Right))
+  , (OTCase, (4 ** uncurry 5 Case))
+  , (OTAbsurd, (1 ** uncurry 2 Absurd))
+  , (OTRefl, (0 ** uncurry 1 Refl))
+  , (OTTransp, (4 ** uncurry 5 Transp))
+  , (OTCast, (2 ** uncurry 3 Cast))
+  , (OTCastRefl, (0 ** uncurry 1 CastId))
   ]
 
 declForms : List (ObsTokenKind, (WithBounds String -> op (WithBounds Syntax) Syntax 2))
@@ -265,7 +293,8 @@ exp : Grammar state ObsToken True (WithBounds Syntax)
 noSortsTerm =
   parens exp <|>
   var <|>
-  bounds (map (uncurry Pair) (pair exp))
+  bounds (map (uncurry Pair) (pair exp)) <|>
+  bounds (choiceMap (\(k, s) => map (const s) (match k)) termForms)
 
 term = noSortsTerm <|> map (map Sort) noArgSort
 
@@ -274,7 +303,7 @@ head =
   map (map Sort) sort <|>
   bounds
     (choiceMap
-      (\(hd, (n ** f)) => match hd *> commit *> [| f (count n (whitespace *> term)) |])
+      (\(hd, (n ** f)) => match hd *> commit *> [| f (count (S n) (whitespace *> term)) |])
       headForms)
 
 spine = map (uncurry $ foldl (\t, u => joinBounds (map (\_ => map (\_ => App t u) u) t))) $
@@ -306,7 +335,7 @@ partial
 fullDef : Grammar state ObsToken True Definition
 fullDef =
   seq
-    [| MkPair (decl exp) (optional whitespace *> match OTNewlines *> def) |]
+    [| MkPair (decl exp <* commit) (optional whitespace *> match OTNewlines *> def <* commit) |]
     (\((name, ty), (name', tm)) =>
       if name.val == name'.val
         then pure (MkDefinition {name = name, ty, tm})
@@ -316,7 +345,7 @@ partial
 file : Grammar state ObsToken False (List Definition)
 file =
   optional (whitespace *> match OTNewlines) *>
-  sepEndBy (optional whitespace *> match OTNewlines) fullDef <*
+  sepEndBy (optional whitespace *> match OTNewlines) (fullDef <* commit) <*
   eof
 
 whitespaceIrrelevant : WithBounds ObsToken -> WithBounds ObsToken
diff --git a/src/Obs/Sort.idr b/src/Obs/Sort.idr
index 70d5ed2..bbd6975 100644
--- a/src/Obs/Sort.idr
+++ b/src/Obs/Sort.idr
@@ -43,6 +43,11 @@ suc Prop    = Set 0
 suc (Set i) = Set (S i)
 
 public export
+ensureSet : Sort -> Sort
+ensureSet Prop    = Set 0
+ensureSet (Set i) = Set i
+
+public export
 lub : Sort -> Sort -> Sort
 lub Prop    s'      = s'
 lub (Set i) Prop    = Set i
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 36b1b9f..9f64c38 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -23,6 +23,11 @@ data Syntax : Type where
   Pair   : WithBounds Syntax -> WithBounds Syntax -> Syntax
   Fst    : WithBounds Syntax -> Syntax
   Snd    : WithBounds Syntax -> Syntax
+  -- Disjoint Coproducts
+  Sum    : WithBounds Syntax -> WithBounds Syntax -> Syntax
+  Left   : WithBounds Syntax -> Syntax
+  Right  : WithBounds Syntax -> Syntax
+  Case   : WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> WithBounds Syntax -> Syntax
   -- True
   Top    : Syntax
   Point  : Syntax
@@ -84,6 +89,22 @@ prettyPrec d (Snd t) =
   parenthesise (d >= App) $
   group $
   fillSep [pretty "snd", prettyPrecBounds App t]
+prettyPrec d (Sum a b) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Either", prettyPrecBounds App a, prettyPrecBounds App b]
+prettyPrec d (Left t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Left", prettyPrecBounds App t]
+prettyPrec d (Right t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Right", prettyPrecBounds App t]
+prettyPrec d (Case t s b f g) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "case", prettyPrecBounds App t, prettyPrecBounds App s, prettyPrecBounds App b, prettyPrecBounds App f, prettyPrecBounds App g]
 prettyPrec d Top = pretty "()"
 prettyPrec d Point = pretty "tt"
 prettyPrec d Bottom = pretty "Void"
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 446fdcb..be3721f 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -24,6 +24,11 @@ data Term : Nat -> Type where
   Pair   : WithBounds (Term n) -> WithBounds (Term n) -> Term n
   Fst    : WithBounds (Term n) -> Term n
   Snd    : WithBounds (Term n) -> Term n
+  -- Disjoint Coproducts
+  Sum    : WithBounds (Term n) -> WithBounds (Term n) -> Term n
+  Left   : WithBounds (Term n) -> Term n
+  Right  : WithBounds (Term n) -> Term n
+  Case   : WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> WithBounds (Term n) -> Term n
   -- True
   Top    : Term n
   Point  : Term n
@@ -90,6 +95,22 @@ prettyPrec d (Snd t) =
   parenthesise (d >= App) $
   group $
   fillSep [pretty "snd", prettyPrecBounds App t]
+prettyPrec d (Sum a b) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Either", prettyPrecBounds App a, prettyPrecBounds App b]
+prettyPrec d (Left t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Left", prettyPrecBounds App t]
+prettyPrec d (Right t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "Right", prettyPrecBounds App t]
+prettyPrec d (Case t s b f g) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "case", prettyPrecBounds App t, prettyPrecBounds App s, prettyPrecBounds App b, prettyPrecBounds App f, prettyPrecBounds App g]
 prettyPrec d Top = pretty "()"
 prettyPrec d Point = pretty "tt"
 prettyPrec d Bottom = pretty "Void"
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index 3ec91f7..b327397 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -4,9 +4,11 @@ import Data.Vect
 
 import Obs.Logging
 import Obs.NormalForm
+import Obs.NormalForm.Normalise
 import Obs.Sort
 import Obs.Substitution
 import Obs.Term
+import Obs.Typing.Conversion
 
 import System
 
@@ -34,271 +36,6 @@ typeMismatch bounds lhs rhs = inScope "type mismatch" $ mismatch bounds lhs rhs
 sortMismatch : Bounds -> Doc ann -> Doc ann -> Logging ann a
 sortMismatch bounds lhs rhs = inScope "sort mismatch" $ mismatch bounds lhs rhs
 
--- Substitution ----------------------------------------------------------------
-
-mergeName : String -> String -> String
-mergeName "" s' = s'
-mergeName "_" s' = s'
-mergeName s s' = s
-
-wkn : Vect k String -> (Fin n -> Logging ann (NormalForm m)) -> Fin (k + n) -> Logging ann (NormalForm (k + m))
-wkn []            f = f
-wkn (var :: vars) f =
-  add
-    (Logging ann . NormalForm)
-    (pure $ Ntrl $ Var var FZ)
-    (\i => pure $ rename !(wkn vars f i) FS)
-
-covering partial
-substCnstr : Constructor n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (Constructor m)
-covering partial
-substNtrl  : Neutral n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m)
-covering partial
-subst      : NormalForm n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m)
-covering partial
-subst1     : NormalForm n -> NormalForm (S n) -> Logging ann (NormalForm n)
-covering partial
-doApp      : NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doFst      : NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doSnd      : NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doEqual    : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doEqualL   : Nat -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doEqualR   : Nat -> Constructor n -> NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doEqualU   : Nat -> Constructor n -> Constructor n -> Logging ann (NormalForm n)
-covering partial
-doCastL    : NormalForm n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doCastR    : Constructor n -> NormalForm n -> NormalForm n -> Logging ann (NormalForm n)
-covering partial
-doCastU    : Constructor n -> Constructor n -> NormalForm n -> Logging ann (NormalForm n)
-
-substCnstr (Sort s) f = pure $ Sort s
-substCnstr (Pi s s' var a b) f = do
-  a <- subst a f
-  b <- subst b (wkn [var] f)
-  pure (Pi s s' var a b)
-substCnstr (Lambda var t) f = do
-  t <- subst t (wkn [var] f)
-  pure (Lambda var t)
-substCnstr (Sigma s s' var a b) f = do
-  a <- subst a f
-  b <- subst b (wkn [var] f)
-  pure (Sigma s s' var a b)
-substCnstr (Pair t u) f = do
-  t <- subst t f
-  u <- subst u f
-  pure (Pair t u)
-substCnstr Top f = pure $ Top
-substCnstr Bottom  f = pure $ Bottom
-
-substNtrl (Var var i) f = do
-  Ntrl (Var var' j) <- f i
-    | t => pure t
-  pure (Ntrl (Var (mergeName var' var) j))
-substNtrl (App t u) f = do
-  t <- substNtrl t f
-  u <- subst u f
-  doApp t u
-substNtrl (Fst t) f = do
-  t <- substNtrl t f
-  doFst t
-substNtrl (Snd t) f = do
-  t <- substNtrl t f
-  doSnd t
-substNtrl Absurd f = pure $ Ntrl Absurd
-substNtrl (Equal a t u) f = do
-  a <- substNtrl a f
-  t <- subst t f
-  u <- subst u f
-  doEqual a t u
-substNtrl (EqualL i t u) f = do
-  t <- substNtrl t f
-  u <- subst u f
-  doEqualL i t u
-substNtrl (EqualR i t u) f = do
-  t <- substCnstr t f
-  u <- substNtrl u f
-  doEqualR i t u
-substNtrl (EqualU i t u) f = do
-  t <- substCnstr t f
-  u <- substCnstr u f
-  doEqualU i t u
-substNtrl (CastL a b t) f = do
-  a <- substNtrl a f
-  b <- subst b f
-  t <- subst t f
-  doCastL 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 (CastU a b t) f = do
-  a <- substCnstr a f
-  b <- substCnstr b f
-  t <- subst t f
-  doCastU a b t
-
-subst (Ntrl t)  f = substNtrl t f
-subst (Cnstr t) f = map Cnstr $ substCnstr t f
-subst Irrel     f = pure Irrel
-
-subst1 t u = subst u (add (Logging ann . NormalForm) (pure t) (pure . point))
-
-doApp (Ntrl t) u = pure $ Ntrl (App t u)
-doApp Irrel u = pure $ Irrel
-doApp (Cnstr (Lambda var t)) u = subst t (add (Logging ann . NormalForm) (pure u) (pure . point))
-doApp (Cnstr t) u = inScope "bug" $ inScope "wrong constructor in apply" $ fatal t
-
-doFst (Ntrl t) = pure $ Ntrl (Fst t)
-doFst Irrel = pure $ Irrel
-doFst (Cnstr (Pair t u)) = pure $ t
-doFst (Cnstr t) = inScope "bug" $ inScope "wrong constructor in fst" $ fatal t
-
-doSnd (Ntrl t) = pure $ Ntrl (Snd t)
-doSnd Irrel = pure $ Irrel
-doSnd (Cnstr (Pair t u)) = pure $ u
-doSnd (Cnstr t) = inScope "bug" $ inScope "wrong constructor in snd" $ fatal t
-
-doEqual (Ntrl a) t u = pure $ Ntrl (Equal a t u)
-doEqual Irrel t u = inScope "bug" $ inScope "wrong type over equal" $ fatal "Irrel"
-doEqual (Cnstr (Sort Prop)) t u =
-  pure $
-  Cnstr (Sigma Prop Prop "_"
-    (Cnstr $ Pi Prop Prop "_" t (weaken 1 u))
-    (weaken 1 $ Cnstr $ Pi Prop Prop "_" u (weaken 1 t)))
-doEqual (Cnstr (Sort (Set k))) t u = doEqualL k t u
-doEqual (Cnstr (Pi s s' var a b)) t u = do
-  eqLhs <- doApp (weaken 1 t) (Ntrl $ Var var FZ)
-  eqRhs <- doApp (weaken 1 u) (Ntrl $ Var var FZ)
-  eq <- doEqual b eqLhs eqRhs -- b in Set because Pi in Set.
-  pure $ Cnstr (Pi s Prop var a eq)
-doEqual (Cnstr (Sigma s s' var a b)) t u = do
-  t1 <- doFst t
-  u1 <- doFst u
-  eq1 <- case s of
-    Prop => pure $ Cnstr Top
-    (Set i) => doEqual a t1 u1
-  eq2 <- case s' of
-    Prop => pure $ Cnstr Top
-    (Set i) => do
-      bt <- subst1 t1 b
-      bu <- subst1 u1 b
-      t2 <- doSnd t
-      t2 <- doCastL bt bu t2
-      u2 <- doSnd u
-      doEqual bu t2 u2
-  pure $ Cnstr (Sigma Prop Prop "_" eq1 (weaken 1 eq2))
-doEqual (Cnstr Top) t u = pure $ Cnstr Top
-doEqual (Cnstr Bottom) t u = pure $ Cnstr Top
-
-doEqualL i (Ntrl t) u = pure $ Ntrl (EqualL i t u)
-doEqualL i Irrel u = inScope "bug" $ inScope "wrong type under equalL" $ fatal "Irrel"
-doEqualL i (Cnstr t) u = doEqualR i t u
-
-doEqualR i t (Ntrl u) = pure $ Ntrl (EqualR i t u)
-doEqualR i t Irrel = inScope "bug" $ inScope "wrong type under equalR" $ fatal "Irrel"
-doEqualR i t (Cnstr u) = doEqualU i t u
-
-doEqualU i (Sort s) (Sort s') = pure $ Cnstr Top -- have suc s = i = suc s', and suc injective
-doEqualU i (Pi s s' _ a b) (Pi l l' var a' b') = case (s == s' && l == l') of
-  False => pure $ Cnstr Bottom
-  True => do
-    eqLhs <- doEqual (cast s) a' a
-    let x = Ntrl $ Var var FZ
-    b <- subst b (add (Logging ann . NormalForm) (doCastL (weaken 1 a') (weaken 1 a) x) (pure . Ntrl . Var "" . FS))
-    eqRhs <- doEqual (cast s') b b'
-    pure $ Cnstr (Sigma Prop Prop "" eqLhs $ weaken 1 $ Cnstr (Pi s Prop var a' eqRhs))
-doEqualU i (Sigma s s' _ a b) (Sigma l l' var a' b') = case (s == s' && l == l') of
-  False => pure $ Cnstr Bottom
-  True => do
-    eqLhs <- doEqual (cast s) a' a
-    let x = Ntrl $ Var var FZ
-    b <- subst b (add (Logging ann . NormalForm) (doCastL (weaken 1 a') (weaken 1 a) x) (pure . Ntrl . Var "" . FS))
-    eqRhs <- doEqual (cast s') b b'
-    pure $ Cnstr (Sigma Prop Prop "" eqLhs $ weaken 1 $ Cnstr (Pi s Prop var a' eqRhs))
-doEqualU i t u = pure $ Ntrl (EqualU i t u) -- assumption: only logical values reach this far
-
-doCastL (Ntrl a) b t = pure $ Ntrl (CastL a b t)
-doCastL Irrel b t = inScope "bug" $ inScope "wrong type for cast" $ fatal "Irrel"
-doCastL (Cnstr a) b t = doCastR a b t
-
-doCastR a (Ntrl b) t = pure $ Ntrl (CastR a b t)
-doCastR a Irrel t = inScope "bug" $ inScope "wrong type for cast" $ fatal "Irrel"
-doCastR a (Cnstr b) t = doCastU a b t
-
-doCastU (Sort s) (Sort s') t = pure t
-doCastU (Pi s s' _ a b) (Pi l l' var a' b') t = do
-  let x' = Ntrl $ Var var FZ
-  let x = doCastL (weaken 1 a') (weaken 1 a) x'
-  b <- subst b (add (Logging ann . NormalForm) x (pure . Ntrl . Var "" . FS))
-  b' <- subst b' (add (Logging ann . NormalForm) (pure x') (pure . Ntrl . Var "" . FS))
-  fx <- doApp (weaken 1 t) !x
-  cast <- doCastL b b' fx
-  pure $ Cnstr (Lambda var cast)
-doCastU (Sigma s s' _ a b) (Sigma l l' var a' b') t = do
-  t1 <- doFst t
-  t2 <- doSnd t
-  t1' <- doCastL a a' t1
-  b <- subst1 t1 b
-  b' <- subst1 t1' b'
-  t2' <- doCastL b b' t2
-  pure $ Cnstr (Pair t1' t2')
-
-doCastU Top Top t = pure Irrel
-doCastU Bottom Bottom t = pure Irrel
-doCastU a b t = pure $ Ntrl (CastU a b t)
-
--- Conversion ------------------------------------------------------------------
-
--- invariant: all definitions fully expanded
--- invariant: m |- t, u <- a : s
-covering partial
-convert : (t, u, a : NormalForm n) -> Sort -> Logging ann Bool
--- In sort Prop
-convert Irrel Irrel a Prop = pure True
--- In unknown type in set
-convert t u (Ntrl _) (Set k) = pure $ t == u
--- In type Set
-convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort _)) (Set _) = pure $ s' == s''
-convert (Cnstr (Pi s s' _ a b)) (Cnstr (Pi l l' _ a' b')) (Cnstr (Sort _)) (Set _) =
-  pure $
-  s == l && s' == l' && !(convert a a' (cast s) (suc s)) && !(convert b b' (cast s') (suc s'))
-convert (Cnstr (Sigma s s' _ a b)) (Cnstr (Sigma l l' _ a' b')) (Cnstr (Sort _)) (Set _) =
-  pure $
-  s == l && s' == l' && !(convert a a' (cast s) (suc s)) && !(convert b b' (cast s') (suc s'))
-convert (Cnstr Top) (Cnstr Top) (Cnstr (Sort _)) (Set _) = pure True
-convert (Cnstr Bottom) (Cnstr Bottom) (Cnstr (Sort _)) (Set _) = pure True
-convert (Ntrl t) u (Cnstr (Sort s)) (Set k) = pure $ Ntrl t == u
-convert t (Ntrl u) (Cnstr (Sort s)) (Set k) = pure $ t == Ntrl u
-convert t u (Cnstr (Sort s)) (Set k) = pure $ False
--- In type Pi
-convert t u (Cnstr (Pi s s' var a b)) (Set k) = do
-  t <- doApp (weaken 1 t) (Ntrl $ Var var FZ)
-  u <- doApp (weaken 1 u) (Ntrl $ Var var FZ)
-  convert t u b s'
--- In type Sigma
-convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do
-  t1 <- doFst t
-  u1 <- doFst t
-  True <- convert t1 u1 a s
-    | False => pure False
-  b <- subst1 t1 b
-  t2 <- doSnd t
-  u2 <- doSnd t
-  convert t2 u2 b s'
--- Default
-convert t u a s =
-  inScope "invalid conversion" $ fatal $
-  fillSep {ann} [prettyPrec App t, prettyPrec App u, prettyPrec App a, prettyPrec App s]
-
-
 -- Typing Contexts -------------------------------------------------------------
 
 infix 5 ::<
@@ -324,7 +61,7 @@ index (ctx ::< (var, ty, s))    FZ     = (Ntrl $ Var var FZ, weaken 1 ty, s)
 index (ctx :< _)                (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
 index (ctx ::< _)               (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
 
-covering partial
+partial
 asSubst : (ctx : TyContext m n) -> Fin n -> Logging ann (NormalForm m)
 asSubst (ctx :< def)             FZ     = subst def.tm (asSubst ctx)
 asSubst (ctx ::< (var, _, Prop)) FZ     = pure Irrel
@@ -334,11 +71,11 @@ asSubst (ctx ::< _)              (FS i) = map (weaken 1) (asSubst ctx i)
 
 -- Checking and Inference ------------------------------------------------------
 
-covering partial
+partial
 check : TyContext m n -> WithBounds (Term n) -> NormalForm n -> Sort -> Logging ann (NormalForm n)
-covering partial
+partial
 infer : TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, NormalForm n, Sort)
-covering partial
+partial
 inferType : {default typeMismatch tag : forall a . Bounds -> Doc ann -> Doc ann -> Logging ann a}
   -> TyContext m n -> WithBounds (Term n) -> Logging ann (NormalForm n, Sort)
 
@@ -364,6 +101,20 @@ check ctx tm ty s = case (tm.val, ty) of
       (Prop, Prop) => pure Irrel
       _ => pure (Cnstr $ Pair t u)
   (Pair _ _, ty) => typeMismatch tm.bounds (pretty "sigma") (pretty ty)
+  (Left t, Cnstr (Sum s s' a b)) => do
+    inScope "check" $ trace $ map (\_ => "checking left injection") tm
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking subterm for type" <++> pretty a) tm
+    t <- check ctx t a s
+    inScope "check" $ trace $ map (\_ => " subterm is well typed") tm
+    pure (Cnstr $ Left t)
+  (Left _, ty) => typeMismatch tm.bounds (pretty "sum") (pretty ty)
+  (Right t, Cnstr (Sum s s' a b)) => do
+    inScope "check" $ trace $ map (\_ => "checking right injection") tm
+    inScope "check" $ trace $ map (\_ => pretty {ann} "checking subterm for type" <++> pretty b) tm
+    t <- check ctx t b s'
+    inScope "check" $ trace $ map (\_ => " subterm is well typed") tm
+    pure (Cnstr $ Right t)
+  (Right _, ty) => typeMismatch tm.bounds (pretty "sum") (pretty ty)
   (_, _) => do
     inScope "check" $ trace $ map (\_ => "checking has fallen through") tm
     (v, a, s') <- infer ctx tm
@@ -421,13 +172,48 @@ infer ctx tm = case tm.val of
   (Snd t) => do
     inScope "infer" $ trace $ map (\_ => "encountered first projection") tm
     (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t
-      | (_, ty, _) => inScope "wrong type to fst" $ fatal (map (\_ => ty) tm)
+      | (_, ty, _) => inScope "wrong type to snd" $ fatal (map (\_ => ty) tm)
     inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) tm
     t1 <- doFst t
     res <- doSnd t
     b <- subst1 t1 b
     inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty b) tm
     pure (res, b, s')
+  (Sum a b) => do
+    inScope "infer" $ trace $ map (\_ => "encountered sum type") tm
+    (a, s) <- inferType ctx a
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "left has type" <++> pretty a) tm
+    (b, s') <- inferType ctx b
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "right has type" <++> pretty b) tm
+    pure (Cnstr (Sum s s' a b), cast (ensureSet (lub s s')), suc (ensureSet (lub s s')))
+  (Left _) => inScope "cannot infer type" $ fatal tm
+  (Right _) => inScope "cannot infer type" $ fatal tm
+  (Case t l out f g) => do
+    inScope "infer" $ trace $ map (\_ => "encountered case") tm
+    (t, ty@(Cnstr (Sum s s' a b)), s'') <- infer ctx t
+      | (_, ty, _) => inScope "wrong type to case" $ fatal (map (\_ => ty) tm)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "sum has type" <++> pretty ty) tm
+    (Cnstr (Sort l), _) <- inferType ctx l
+      | (s, _) => typeMismatch l.bounds (pretty "sort") (pretty s)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "output has sort" <++> pretty l) tm
+    let ty' = Cnstr (Pi s'' (suc l) "x" ty (cast l))
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking output has type" <++> pretty ty') tm
+    out <- check ctx out ty' (s'' ~> suc l)
+    inScope "infer" $ trace $ map (\_ => "output is well typed") tm
+    outL <- doApp (weaken 1 out) (Cnstr (Left (Ntrl (Var "x" 0))))
+    let fTy = Cnstr (Pi s l "x" a outL)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking left branch has type" <++> pretty fTy) tm
+    f <- check ctx f fTy (s ~> l)
+    inScope "infer" $ trace $ map (\_ => "left branch is well typed") tm
+    outR <- doApp (weaken 1 out) (Cnstr (Right (Ntrl (Var "x" 0))))
+    let gTy = Cnstr (Pi s' l "x" b outR)
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "checking right branch has type" <++> pretty gTy) tm
+    g <- check ctx g gTy (s' ~> l)
+    inScope "infer" $ trace $ map (\_ => "right branch is well typed") tm
+    res <- doCase t f g
+    out <- doApp out t
+    inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty out) tm
+    pure (res, out, l)
   Top => pure $ (Cnstr Top, cast Prop, Set 0)
   Point => pure $ (Irrel, Cnstr Top, Prop)
   Bottom  => pure $ (Cnstr Bottom, cast Prop, Set 0)
@@ -508,7 +294,7 @@ inferType ctx a = do
 
 -- Checking Definitions and Blocks ---------------------------------------------
 
-covering partial
+partial
 checkDef : Context n -> Term.Definition n -> Logging ann (NormalForm.Definition n)
 checkDef ctx def = do
   (ty, sort) <-
@@ -519,7 +305,7 @@ checkDef ctx def = do
   inScope "check" $ debug $ map (\name => pretty {ann} "\{name} is well typed with value" <++> pretty tm) def.name
   pure $ MkDefinition {name = def.name, ty, tm, sort}
 
-covering partial
+partial
 export
 checkBlock : Block n -> Logging ann (Context n)
 checkBlock [] = pure []
diff --git a/src/Obs/Typing/Conversion.idr b/src/Obs/Typing/Conversion.idr
new file mode 100644
index 0000000..20198c5
--- /dev/null
+++ b/src/Obs/Typing/Conversion.idr
@@ -0,0 +1,70 @@
+module Obs.Typing.Conversion
+
+import Data.Fin
+
+import Obs.Logging
+import Obs.NormalForm
+import Obs.NormalForm.Normalise
+import Obs.Sort
+import Obs.Substitution
+
+-- Conversion ------------------------------------------------------------------
+
+-- invariant: all definitions fully expanded
+-- invariant: m |- t, u <- a : s
+partial export
+convert : (t, u, a : NormalForm n) -> Sort -> Logging ann Bool
+partial
+convertSet : (t, u : NormalForm n) -> Logging ann Bool
+partial
+convertSum : (t, u : NormalForm n) -> (s, s' : Sort) -> (a, b : NormalForm n) -> Logging ann Bool
+
+-- In sort Prop
+convert Irrel Irrel a Prop = pure True
+-- In unknown type in set
+convert t u (Ntrl _) (Set k) = pure $ t == u
+-- In type Set
+convert t u (Cnstr (Sort _)) (Set _) = convertSet t u
+-- In type Pi
+convert t u (Cnstr (Pi s s' var a b)) (Set k) = do
+  t <- doApp (weaken 1 t) (Ntrl $ Var var FZ)
+  u <- doApp (weaken 1 u) (Ntrl $ Var var FZ)
+  convert t u b s'
+-- In type Sigma
+convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do
+  t1 <- doFst t
+  u1 <- doFst t
+  True <- convert t1 u1 a s
+    | False => pure False
+  b <- subst1 t1 b
+  t2 <- doSnd t
+  u2 <- doSnd t
+  convert t2 u2 b s'
+-- In type Sum (manually expanding definition of doCase)
+convert t u (Cnstr (Sum s s' a b)) (Set _) = convertSum t u s s' a b
+-- Default
+convert t u a s =
+  inScope "invalid conversion" $ fatal $
+  fillSep {ann} [prettyPrec App t, prettyPrec App u, prettyPrec App a, prettyPrec App s]
+
+convertSet (Cnstr (Sort s')) (Cnstr (Sort s'')) = pure $ s' == s''
+convertSet (Cnstr (Pi s s' _ a b)) (Cnstr (Pi l l' _ a' b')) =
+  pure $
+  s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
+convertSet (Cnstr (Sigma s s' _ a b)) (Cnstr (Sigma l l' _ a' b')) =
+  pure $
+  s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
+convertSet (Cnstr (Sum s s' a b)) (Cnstr (Sum l l' a' b')) =
+  pure $
+  s == l && s' == l' && !(convertSet a a') && !(convertSet b b')
+convertSet (Cnstr Top) (Cnstr Top) = pure True
+convertSet (Cnstr Bottom) (Cnstr Bottom) = pure True
+convertSet (Ntrl t) u = pure (Ntrl t == u)
+convertSet t (Ntrl u) = pure (t == Ntrl u)
+convertSet t u = pure $ False
+
+convertSum (Cnstr (Left t)) (Cnstr (Left u)) s s' a b = convert t u a s
+convertSum (Cnstr (Right t)) (Cnstr (Right u)) s s' a b = convert t u b s'
+convertSum (Ntrl t) u s s' a b = pure (Ntrl t == u)
+convertSum t (Ntrl u) s s' a b = pure (t == Ntrl u)
+convertSum t u s s' a b = pure False