Add equality types and casts.

6 files changed, 437 insertions, 29 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index ef90cb8..9215dda 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -57,6 +57,28 @@ abstractSyntax ctx (Absurd bounds a t) = do
   a <- abstractSyntax ctx a
   t <- abstractSyntax ctx t
   pure (Absurd bounds a t)
+abstractSyntax ctx (Equal bounds t u) = do
+  t <- abstractSyntax ctx t
+  u <- abstractSyntax ctx u
+  pure (Equal bounds t u)
+abstractSyntax ctx (Refl bounds t) = do
+  t <- abstractSyntax ctx t
+  pure (Refl bounds t)
+abstractSyntax ctx (Transp bounds t b u t' e) = do
+  t <- abstractSyntax ctx t
+  b <- abstractSyntax ctx b
+  u <- abstractSyntax ctx u
+  t' <- abstractSyntax ctx t'
+  e <- abstractSyntax ctx e
+  pure (Transp bounds t b u t' e)
+abstractSyntax ctx (Cast bounds b e t) = do
+  b <- abstractSyntax ctx b
+  e <- abstractSyntax ctx e
+  t <- abstractSyntax ctx t
+  pure (Cast bounds b e t)
+abstractSyntax ctx (CastId bounds t) = do
+  t <- abstractSyntax ctx t
+  pure (CastId bounds t)
 
 abstractDefinition : Context n -> Definition -> Logging ann (Definition n)
 abstractDefinition ctx def = pure $ MkDefinition
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index 4b4fded..2caf733 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -32,6 +32,13 @@ data Neutral : Nat -> Type where
   Fst    : Neutral n -> Neutral n
   Snd    : Neutral n -> Neutral n
   Absurd : Neutral n
+  Equal  : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
+  EqualL : Nat -> Neutral n -> NormalForm n -> Neutral n
+  EqualR : Nat -> Constructor n -> Neutral n -> Neutral n
+  EqualU : Nat -> Constructor n -> Constructor n -> Neutral n
+  CastL  : Neutral n -> NormalForm n -> NormalForm n -> Neutral n
+  CastR  : Constructor n -> Neutral n -> NormalForm n -> Neutral n
+  CastU  : Constructor n -> Constructor n -> NormalForm n -> Neutral n
 
 public export
 data NormalForm : Nat -> Type where
@@ -73,6 +80,13 @@ 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 Absurd Absurd = True
+eqNtrl (Equal a t u) (Equal a' t' u') = eqNtrl a a' && eqWhnf t t' && eqWhnf u u'
+eqNtrl (EqualL i t u) (EqualL j t' u') = i == j && eqNtrl t t' && eqWhnf u u'
+eqNtrl (EqualR i t u) (EqualR j t' u') = i == j && eqCnstr t t' && eqNtrl u u'
+eqNtrl (EqualU i t u) (EqualU j t' u') = i == j && eqCnstr t t' && eqCnstr u u'
+eqNtrl (CastL a b t) (CastL a' b' t') = eqNtrl a a' && eqWhnf b b' && eqWhnf t t'
+eqNtrl (CastR a b t) (CastR a' b' t') = eqCnstr a a' && eqNtrl b b' && eqWhnf t t'
+eqNtrl (CastU a b t) (CastU a' b' t') = eqCnstr a a' && eqCnstr b b' && eqWhnf t t'
 eqNtrl _ _ = False
 
 eqWhnf (Ntrl t)  (Ntrl u)  = eqNtrl t u
@@ -146,6 +160,34 @@ prettyPrecNtrl d (Snd t) =
   group $
   fillSep [pretty "snd", prettyPrecNtrl App t]
 prettyPrecNtrl d Absurd = pretty "absurd"
+prettyPrecNtrl d (Equal _ t u) =
+  parenthesise (d >= Equal) $
+  group $
+  prettyPrecWhnf Equal t <++> pretty "~" <+> softline <+> prettyPrecWhnf Equal u
+prettyPrecNtrl d (EqualL _ t u) =
+  parenthesise (d >= Equal) $
+  group $
+  prettyPrecNtrl Equal t <++> pretty "~" <+> softline <+> prettyPrecWhnf Equal u
+prettyPrecNtrl d (EqualR _ t u) =
+  parenthesise (d >= Equal) $
+  group $
+  prettyPrecCnstr Equal t <++> pretty "~" <+> softline <+> prettyPrecNtrl Equal u
+prettyPrecNtrl d (EqualU _ t u) =
+  parenthesise (d >= Equal) $
+  group $
+  prettyPrecCnstr Equal t <++> pretty "~" <+> softline <+> prettyPrecCnstr Equal u
+prettyPrecNtrl d (CastL a b t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "cast", prettyPrecNtrl App a, prettyPrecWhnf App b, prettyPrecWhnf App t]
+prettyPrecNtrl d (CastR a b t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "cast", prettyPrecCnstr App a, prettyPrecNtrl App b, prettyPrecWhnf App t]
+prettyPrecNtrl d (CastU a b t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "cast", prettyPrecCnstr App a, prettyPrecCnstr App b, prettyPrecWhnf App t]
 
 prettyPrecWhnf d (Ntrl t)  = prettyPrecNtrl d t
 prettyPrecWhnf d (Cnstr t) = prettyPrecCnstr d t
@@ -196,6 +238,13 @@ 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 Absurd f = Absurd
+renameNtrl (Equal a t u) f = Equal (renameNtrl a f) (renameWhnf t f) (renameWhnf u f)
+renameNtrl (EqualL i t u) f = EqualL i (renameNtrl t f) (renameWhnf u f)
+renameNtrl (EqualR i t u) f = EqualR i (renameCnstr t f) (renameNtrl u f)
+renameNtrl (EqualU i t u) f = EqualU i (renameCnstr t f) (renameCnstr u f)
+renameNtrl (CastL a b t) f = CastL (renameNtrl a f) (renameWhnf b f) (renameWhnf t f)
+renameNtrl (CastR a b t) f = CastR (renameCnstr a f) (renameNtrl b f) (renameWhnf t f)
+renameNtrl (CastU a b t) f = CastU (renameCnstr a f) (renameCnstr b f) (renameWhnf t f)
 
 renameWhnf (Ntrl t)  f = Ntrl $ renameNtrl t f
 renameWhnf (Cnstr t) f = Cnstr $ renameCnstr t f
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index efe7857..95d8e96 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -27,6 +27,10 @@ data ObsTokenKind
   | OTPoint
   | OTVoid
   | OTAbsurd
+  | OTRefl
+  | OTTransp
+  | OTCast
+  | OTCastRefl
   -- Special symbols
   | OTUnit
   -- Grouping symbols
@@ -40,6 +44,7 @@ data ObsTokenKind
   | OTFatArrow
   | OTProduct
   | OTComma
+  | OTTilde
   | OTEqual
   | OTColon
 
@@ -55,6 +60,10 @@ Eq ObsTokenKind where
   OTPoint == OTPoint = True
   OTVoid == OTVoid = True
   OTAbsurd == OTAbsurd = True
+  OTRefl == OTRefl = True
+  OTTransp == OTTransp = True
+  OTCast == OTCast = True
+  OTCastRefl == OTCastRefl = True
   OTUnit == OTUnit = True
   OTPOpen == OTPOpen = True
   OTPClose == OTPClose = True
@@ -65,6 +74,7 @@ Eq ObsTokenKind where
   OTFatArrow == OTFatArrow = True
   OTProduct == OTProduct = True
   OTComma == OTComma = True
+  OTTilde == OTTilde = True
   OTEqual == OTEqual = True
   OTColon == OTColon = True
   _ == _ = False
@@ -85,6 +95,10 @@ TokenKind ObsTokenKind where
   tokValue OTPoint s = ()
   tokValue OTVoid s = ()
   tokValue OTAbsurd s = ()
+  tokValue OTRefl s = ()
+  tokValue OTTransp s = ()
+  tokValue OTCast s = ()
+  tokValue OTCastRefl s = ()
   tokValue OTUnit s = ()
   tokValue OTPOpen s = ()
   tokValue OTPClose s = ()
@@ -95,6 +109,7 @@ TokenKind ObsTokenKind where
   tokValue OTFatArrow s = ()
   tokValue OTProduct s = ()
   tokValue OTComma s = ()
+  tokValue OTTilde s = ()
   tokValue OTEqual s = ()
   tokValue OTColon s = ()
 
@@ -117,6 +132,10 @@ keywords =
   , ("tt", OTPoint)
   , ("Void", OTVoid)
   , ("absurd", OTAbsurd)
+  , ("refl", OTRefl)
+  , ("transp", OTTransp)
+  , ("cast", OTCast)
+  , ("castRefl", OTCastRefl)
   ]
 
 obsTokenMap : TokenMap ObsToken
@@ -136,16 +155,20 @@ obsTokenMap = toTokenMap [(newline, OTNewline), (spaces, OTIgnore)] ++
   , (exact "\\", OTBackslash)
   , (exact "**", OTProduct)
   , (exact ",", OTComma)
+  , (exact "~", OTTilde)
   , (exact "=", OTEqual)
   , (exact ":", OTColon)
   ]
 
+newlines : Grammar state ObsToken False ()
+newlines = map (\_ => ()) $ many (match OTNewline)
+
 parens : {c : _} -> Grammar state ObsToken c a -> Grammar state ObsToken True a
 parens g =
   match OTPOpen *>
-  many (match OTNewline) *>
+  newlines *>
   g <*
-  many (match OTNewline) <*
+  newlines <*
   match OTPClose
 
 ident : Grammar state ObsToken True (WithBounds String)
@@ -192,7 +215,7 @@ set = do
 
 lambda : Grammar state ObsToken True (Syntax -> Syntax)
 lambda = do
-  name <- bounds $ match OTBackslash *> commit *> ident <* match OTFatArrow
+  name <- bounds $ match OTBackslash *> commit *> ident <* newlines <* match OTFatArrow <* newlines
   pure (Lambda name.bounds name.val)
 
 projFst : Grammar state ObsToken True (Syntax -> Syntax)
@@ -210,6 +233,26 @@ botElim = do
   absurd <- bounds $ match OTAbsurd <* commit
   pure (Absurd absurd.bounds)
 
+refl : Grammar state ObsToken True (Syntax -> Syntax)
+refl = do
+  refl <- bounds $ match OTRefl <* commit
+  pure (Refl refl.bounds)
+
+transp : Grammar state ObsToken True (Syntax -> Syntax -> Syntax -> Syntax -> Syntax -> Syntax)
+transp = do
+  transp <- bounds $ match OTTransp <* commit
+  pure (Transp transp.bounds)
+
+cast : Grammar state ObsToken True (Syntax -> Syntax -> Syntax -> Syntax)
+cast = do
+  cast <- bounds $ match OTCast <* commit
+  pure (Cast cast.bounds)
+
+castRefl : Grammar state ObsToken True (Syntax -> Syntax)
+castRefl = do
+  castRefl <- bounds $ match OTCastRefl <* commit
+  pure (CastId castRefl.bounds)
+
 -- NOTE: these functions are all total.
 partial
 pi : WithBounds (WithBounds String, Syntax) -> Grammar state ObsToken True (Syntax -> Syntax)
@@ -222,6 +265,8 @@ term : Grammar state ObsToken True Syntax
 partial
 precGteApp : Grammar state ObsToken True Syntax
 partial
+precGteEqual : Grammar state ObsToken True Syntax
+partial
 exp' : Grammar state ObsToken True Syntax
 partial
 exp : Grammar state ObsToken True Syntax
@@ -229,22 +274,33 @@ partial
 decl : Grammar state ObsToken True (WithBounds String, Syntax)
 
 pi decl = do
-  _ <- match OTThinArrow <* commit
+  _ <- match OTThinArrow <* commit <* newlines
   Parser.Core.pure (uncurry (Pi decl.bounds) decl.val)
 
 sigma decl = do
-  _ <- match OTProduct <* commit
+  _ <- match OTProduct <* commit <* newlines
   Parser.Core.pure (uncurry (Sigma decl.bounds) decl.val)
 
 pair fst snd = do
-  pair <- bounds $ [| MkPair (match OTAOpen *> fst <* match OTComma) (snd <* match OTAClose) |]
+  pair <- bounds $ [| MkPair (match OTAOpen *> fst <* newlines <* match OTComma <* newlines) (snd <* newlines <* match OTAClose) |]
   pure (uncurry (Pair pair.bounds) pair.val)
 
 term = atomic <|> pair exp exp <|> parens exp
 precGteApp = atomicNoSet <|> set <|> pair exp exp <|> parens exp
-exp' = precGteApp <|> (projFst <*> term) <|> (projSnd <*> term) <|> (botElim <*> term <*> term)
+precGteEqual =
+  map (\ty => let (t, t') = ty.val in maybe t (Equal ty.bounds t) t') $
+  bounds [| MkPair precGteApp (optional (newlines *> match OTTilde *> commit *> newlines *> precGteApp)) |]
+exp' =
+  precGteEqual <|>
+  (projFst <*> term) <|>
+  (projSnd <*> term) <|>
+  (botElim <*> term <*> term) <|>
+  (refl <*> term) <|>
+  (transp <*> term <*> term <*> term <*> term <*> term) <|>
+  (Parser.cast <*> term <*> term <*> term) <|>
+  (castRefl <*> term)
 exp =
-  (bounds (parens decl) >>= (\decl => (pi decl <|> sigma decl) <*> exp)) <|>
+  (bounds (parens decl) <* many (match OTNewline) >>= (\decl => (pi decl <|> sigma decl) <*> exp)) <|>
   (lambda <*> exp) <|>
   (map (\(t, ts) => foldl1 App (t :: ts)) [| MkPair exp' (many term) |])
 decl = [| MkPair ident (match OTColon *> commit *> exp) |]
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index f1a552f..bcc0cb4 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -29,6 +29,12 @@ data Syntax : Type where
   -- False
   Bottom : Bounds -> Syntax
   Absurd : Bounds -> Syntax -> Syntax -> Syntax
+  -- Equality
+  Equal  : Bounds -> Syntax -> Syntax -> Syntax
+  Refl   : Bounds -> Syntax -> Syntax
+  Transp : Bounds -> Syntax -> Syntax -> Syntax -> Syntax -> Syntax -> Syntax
+  Cast   : Bounds -> Syntax -> Syntax -> Syntax -> Syntax
+  CastId : Bounds -> Syntax -> Syntax
 
 public export
 record Definition where
@@ -85,6 +91,33 @@ Pretty Syntax where
     parenthesise (d >= App) $
     group $
     fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
+  prettyPrec d (Equal _ t u) =
+    parenthesise (d >= Equal) $
+    group $
+    prettyPrec Equal t <++> pretty "~" <+> softline <+> prettyPrec Equal u
+  prettyPrec d (Refl _ t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "refl", prettyPrec App t]
+  prettyPrec d (Transp _ t b u t' e) =
+    parenthesise (d >= App) $
+    group $
+    fillSep $
+    [ pretty "transp"
+    , prettyPrec App t
+    , prettyPrec App b
+    , prettyPrec App u
+    , prettyPrec App t'
+    , prettyPrec App e
+    ]
+  prettyPrec d (Cast _ b e t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "cast", prettyPrec App b, prettyPrec App e, prettyPrec App t]
+  prettyPrec d (CastId _ t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "castRefl", prettyPrec App t]
 
 export
 Pretty Definition where
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 9221dbd..578bf83 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -30,6 +30,12 @@ data Term : Nat -> Type where
   -- False
   Bottom : Bounds -> Term n
   Absurd : Bounds -> Term n -> Term n -> Term n
+  -- Equality
+  Equal  : Bounds -> Term n -> Term n -> Term n
+  Refl   : Bounds -> Term n -> Term n
+  Transp : Bounds -> Term n -> Term n -> Term n -> Term n -> Term n -> Term n
+  Cast   : Bounds -> Term n -> Term n -> Term n -> Term n
+  CastId : Bounds -> Term n -> Term n
 
 public export
 record Definition (n : Nat) where
@@ -61,6 +67,11 @@ fullBounds tm@(Top x) = MkBounded tm False x
 fullBounds tm@(Point x) = MkBounded tm False x
 fullBounds tm@(Bottom x) = MkBounded tm False x
 fullBounds tm@(Absurd x a t) = mergeBounds (mergeBounds (fullBounds a) (fullBounds t)) (MkBounded tm False x)
+fullBounds tm@(Equal x t u) = mergeBounds (mergeBounds (fullBounds t) (fullBounds u)) (MkBounded tm False x)
+fullBounds tm@(Refl x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
+fullBounds tm@(Transp x t b u t' e) = mergeBounds (mergeBounds (mergeBounds (fullBounds t) (fullBounds b)) (mergeBounds (fullBounds u) (fullBounds t'))) (mergeBounds (fullBounds e) (MkBounded tm False x))
+fullBounds tm@(Cast x b e t) = mergeBounds (mergeBounds (fullBounds b) (fullBounds e)) (mergeBounds (fullBounds t) (MkBounded tm False x))
+fullBounds tm@(CastId x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
 
 -- Pretty Print ----------------------------------------------------------------
 
@@ -109,6 +120,33 @@ Pretty (Term n) where
     parenthesise (d > Open) $
     group $
     fillSep [pretty "absurd", prettyPrec App a, prettyPrec App t]
+  prettyPrec d (Equal _ t u) =
+    parenthesise (d >= Equal) $
+    group $
+    prettyPrec Equal t <++> pretty "~" <+> softline <+> prettyPrec Equal u
+  prettyPrec d (Refl _ t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "refl", prettyPrec App t]
+  prettyPrec d (Transp _ t b u t' e) =
+    parenthesise (d >= App) $
+    group $
+    fillSep $
+    [ pretty "transp"
+    , prettyPrec App t
+    , prettyPrec App b
+    , prettyPrec App u
+    , prettyPrec App t'
+    , prettyPrec App e
+    ]
+  prettyPrec d (Cast _ b e t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "cast", prettyPrec App b, prettyPrec App e, prettyPrec App t]
+  prettyPrec d (CastId _ t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "castRefl", prettyPrec App t]
 
 export
 Pretty (Definition n) where
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index bf7ebc1..834dbb7 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -36,6 +36,11 @@ 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 =
@@ -51,11 +56,27 @@ substNtrl  : Neutral n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (
 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
@@ -77,9 +98,9 @@ substCnstr Top f = pure $ Top
 substCnstr Bottom  f = pure $ Bottom
 
 substNtrl (Var var i) f = do
-  Ntrl (Var "" j) <- f i
+  Ntrl (Var var' j) <- f i
     | t => pure t
-  pure (Ntrl (Var var j))
+  pure (Ntrl (Var (mergeName var' var) j))
 substNtrl (App t u) f = do
   t <- substNtrl t f
   u <- subst u f
@@ -91,29 +112,148 @@ 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 "wrong constructor in apply:" $ fatal t
+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 "wrong constructor in fst:" $ fatal 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 "wrong constructor in snd:" $ fatal t
+doSnd (Cnstr t) = inScope "bug" $ inScope "wrong constructor in snd" $ fatal t
 
-partial
-subst1 : NormalForm n -> NormalForm (S n) -> Logging ann (NormalForm n)
-subst1 t u = subst u (add (Logging ann . NormalForm) (pure t) (pure . point))
+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 ------------------------------------------------------------------
 
@@ -155,7 +295,7 @@ convert t u (Cnstr (Sigma s s' var a b)) (Set k) = do
   convert t2 u2 b s'
 -- Default
 convert t u a s =
-  inScope "invalid conversion:" $ fatal $
+  inScope "invalid conversion" $ fatal $
   fillSep {ann} [prettyPrec App t, prettyPrec App u, prettyPrec App a, prettyPrec App s]
 
 
@@ -178,17 +318,19 @@ countVars (ctx :< y)  = weaken $ countVars ctx
 countVars (ctx ::< y) = FS $ countVars ctx
 
 index : TyContext m n -> Fin n -> (NormalForm n, NormalForm n, Sort)
-index (ctx :< def)           FZ     = (weaken 1 def.tm, weaken 1 def.ty, def.sort)
-index (ctx ::< (var, ty, 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
+index (ctx :< def)              FZ     = (weaken 1 def.tm, weaken 1 def.ty, def.sort)
+index (ctx ::< (var, ty, Prop)) FZ     = (Irrel, weaken 1 ty, Prop)
+index (ctx ::< (var, ty, s))    FZ     = (Ntrl $ Var var FZ, weaken 1 ty, s)
+index (ctx :< _)                (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
+index (ctx ::< _)               (FS i) = bimap (weaken 1) (mapFst (weaken 1)) $ index ctx i
 
 covering partial
 asSubst : (ctx : TyContext m n) -> Fin n -> Logging ann (NormalForm m)
-asSubst (ctx :< def)           FZ     = subst def.tm (asSubst ctx)
-asSubst (ctx ::< (var, _, _))  FZ     = pure $ Ntrl $ Var var FZ
-asSubst (ctx :< def)           (FS i) = asSubst ctx i
-asSubst (ctx ::< _)            (FS i) = map (weaken 1) (asSubst ctx i)
+asSubst (ctx :< def)             FZ     = subst def.tm (asSubst ctx)
+asSubst (ctx ::< (var, _, Prop)) FZ     = pure Irrel
+asSubst (ctx ::< (var, _, _))    FZ     = pure $ Ntrl (Var var FZ)
+asSubst (ctx :< def)             (FS i) = asSubst ctx i
+asSubst (ctx ::< _)              (FS i) = map (weaken 1) (asSubst ctx i)
 
 -- Checking and Inference ------------------------------------------------------
 
@@ -205,7 +347,9 @@ check ctx tm@(Lambda _ _ t) (Cnstr (Pi s s' var a b)) _ = do
   inScope "check" $ trace $ map (\_ => "binding new variable to \{var}") (fullBounds tm)
   inScope "check" $ trace $ map (\_ => pretty {ann} "checking for type" <++> pretty b) (fullBounds tm)
   t <- check (ctx ::< (var, a, s)) t b s'
-  pure (Cnstr $ Lambda var t)
+  case s' of
+    Prop => pure Irrel
+    _ => pure (Cnstr $ Lambda var t)
 check ctx tm@(Lambda _ _ _) ty _ = typeMismatch (fullBounds tm).bounds (pretty "pi") (pretty ty)
 check ctx tm@(Pair _ t u) (Cnstr (Sigma s s' var a b)) _ = do
   inScope "check" $ trace $ map (\_ => "checking pair") (fullBounds tm)
@@ -215,7 +359,10 @@ check ctx tm@(Pair _ t u) (Cnstr (Sigma s s' var a b)) _ = do
   inScope "check" $ trace $ map (\_ => pretty {ann} "checking second for type" <++> pretty b) (fullBounds tm)
   u <- check ctx u b s'
   inScope "check" $ trace $ map (\_ => pretty {ann} "pair is well typed") (fullBounds tm)
-  pure (Cnstr $ Pair t u)
+  case (s, s') of
+    (Prop, Prop) => pure Irrel
+    _ => pure (Cnstr $ Pair t u)
+check ctx tm@(Pair _ _ _) ty _ = typeMismatch (fullBounds tm).bounds (pretty "sigma") (pretty ty)
 check ctx tm ty s = do
   let bounded = fullBounds tm
   inScope "check" $ trace $ map (\_ => "checking has fallen through") bounded
@@ -232,8 +379,8 @@ infer ctx tm@(Var b i) = do
   inScope "infer" $ trace $ map (\_ => "encountered variable \{b.val}@\{show i}") (fullBounds tm)
   let (t, a, s) = index ctx i
   inScope "infer" $ trace $ map (\_ => pretty {ann} "variable has type" <++> pretty a) (fullBounds tm)
-  pure $ (t, a, s)
-infer ctx (Sort b s) = pure $ (cast s, cast (suc s), suc (suc s))
+  pure (t, a, s)
+infer ctx (Sort b s) = pure (cast s, cast (suc s), suc (suc s))
 infer ctx tm@(Pi _ var a b) = do
   inScope "infer" $ trace $ map (\_ => "encountered Pi type") (fullBounds tm)
   (a, s) <- inferType ctx a
@@ -262,6 +409,7 @@ infer ctx tm@(Sigma _ var a b) = do
   (b, s') <- inferType (ctx ::< (var, a, s)) b
   inScope "infer" $ trace $ map (\_ => pretty {ann} "second has type" <++> pretty b <+> comma <+> softline <+> pretty "so Sigma type has type" <++> pretty (lub s s')) (fullBounds tm)
   pure (Cnstr (Sigma s s' var a b), cast (lub s s'), suc (lub s s'))
+infer ctx tm@(Pair _ _ _) = inScope "cannot infer type" $ fatal (fullBounds tm)
 infer ctx tm@(Fst _ t) = do
   inScope "infer" $ trace $ map (\_ => "encountered first projection") (fullBounds tm)
   let bounded = fullBounds t
@@ -293,6 +441,68 @@ infer ctx tm@(Absurd b a t) = do
   _ <- check ctx t (Cnstr Bottom) Prop
   inScope "infer" $ trace $ map (\_ => "proof of false is well typed") (fullBounds tm)
   pure (Ntrl Absurd, a, s)
+infer ctx tm@(Equal b t u) = do
+  inScope "infer" $ trace $ map (\_ => "encountered equal") (fullBounds tm)
+  (t, a, s) <- infer ctx t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "lhs has type" <++> pretty a) (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => "checking rhs has same type") (fullBounds tm)
+  u <- check ctx u a s
+  inScope "infer" $ trace $ map (\_ => "rhs is well typed") (fullBounds tm)
+  res <- doEqual a t u
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "equality computes to" <++> pretty res) (fullBounds tm)
+  pure (res, cast Prop, Set 0)
+infer ctx tm@(Refl b t) = do
+  inScope "infer" $ trace $ map (\_ => "encountered refl") (fullBounds tm)
+  (t, a, s) <- infer ctx t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "term has type" <++> pretty a) (fullBounds tm)
+  ty <- doEqual a t t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "equality computes to" <++> pretty ty) (fullBounds tm)
+  pure (Irrel, ty, Prop)
+infer ctx tm@(Transp _ t b u t' e) = do
+  inScope "infer" $ trace $ map (\_ => "encountered transp") (fullBounds tm)
+  (t, a, s) <- infer ctx t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "start index has type" <++> pretty a) (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => "checking end index has same type") (fullBounds tm)
+  t' <- check ctx t' a s
+  inScope "infer" $ trace $ map (\_ => "end index is well typed") (fullBounds tm)
+  let bounded = fullBounds b
+  let ty = Cnstr (Pi s (Set 0) "_" a (cast Prop))
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "checkout output is in" <++> pretty ty) (fullBounds tm)
+  b <- check ctx b ty s
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "output is well typed") (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => "checking equality type") (fullBounds tm)
+  eq <- doEqual a t t'
+  _ <- check ctx e eq Prop
+  inScope "infer" $ trace $ map (\_ => "equality is well typed") (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => "checking transformed value") (fullBounds tm)
+  inTy <- doApp b t
+  _ <- check ctx u inTy Prop
+  inScope "infer" $ trace $ map (\_ => "transformed value is well typed") (fullBounds tm)
+  outTy <- doApp b t'
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "producing value of type" <++> pretty outTy) (fullBounds tm)
+  pure (Irrel, outTy, Prop)
+infer ctx tm@(Cast _ b e t) = do
+  inScope "infer" $ trace $ map (\_ => "encountered cast") (fullBounds tm)
+  (t, a, s) <- infer ctx t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "input has type" <++> pretty a) (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => "checking output has same sort") (fullBounds tm)
+  b <- check ctx b (cast s) (suc s)
+  inScope "infer" $ trace $ map (\_ => "output is well sorted") (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => "checking equality type") (fullBounds tm)
+  eq <- doEqual (cast s) a b
+  _ <- check ctx e eq Prop
+  inScope "infer" $ trace $ map (\_ => "equality is well typed") (fullBounds tm)
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "producing value of type" <++> pretty b) (fullBounds tm)
+  res <- doCastL a b t
+  pure (res, b, s)
+infer ctx tm@(CastId _ t) = do
+  inScope "infer" $ trace $ map (\_ => "encountered cast identity proof") (fullBounds tm)
+  (t, a, s) <- infer ctx t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "term has type" <++> pretty a) (fullBounds tm)
+  cast <- doCastL a a t
+  eq <- doEqual a cast t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "producing equality type" <++> pretty eq) (fullBounds tm)
+  pure (Irrel, eq, Prop)
 
 inferType ctx a = do
   (a, Cnstr (Sort s), _) <- infer ctx a