Add dependent sums.

6 files changed, 235 insertions, 15 deletions

diff --git a/src/Obs/Abstract.idr b/src/Obs/Abstract.idr
index 90616d4..ef90cb8 100644
--- a/src/Obs/Abstract.idr
+++ b/src/Obs/Abstract.idr
@@ -36,6 +36,20 @@ abstractSyntax ctx (App t u) = do
   t <- abstractSyntax ctx t
   u <- abstractSyntax ctx u
   pure (App t u)
+abstractSyntax ctx (Sigma bounds var a b) = do
+  a <- abstractSyntax ctx a
+  b <- abstractSyntax (bind ctx var.val) b
+  pure (Sigma bounds var.val a b)
+abstractSyntax ctx (Pair b t u) = do
+  t <- abstractSyntax ctx t
+  u <- abstractSyntax ctx u
+  pure (Pair b t u)
+abstractSyntax ctx (Fst b t) = do
+  t <- abstractSyntax ctx t
+  pure (Fst b t)
+abstractSyntax ctx (Snd b t) = do
+  t <- abstractSyntax ctx t
+  pure (Snd b t)
 abstractSyntax ctx (Top b) = pure (Top b)
 abstractSyntax ctx (Point b) = pure (Point b)
 abstractSyntax ctx (Bottom b) = pure (Bottom b)
diff --git a/src/Obs/NormalForm.idr b/src/Obs/NormalForm.idr
index a15c3c1..4b4fded 100644
--- a/src/Obs/NormalForm.idr
+++ b/src/Obs/NormalForm.idr
@@ -20,6 +20,8 @@ data Constructor : Nat -> Type where
   Sort   : Sort -> Constructor n
   Pi     : Sort -> Sort -> String -> NormalForm n -> NormalForm (S n) -> Constructor n
   Lambda : String -> NormalForm (S n) -> Constructor n
+  Sigma  : Sort -> Sort -> String -> NormalForm n -> NormalForm (S n) -> Constructor n
+  Pair   : NormalForm n -> NormalForm n -> Constructor n
   Top    : Constructor n
   Bottom : Constructor n
 
@@ -27,6 +29,8 @@ public export
 data Neutral : Nat -> Type where
   Var    : String -> Fin n -> Neutral n
   App    : Neutral n -> NormalForm n -> Neutral n
+  Fst    : Neutral n -> Neutral n
+  Snd    : Neutral n -> Neutral n
   Absurd : Neutral n
 
 public export
@@ -58,12 +62,16 @@ eqWhnf  : NormalForm n -> NormalForm n -> Bool
 eqCnstr (Sort s) (Sort s') = s == s'
 eqCnstr (Pi s s' _ a b) (Pi l l' _ a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
 eqCnstr (Lambda _ t) (Lambda _ u) = eqWhnf t u
+eqCnstr (Sigma s s' _ a b) (Sigma l l' _ a' b') = s == l && s' == l' && eqWhnf a a' && eqWhnf b b'
+eqCnstr (Pair t u) (Pair t' u') = eqWhnf t t' && eqWhnf u u'
 eqCnstr Top Top = True
 eqCnstr Bottom Bottom = True
 eqCnstr _ _ = False
 
 eqNtrl (Var _ i) (Var _ j) = i == j
 eqNtrl (App t u) (App t' u') = eqNtrl t t' && eqWhnf u u'
+eqNtrl (Fst t) (Fst t') = eqNtrl t t'
+eqNtrl (Snd t) (Snd t') = eqNtrl t t'
 eqNtrl Absurd Absurd = True
 eqNtrl _ _ = False
 
@@ -111,6 +119,16 @@ prettyPrecCnstr d (Lambda var t) =
   backslash <+> pretty var <++>
   pretty "=>" <+> softline <+>
   prettyPrecWhnf Open t
+prettyPrecCnstr d (Sigma _ _ var a b) =
+  parenthesise (d > Open) $
+  group $
+  parens (pretty var <++> colon <+> softline <+> prettyPrecWhnf Open a) <++>
+  pretty "**" <+> softline <+>
+  prettyPrecWhnf Open b
+prettyPrecCnstr d (Pair t u) =
+  angles $
+  group $
+  neutral <++> prettyPrecWhnf Open t <+> comma <+> softline <+> prettyPrecWhnf Open u <++> neutral
 prettyPrecCnstr d Top = pretty "()"
 prettyPrecCnstr d Bottom = pretty "Void"
 
@@ -119,6 +137,14 @@ prettyPrecNtrl d (App t u) =
   parenthesise (d >= App) $
   group $
   fillSep [prettyPrecNtrl Open t, prettyPrecWhnf App u]
+prettyPrecNtrl d (Fst t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "fst", prettyPrecNtrl App t]
+prettyPrecNtrl d (Snd t) =
+  parenthesise (d >= App) $
+  group $
+  fillSep [pretty "snd", prettyPrecNtrl App t]
 prettyPrecNtrl d Absurd = pretty "absurd"
 
 prettyPrecWhnf d (Ntrl t)  = prettyPrecNtrl d t
@@ -160,11 +186,15 @@ renameWhnf  : NormalForm n -> (Fin n -> Fin m) -> NormalForm m
 renameCnstr (Sort s) f = Sort s
 renameCnstr (Pi s s' var a b) f = Pi s s' var (renameWhnf a f) (renameWhnf b $ lift 1 f)
 renameCnstr (Lambda var t) f = Lambda var (renameWhnf t $ lift 1 f)
+renameCnstr (Sigma s s' var a b) f = Sigma s s' var (renameWhnf a f) (renameWhnf b $ lift 1 f)
+renameCnstr (Pair t u) f = Pair (renameWhnf t f) (renameWhnf u f)
 renameCnstr Top f = Top
 renameCnstr Bottom f = Bottom
 
 renameNtrl (Var var i) f = Var var (f i)
 renameNtrl (App t u) f = App (renameNtrl t f) (renameWhnf u f)
+renameNtrl (Fst t) f = Fst (renameNtrl t f)
+renameNtrl (Snd t) f = Snd (renameNtrl t f)
 renameNtrl Absurd f = Absurd
 
 renameWhnf (Ntrl t)  f = Ntrl $ renameNtrl t f
diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index f9daa62..efe7857 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -22,18 +22,24 @@ data ObsTokenKind
   | OTProp
   | OTSet
   | OTNat
+  | OTFst
+  | OTSnd
+  | OTPoint
   | OTVoid
   | OTAbsurd
   -- Special symbols
   | OTUnit
-  | OTPoint
   -- Grouping symbols
   | OTPOpen
   | OTPClose
+  | OTAOpen
+  | OTAClose
   -- Definition characters
   | OTBackslash
   | OTThinArrow
   | OTFatArrow
+  | OTProduct
+  | OTComma
   | OTEqual
   | OTColon
 
@@ -44,15 +50,21 @@ Eq ObsTokenKind where
   OTProp == OTProp = True
   OTSet == OTSet = True
   OTNat == OTNat = True
-  OTUnit == OTUnit = True
+  OTFst == OTFst = True
+  OTSnd == OTSnd = True
   OTPoint == OTPoint = True
   OTVoid == OTVoid = True
   OTAbsurd == OTAbsurd = True
+  OTUnit == OTUnit = True
   OTPOpen == OTPOpen = True
   OTPClose == OTPClose = True
+  OTAOpen == OTAOpen = True
+  OTAClose == OTAClose = True
   OTBackslash == OTBackslash = True
   OTThinArrow == OTThinArrow = True
   OTFatArrow == OTFatArrow = True
+  OTProduct == OTProduct = True
+  OTComma == OTComma = True
   OTEqual == OTEqual = True
   OTColon == OTColon = True
   _ == _ = False
@@ -68,15 +80,21 @@ TokenKind ObsTokenKind where
   tokValue OTProp s = ()
   tokValue OTSet s = ()
   tokValue OTNat s = stringToNatOrZ s
-  tokValue OTUnit s = ()
+  tokValue OTFst s = ()
+  tokValue OTSnd s = ()
   tokValue OTPoint s = ()
   tokValue OTVoid s = ()
   tokValue OTAbsurd s = ()
+  tokValue OTUnit s = ()
   tokValue OTPOpen s = ()
   tokValue OTPClose s = ()
+  tokValue OTAOpen s = ()
+  tokValue OTAClose s = ()
   tokValue OTBackslash s = ()
   tokValue OTThinArrow s = ()
   tokValue OTFatArrow s = ()
+  tokValue OTProduct s = ()
+  tokValue OTComma s = ()
   tokValue OTEqual s = ()
   tokValue OTColon s = ()
 
@@ -94,6 +112,9 @@ keywords : List (String, ObsTokenKind)
 keywords =
   [ ("Set", OTSet)
   , ("Prop", OTProp)
+  , ("fst", OTFst)
+  , ("snd", OTSnd)
+  , ("tt", OTPoint)
   , ("Void", OTVoid)
   , ("absurd", OTAbsurd)
   ]
@@ -106,12 +127,15 @@ obsTokenMap = toTokenMap [(newline, OTNewline), (spaces, OTIgnore)] ++
           Nothing => Tok OTIdent s)
   ] ++ toTokenMap
   [ (digits, OTNat)
-  , (exact "*", OTPoint)
   , (exact "(", OTPOpen)
   , (exact ")", OTPClose)
+  , (exact "<", OTAOpen)
+  , (exact ">", OTAClose)
   , (exact "=>", OTFatArrow)
   , (exact "->", OTThinArrow)
   , (exact "\\", OTBackslash)
+  , (exact "**", OTProduct)
+  , (exact ",", OTComma)
   , (exact "=", OTEqual)
   , (exact ":", OTColon)
   ]
@@ -171,6 +195,16 @@ lambda = do
   name <- bounds $ match OTBackslash *> commit *> ident <* match OTFatArrow
   pure (Lambda name.bounds name.val)
 
+projFst : Grammar state ObsToken True (Syntax -> Syntax)
+projFst = do
+  fst <- bounds $ match OTFst <* commit
+  pure (Fst fst.bounds)
+
+projSnd : Grammar state ObsToken True (Syntax -> Syntax)
+projSnd = do
+  snd <- bounds $ match OTSnd <* commit
+  pure (Snd snd.bounds)
+
 botElim : Grammar state ObsToken True (Syntax -> Syntax -> Syntax)
 botElim = do
   absurd <- bounds $ match OTAbsurd <* commit
@@ -178,7 +212,11 @@ botElim = do
 
 -- NOTE: these functions are all total.
 partial
-pi : Grammar state ObsToken True (Syntax -> Syntax)
+pi : WithBounds (WithBounds String, Syntax) -> Grammar state ObsToken True (Syntax -> Syntax)
+partial
+sigma : WithBounds (WithBounds String, Syntax) -> Grammar state ObsToken True (Syntax -> Syntax)
+partial
+pair : Grammar state ObsToken True Syntax -> Grammar state ObsToken True Syntax -> Grammar state ObsToken True Syntax
 partial
 term : Grammar state ObsToken True Syntax
 partial
@@ -190,14 +228,25 @@ exp : Grammar state ObsToken True Syntax
 partial
 decl : Grammar state ObsToken True (WithBounds String, Syntax)
 
-pi = do
-  decl <- bounds $ parens decl <* match OTThinArrow <* commit
-  pure (uncurry (Pi decl.bounds) decl.val)
-
-term = atomic <|> parens exp
-precGteApp = atomicNoSet <|> set <|> parens exp
-exp' = precGteApp <|> (botElim <*> term <*> term)
-exp = (pi <*> exp) <|> (lambda <*> exp) <|> (map (\(t, ts) => foldl1 App (t :: ts)) [| MkPair exp' (many term) |])
+pi decl = do
+  _ <- match OTThinArrow <* commit
+  Parser.Core.pure (uncurry (Pi decl.bounds) decl.val)
+
+sigma decl = do
+  _ <- match OTProduct <* commit
+  Parser.Core.pure (uncurry (Sigma decl.bounds) decl.val)
+
+pair fst snd = do
+  pair <- bounds $ [| MkPair (match OTAOpen *> fst <* match OTComma) (snd <* 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)
+exp =
+  (bounds (parens decl) >>= (\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) |]
 
 partial
diff --git a/src/Obs/Syntax.idr b/src/Obs/Syntax.idr
index 4a7ee0c..f1a552f 100644
--- a/src/Obs/Syntax.idr
+++ b/src/Obs/Syntax.idr
@@ -18,6 +18,11 @@ data Syntax : Type where
   Pi     : Bounds -> WithBounds String -> Syntax -> Syntax -> Syntax
   Lambda : Bounds -> WithBounds String -> Syntax -> Syntax
   App    : Syntax -> Syntax -> Syntax
+  -- Dependent Sums
+  Sigma  : Bounds -> WithBounds String -> Syntax -> Syntax -> Syntax
+  Pair   : Bounds -> Syntax -> Syntax -> Syntax
+  Fst    : Bounds -> Syntax -> Syntax
+  Snd    : Bounds -> Syntax -> Syntax
   -- True
   Top    : Bounds -> Syntax
   Point  : Bounds -> Syntax
@@ -55,8 +60,26 @@ Pretty Syntax where
     parenthesise (d >= App) $
     group $
     fillSep [prettyPrec Open t, prettyPrec App u]
+  prettyPrec d (Sigma _ var a b) =
+    parenthesise (d >= App) $
+    group $
+    parens (pretty var.val <++> colon <+> softline <+> prettyPrec Open a) <++>
+    pretty "**" <+> softline <+>
+    prettyPrec Open b
+  prettyPrec d (Pair _ t u) =
+    angles $
+    group $
+    neutral <++> prettyPrec Open t <+> comma <+> softline <+> prettyPrec Open u <++> neutral
+  prettyPrec d (Fst _ t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "fst", prettyPrec App t]
+  prettyPrec d (Snd _ t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "snd", prettyPrec App t]
   prettyPrec d (Top _) = pretty "()"
-  prettyPrec d (Point _) = pretty "*"
+  prettyPrec d (Point _) = pretty "tt"
   prettyPrec d (Bottom _) = pretty "Void"
   prettyPrec d (Absurd _ a t) =
     parenthesise (d >= App) $
diff --git a/src/Obs/Term.idr b/src/Obs/Term.idr
index 366a4b7..9221dbd 100644
--- a/src/Obs/Term.idr
+++ b/src/Obs/Term.idr
@@ -19,6 +19,11 @@ data Term : Nat -> Type where
   Pi     : Bounds -> String -> Term n -> Term (S n) -> Term n
   Lambda : Bounds -> String -> Term (S n) -> Term n
   App    : Term n -> Term n -> Term n
+  -- Dependent Sums
+  Sigma  : Bounds -> String -> Term n -> Term (S n) -> Term n
+  Pair   : Bounds -> Term n -> Term n -> Term n
+  Fst    : Bounds -> Term n -> Term n
+  Snd    : Bounds -> Term n -> Term n
   -- True
   Top    : Bounds -> Term n
   Point  : Bounds -> Term n
@@ -48,6 +53,10 @@ fullBounds tm@(Sort x s) = MkBounded tm False x
 fullBounds tm@(Pi x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
 fullBounds tm@(Lambda x var t) = mergeBounds (fullBounds t) (MkBounded tm False x)
 fullBounds tm@(App t u) = map (\_ => tm) (mergeBounds (fullBounds t) (fullBounds u))
+fullBounds tm@(Sigma x var a b) = mergeBounds (mergeBounds (fullBounds a) (fullBounds b)) (MkBounded tm False x)
+fullBounds tm@(Pair x t u) = mergeBounds (mergeBounds (fullBounds t) (fullBounds u)) (MkBounded tm False x)
+fullBounds tm@(Fst x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
+fullBounds tm@(Snd x t) = mergeBounds (fullBounds t) (MkBounded tm False x)
 fullBounds tm@(Top x) = MkBounded tm False x
 fullBounds tm@(Point x) = MkBounded tm False x
 fullBounds tm@(Bottom x) = MkBounded tm False x
@@ -75,8 +84,26 @@ Pretty (Term n) where
     parenthesise (d >= App) $
     group $
     fillSep [prettyPrec Open t, prettyPrec App u]
+  prettyPrec d (Sigma _ var a b) =
+    parenthesise (d >= App) $
+    group $
+    parens (pretty var <++> colon <+> softline <+> prettyPrec Open a) <++>
+    pretty "**" <+> softline <+>
+    prettyPrec Open b
+  prettyPrec d (Pair _ t u) =
+    angles $
+    group $
+    neutral <++> prettyPrec Open t <+> comma <+> softline <+> prettyPrec Open u <++> neutral
+  prettyPrec d (Fst _ t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "fst", prettyPrec App t]
+  prettyPrec d (Snd _ t) =
+    parenthesise (d >= App) $
+    group $
+    fillSep [pretty "snd", prettyPrec App t]
   prettyPrec d (Top _) = pretty "()"
-  prettyPrec d (Point _) = pretty "*"
+  prettyPrec d (Point _) = pretty "tt"
   prettyPrec d (Bottom _) = pretty "Void"
   prettyPrec d (Absurd _ a t) =
     parenthesise (d > Open) $
diff --git a/src/Obs/Typing.idr b/src/Obs/Typing.idr
index c5d837f..bf7ebc1 100644
--- a/src/Obs/Typing.idr
+++ b/src/Obs/Typing.idr
@@ -52,6 +52,10 @@ covering partial
 subst      : NormalForm n -> (Fin n -> Logging ann (NormalForm m)) -> Logging ann (NormalForm m)
 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)
 
 substCnstr (Sort s) f = pure $ Sort s
 substCnstr (Pi s s' var a b) f = do
@@ -61,6 +65,14 @@ substCnstr (Pi s s' var a b) f = do
 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
 
@@ -72,6 +84,12 @@ 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
 
 subst (Ntrl t)  f = substNtrl t f
@@ -83,6 +101,16 @@ 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
 
+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
+
+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
+
 partial
 subst1 : NormalForm n -> NormalForm (S n) -> Logging ann (NormalForm n)
 subst1 t u = subst u (add (Logging ann . NormalForm) (pure t) (pure . point))
@@ -102,6 +130,9 @@ convert (Cnstr (Sort s')) (Cnstr (Sort s'')) (Cnstr (Sort _)) (Set _) = pure $ 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
@@ -112,6 +143,16 @@ 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 $
@@ -166,6 +207,15 @@ check ctx tm@(Lambda _ _ t) (Cnstr (Pi s s' var a b)) _ = do
   t <- check (ctx ::< (var, a, s)) t b s'
   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)
+  inScope "check" $ trace $ map (\_ => pretty {ann} "checking first for type" <++> pretty a) (fullBounds tm)
+  t <- check ctx t a s
+  b <- subst1 t b
+  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)
 check ctx tm ty s = do
   let bounded = fullBounds tm
   inScope "check" $ trace $ map (\_ => "checking has fallen through") bounded
@@ -205,6 +255,33 @@ infer ctx tm@(App t u) = do
   ty <- subst1 u b
   inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty ty) (fullBounds tm)
   pure (res, ty, s')
+infer ctx tm@(Sigma _ var a b) = do
+  inScope "infer" $ trace $ map (\_ => "encountered Sigma type") (fullBounds tm)
+  (a, s) <- inferType ctx a
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "first has type" <++> pretty a) (fullBounds tm)
+  (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@(Fst _ t) = do
+  inScope "infer" $ trace $ map (\_ => "encountered first projection") (fullBounds tm)
+  let bounded = fullBounds t
+  (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t
+    | (_, t, _) => inScope "wrong type to fst" $ fatal (map (\_ => t) bounded)
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) (fullBounds tm)
+  res <- doFst t
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "final result is" <++> pretty res <+> softline <+> pretty "of type" <++> pretty a) (fullBounds tm)
+  pure (res, a, s)
+infer ctx tm@(Snd _ t) = do
+  inScope "infer" $ trace $ map (\_ => "encountered first projection") (fullBounds tm)
+  let bounded = fullBounds t
+  (t, ty@(Cnstr (Sigma s s' _ a b)), _) <- infer ctx t
+    | (_, t, _) => inScope "wrong type to fst" $ fatal (map (\_ => t) bounded)
+  inScope "infer" $ trace $ map (\_ => pretty {ann} "pair has type" <++> pretty ty) (fullBounds 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) (fullBounds tm)
+  pure (res, b, s')
 infer ctx (Top b) = pure $ (Cnstr Top, cast Prop, Set 0)
 infer ctx (Point b) = pure $ (Irrel, Cnstr Top, Prop)
 infer ctx (Bottom b) = pure $ (Cnstr Bottom, cast Prop, Set 0)