diff --git a/README.md b/README.md
index 0ba1881..52c6397 100644
--- a/README.md
+++ b/README.md
@@ -19,7 +19,6 @@ A dependently typed system
 # TODO
 
 * Fun types
-  * Σ
   * Id
 
 * Parser
diff --git a/src/Check.idr b/src/Check.idr
index b72feea..b438257 100644
--- a/src/Check.idr
+++ b/src/Check.idr
@@ -22,20 +22,32 @@ mutual
   check trs tys xpt' tr = do
     xpt <- whnf xpt'
     case tr of
-      TLam sc => case xpt of
-                      VClos env (TPi a b) => do
-                        v <- VGen <$> fresh
-                        check (v :: trs) (VClos env a :: tys) (VClos (v :: env) b) sc
-                      _ => oops "expected pi"
+      TLam sc    => case xpt of
+                         VClos env (TPi a b) => do
+                           v <- VGen <$> fresh
+                           check (v :: trs) (VClos env a :: tys) (VClos (v :: env) b) sc
+                         _ => oops "expected pi"
 
-      TPi a b => case xpt of
-                      VType => do
-                        v <- VGen <$> fresh
-                        (&&) <$> check trs tys VType a 
-                             <*> delay <$> check (v :: trs) (VClos trs a :: tys) VType b
+      -- pi and sigma could be inferred /shrug
+      TPi a b    => case xpt of
+                         VType => do
+                           v <- VGen <$> fresh
+                           guardS "Pi a" =<< check trs tys VType a 
+                           check (v :: trs) (VClos trs a :: tys) VType b
+                         _ => oops "expected type"
 
+      TSigma a b => case xpt of
+                         VType => do
+                           v <- VGen <$> fresh
+                           guardS "Σ a" =<< check trs tys VType a 
+                           check trs tys (VClos trs (TPi a TType)) b
+                         _ => oops "expected type"
 
-                      _ => oops "expected type"
+      TPair  x y => case xpt of
+                         (VClos env (TSigma a b)) => do
+                           guardS "Pair a" =<< check trs tys (VClos env a) x
+                           check trs tys (VClos env b `VApp` VClos trs x) y
+                         _ => oops "expected sigma"
 
       _       => convert xpt =<< infer trs tys tr
 
@@ -46,7 +58,7 @@ mutual
   infer trs tys (TApp f x) = infer trs tys f >>= whnf >>=
                               \case
                                  VClos env (TPi a b) => do
-                                   guard =<< check trs tys (VClos env a) x
+                                   guardS "app x" =<< check trs tys (VClos env a) x
                                    pure (VClos (VClos trs x :: env) b)
 
                                  _ => oops "expected infer pi"
@@ -57,27 +69,37 @@ mutual
   infer trs tys TStar     = pure VTop
   infer trs tys TZero     = pure VNat
   infer trs tys (TSuc n)  = do 
-    guard =<< check trs tys VNat n
+    guardS "suc n" =<< check trs tys VNat n
     pure VNat
 
   infer trs tys (TTopInd c st) = do
-    guard =<< check trs tys (VClos trs (TPi TTop TType)) c
-    guard =<< check trs tys (VApp (VClos trs c) VStar)   st
+    guardS "⊤ C" =<< check trs tys (VClos trs (TPi TTop TType)) c
+    guardS "⊤ ★" =<< check trs tys (VApp (VClos trs c) VStar)   st
     pure (VClos trs (TPi TTop (TApp (weakTr c) (TVar 0))))
 
   infer trs tys (TBotInd c) = do
-    guard =<< check trs tys (VClos trs (TPi TBot TType)) c
+    guardS "⊥ C" =<< check trs tys (VClos trs (TPi TBot TType)) c
     pure (VClos trs (TPi TBot (TApp (weakTr c) (TVar 0))))
 
   infer trs tys (TNatInd c z s) = do
-    guard =<< check trs tys (VClos trs (TPi TNat TType)) c
-    guard =<< check trs tys (VApp (VClos trs c) (VNatTr 0)) z
-    guard =<< check trs tys (VClos trs (TPi TNat 
-                                            (TPi (TApp (weakTr c) (TVar 0)) 
-                                                 (TApp (weakTr2 c) (TSuc (TVar (FS FZ))))))) s
+    guardS "ℕ C" =<< check trs tys (VClos trs (TPi TNat TType)) c
+    guardS "ℕ z" =<< check trs tys (VApp (VClos trs c) (VNatTr 0)) z
+    guardS "ℕ s" =<< check trs tys (VClos trs (TPi TNat 
+                                              (TPi (TApp (weakTr c) (TVar 0)) 
+                                                   (TApp (weakTr2 c) (TSuc (TVar (FS FZ))))))) s
     pure (VClos trs (TPi TNat (TApp (weakTr c) (TVar 0))))
 
-  infer trs tys _          = oops "cannot infer type"
+  infer trs tys (TSigInd a b c f) = do
+    guardS "Σ A" =<< check trs tys VType a
+    guardS "Σ B" =<< check trs tys (VClos trs (TPi a TType)) b
+    guardS "Σ C" =<< check trs tys (VClos trs (TPi (TSigma a b) TType)) c
+    guardS "Σ f" =<< check trs tys (VClos trs (TPi a {-a:A-}
+                                              (TPi (weakTr b `TApp` TVar 0) {-b:Ba-}
+                                                   (weakTr2 c `TApp` TPair (TVar (FS FZ)) (TVar 0))))) f
+    pure (VClos trs (TPi (TSigma a b) (weakTr c `TApp` TVar 0)))
+                                      
+
+  infer trs tys x          = oops ("cannot infer type" ++ show x)
 
 public export
 typecheck : Term 0 -> Term 0 -> Either String (Bool, List String)
diff --git a/src/Convert.idr b/src/Convert.idr
index 7cef25f..07ce672 100644
--- a/src/Convert.idr
+++ b/src/Convert.idr
@@ -14,6 +14,8 @@ import Data.Vect
 
 %default total
 
+{- TODO: I should throw eval, eval, convert into a helper sometime -}
+
 public export
 convert : Value -> Value -> PI Bool
 convert u1 u2 = do
@@ -31,28 +33,28 @@ convert u1 u2 = do
 
       (VNatTr n, VNatTr m) => pure (n == m)
 
-      (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 
-                                       <*> delay <$> convert x1 x2
+      (VApp f1 x1, VApp f2 x2) => (&&) <$> convert f1 f2 <*> delay <$> convert x1 x2
+
       (VGen k1, VGen k2) => pure (k1 == k2)
 
+      (VPair a1 b1, VPair a2 b2) => (&&) <$> convert a1 a2 <*> delay <$> convert b1 b2
+
       (VClos env1 (TLam sc1), VClos env2 (TLam sc2)) => do
         v <- VGen <$> fresh
-        convert (VClos (v :: env1) sc1)
-                (VClos (v :: env2) sc2)
+        convert (VClos (v :: env1) sc1) (VClos (v :: env2) sc2)
 
       (VClos env1 (TPi a1 b1), VClos env2 (TPi a2 b2)) => do
         v <- VGen <$> fresh
-        (&&) <$> convert (VClos env1 a1)
-                         (VClos env2 a2)
-             <*> delay <$> convert (VClos (v :: env1) b1)
-                                   (VClos (v :: env2) b2)
+        guard =<< convert (VClos env1 a1) (VClos env2 a2)
+        convert (VClos (v :: env1) b1) (VClos (v :: env2) b2)
 
       (VClos env1 (TTopInd c1 st1), VClos env2 (TTopInd c2 st2)) => do
         c1' <- eval env1 c1
         c2' <- eval env2 c2
+        guard =<< convert c1' c2'
         st1' <- eval env1 st1
         st2' <- eval env2 st2
-        (&&) <$> convert c1' c2' <*> delay <$> convert st1' st2'
+        convert st1' st2'
 
       (VClos env1 (TBotInd c1), VClos env2 (TBotInd c2)) => do
         c1' <- eval env1 c1
@@ -63,12 +65,34 @@ convert u1 u2 = do
       (VClos env1 (TNatInd c1 z1 s1), VClos env2 (TNatInd c2 z2 s2)) => do
         c1' <- eval env1 c1
         c2' <- eval env2 c2
+        guard =<< convert c1' c2'
         z1' <- eval env1 z1
         z2' <- eval env2 z2
+        guard =<< convert z1' z2'
         s1' <- eval env1 s1
         s2' <- eval env2 s2
-        b1  <- (&&) <$> convert c1' c2' <*> delay <$> convert z1' z2'
-        guard b1 
         convert s1' s2'
+
+      (VClos env1 (TSigma a1 b1), VClos env2 (TSigma a2 b2)) => do
+        a1' <- eval env1 a1
+        a2' <- eval env2 a2
+        guard =<< convert a1' a2'
+        b1' <- eval env1 b1
+        b2' <- eval env2 b2
+        convert b1' b2'
+
+      (VClos env1 (TSigInd a1 b1 c1 f1), VClos env2 (TSigInd a2 b2 c2 f2)) => do
+        a1' <- eval env1 a1
+        a2' <- eval env2 a2
+        guard =<< convert a1' a2'
+        b1' <- eval env1 b1
+        b2' <- eval env2 b2
+        guard =<< convert b1' b2'
+        c1' <- eval env1 c1
+        c2' <- eval env2 c2
+        guard =<< convert c1' c2'
+        f1' <- eval env1 f1
+        f2' <- eval env2 f2
+        convert f1' f2'
                                   
       _ => pure False
diff --git a/src/Misc.idr b/src/Misc.idr
index 86b2b6b..9eb9b59 100644
--- a/src/Misc.idr
+++ b/src/Misc.idr
@@ -30,6 +30,12 @@ public export
 oops : String -> PI a
 oops = left
 
+public export
+guardS : String -> Bool -> PI ()
+guardS str True  = pure ()
+guardS str False = oops str
+
+
 public export
 fresh : PI Nat
 fresh = do
diff --git a/src/Normalize.idr b/src/Normalize.idr
index 8c0a35b..ee3505b 100644
--- a/src/Normalize.idr
+++ b/src/Normalize.idr
@@ -17,10 +17,10 @@ mutual
   public export
   -- no computational rule for ⊥
   app : Value -> Value -> PI Value
-  app (VClos env (TLam sc))       x          = eval (x :: env) sc
+  app (VClos env (TLam sc))       x = eval (x :: env) sc
 
-  app (VClos env (TTopInd c st))  VTop       = eval env st
-  app f@(VClos env (TTopInd c st))  x        = logS ("⊤-ind applied to " ++ show x)
+  app (VClos env (TTopInd c st)) VTop = eval env st
+  app f@(VClos env (TTopInd c st))  x = logS ("⊤-ind applied to " ++ show x)
                                                >> pure (VApp f x)
 
   app (VClos env (TNatInd _ z s)) (VNatTr n) = do
@@ -35,8 +35,16 @@ mutual
         sn <- app s (VNatTr n)
         app sn rec
 
-  app f@(VClos env (TNatInd _ z s)) x          = logS ("ℕ-ind applied to " ++ show x)
-                                                 >> pure (VApp f x)
+  app f@(VClos env (TNatInd _ z s)) x = logS ("ℕ-ind applied to " ++ show x)
+                                        >> pure (VApp f x)
+
+  app (VClos env (TSigInd _ _ c f)) (VPair a b) = do
+    f' <- eval env f
+    fa <- app f' a
+    app fa b
+
+  app f@(VClos env (TSigInd _ _ c p)) x = logS ("Σ-ind applied to " ++ show x)
+                                          >> pure (VApp f x)
 
   app f x = pure (VApp f x)
 
@@ -47,21 +55,26 @@ mutual
     f' <- eval env f
     x' <- eval env x
     assert_total (app f' x') -- :(
-  eval env TType      = pure VType
-  eval env TTop       = pure VTop
-  eval env TStar      = pure VStar
-  eval env TBot       = pure VBot
-  eval env TNat       = pure VNat
-  eval env TZero      = pure (VNatTr 0)
+  eval env TType       = pure VType
+  eval env TTop        = pure VTop
+  eval env TStar       = pure VStar
+  eval env TBot        = pure VBot
+  eval env TNat        = pure VNat
+  eval env TZero       = pure (VNatTr 0)
 
-  eval env (TSuc n)   = do
+  eval env (TSuc n)    = do
     n' <- eval env n
     case n' of
          VNatTr n => pure (VNatTr (S n))
          x        => logS ("suc applied to " ++ show x)
                      >> pure (VClos env (TSuc n))
 
-  eval env tr         = pure (VClos env tr)
+  eval env (TPair a b) = do
+    a' <- eval env a
+    b' <- eval env b
+    pure (VPair a' b')
+
+  eval env tr          = pure (VClos env tr)
 
 public export
 whnf : Value -> PI Value
diff --git a/src/Term.idr b/src/Term.idr
index 9fd77cb..c128b1d 100644
--- a/src/Term.idr
+++ b/src/Term.idr
@@ -26,13 +26,17 @@ data Term : (_ : Index) -> Type where
   TSuc    : Term n -> Term n                     -- successor
   TNatInd : Term n -> Term n -> Term n -> Term n -- : (x : ℕ) → C x
 
+  TSigma  : Term n -> Term n -> Term n                     -- Sum type (Σ _ : A, B _)
+  TPair   : Term n -> Term n -> Term n                     -- Sum constructor _,_
+  TSigInd : Term n -> Term n -> Term n -> Term n -> Term n -- A B C f : (x : Σ _ : A , B _) → C x
+
   TLam    : Term (S n) -> Term n                 -- Lambda abstraction (λ _ . Scope)
   TPi     : Term n -> Term (S n) -> Term n       -- Pi type            (∏ _ : A . B _ )
 
   TApp    : Term n -> Term n -> Term n           -- Appliction
-  TVar    : Fin n  -> Term n                      -- Variable
+  TVar    : Fin n  -> Term n                     -- Variable
 
-infixl 2 `TApp`
+infixl 3 `TApp`
 
 public export
 Show (Term n) where
@@ -50,6 +54,10 @@ Show (Term n) where
   show (TSuc n)        = "suc (" ++ show n ++ ")"
   show (TNatInd c z s) = "ℕ-ind (" ++ show c ++ ") (" ++ show z ++ ") (" ++ show s ++ ")"
 
+  show (TSigma a b)    = "TSigma (" ++ show a ++ ") (" ++ show b ++ ")"
+  show (TPair a b)     = "TPair (" ++ show a ++ ") (" ++ show b ++ ")"
+  show (TSigInd a b c f) = "Σ-ind (" ++ show a ++ ") (" ++ show b ++ ") (" ++ show c ++ ") (" ++ show f ++ ")"
+
   show (TLam sc)       = "TLam (" ++ show sc ++ ")"
   show (TPi  ty sc)    = "TPi (" ++ show ty ++ ") (" ++ show sc ++ ")"
 
@@ -61,22 +69,25 @@ weakTr : Term n -> Term (S n)
 weakTr = go 0
   where
     go : {0 n : Nat} -> Fin (S n) -> Term n -> Term (S n)
-    go n TType           = TType
-    go n TTop            = TTop
-    go n TStar           = TTop
-    go n (TTopInd c st)  = TTopInd (go n c) (go n st)
-    go n TBot            = TBot
-    go n (TBotInd c)     = TBotInd (go n c)
-    go n TNat            = TNat
-    go n TZero           = TZero
-    go n (TSuc m)        = TSuc (go n m)
-    go n (TNatInd c z s) = TNatInd (go n c) (go n z) (go n s)
-    go n (TLam sc)       = TLam (go (FS n) sc)
-    go n (TPi  ty sc)    = TPi (go n ty) (go (FS n) sc)
-    go n (TApp f x)      = TApp (go n f) (go n x)
-    go n (TVar i)        = if weaken i < n
-                              then TVar (weaken i)
-                              else TVar (FS i)
+    go n TType             = TType
+    go n TTop              = TTop
+    go n TStar             = TTop
+    go n (TTopInd c st)    = TTopInd (go n c) (go n st)
+    go n TBot              = TBot
+    go n (TBotInd c)       = TBotInd (go n c)
+    go n TNat              = TNat
+    go n TZero             = TZero
+    go n (TSuc m)          = TSuc (go n m)
+    go n (TNatInd c z s)   = TNatInd (go n c) (go n z) (go n s)
+    go n (TSigma a b)      = TSigma (go n a) (go n b)
+    go n (TPair a b)       = TPair (go n a) (go n b)
+    go n (TSigInd a b c f) = TSigInd (go n a) (go n b) (go n c) (go n f)
+    go n (TLam sc)         = TLam (go (FS n) sc)
+    go n (TPi  ty sc)      = TPi (go n ty) (go (FS n) sc)
+    go n (TApp f x)        = TApp (go n f) (go n x)
+    go n (TVar i)          = if weaken i < n
+                                then TVar (weaken i)
+                                else TVar (FS i)
 
 public export
 weakTr2 : Term n -> Term (2+n)
diff --git a/src/Tests.idr b/src/Tests.idr
index 6e8499b..37abb8e 100644
--- a/src/Tests.idr
+++ b/src/Tests.idr
@@ -22,11 +22,11 @@ test_id = typecheck (TLam (TLam (TVar 0)))
 
 {- λA. λB. λf. λx. f x : ∏ (A : Type) ∏ (B : A → Type) ∏ (f : ∏ (x : A) B x) ∏ (x : A) B x -}
 test_app : Either String (Bool, List String)
-test_app = typecheck (TLam (TLam (TLam (TLam (TApp (TVar 1) (TVar 0))))))
+test_app = typecheck (TLam (TLam (TLam (TLam (TVar 1 `TApp` TVar 0)))))
                      (TPi TType 
                           (TPi (TPi (TVar 0) TType)
-                               (TPi (TPi (TVar 1) (TApp (TVar 1) (TVar 0))) 
-                                    (TPi (TVar 2) (TApp (TVar 2) (TVar 0))))))
+                               (TPi (TPi (TVar 1) (TVar 1 `TApp` TVar 0)) 
+                                    (TPi (TVar 2) (TVar 2 `TApp` TVar 0)))))
 
 {- λf. λx. f x ≃ λf. λx. (λy. f y) x -}
 eta_test : Either String (Bool, List String)
@@ -34,14 +34,14 @@ eta_test = resolve action
   where
     action : PI Bool
     action = do
-      x <- eval ctx0 (TLam (TLam (TApp (TVar 1) (TVar 0))))
-      y <- eval ctx0 (TLam (TLam (TApp (TLam (TApp (TVar 2) (TVar 0))) (TVar 0))))
+      x <- eval ctx0 (TLam (TLam (TVar 1 `TApp` TVar 0)))
+      y <- eval ctx0 (TLam (TLam (TLam (TVar 2 `TApp` TVar 0) `TApp` TVar 0)))
       convert x y
 
 addition : Term 0
 addition = TNatInd (TLam (TPi TNat TNat)) 
                    (TLam (TVar 0)) 
-                   (TLam {-n-} (TLam {-n+-} (TLam {-m-} (TSuc (TApp (TVar 1) (TVar 0))))))
+                   (TLam {-n-} (TLam {-n+-} (TLam {-m-} (TSuc (TVar 1 `TApp` TVar 0)))))
 
 addition_type : Either String (Bool, List String)
 addition_type = typecheck addition (TPi TNat (TPi TNat TNat))
@@ -80,3 +80,38 @@ unit_test = typecheck TStar TTop
 
 absurd_test : Either String (Bool, List String)
 absurd_test = typecheck (TLam (TBotInd (TLam (TVar 1)))) (TPi TType (TPi TBot (TVar 1)))
+
+pr1ty : Term 0
+pr1ty = TPi TType {- A : Type -}
+            (TPi (TPi (TVar 0) TType) {- B : A → Type -}
+                 (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -}
+                      (TVar 2)))
+
+pr1 : Term 0
+pr1 = TLam {- A : Type -} 
+           (TLam {- B : A → Type -}
+                 (TSigInd (TVar 1) (TVar 0) (TLam {-ΣAB-} (TVar 2)) (TLam (TLam (TVar 1)))))
+
+pr1_test : Either String (Bool, List String)
+pr1_test = typecheck pr1 pr1ty
+
+pr2ty : Term 0
+pr2ty = TPi TType {- A : Type -}
+            (TPi (TPi (TVar 0) TType) {- B : A → Type -}
+                 (TPi (TSigma (TVar 1) (TVar 0)) {- Σ A B -}
+                      (TVar 1 `TApp` (TSigInd (TVar 2) (TVar 1) (TLam (TVar 3)) (TLam (TLam (TVar 1))) `TApp` TVar 0))))
+
+pr2 : Term 0
+pr2 = TLam {- A : Type -} 
+           (TLam {- B : A → Type -}
+                 (TSigInd (TVar 1)
+                          (TVar 0)
+                          (TLam {-ΣAB-}
+                                (TVar 1 `TApp` (TSigInd (TVar 2) (TVar 1) (TLam (TVar 3)) (TLam (TLam (TVar 1))) `TApp` TVar 0)))
+                          (TLam (TLam (TVar 0)))))
+
+pr2ty_test : Either String (Bool, List String)
+pr2ty_test = typecheck pr2ty TType
+
+pr2_test : Either String (Bool, List String)
+pr2_test = typecheck pr2 pr2ty
diff --git a/src/Value.idr b/src/Value.idr
index da75fe3..43b3541 100644
--- a/src/Value.idr
+++ b/src/Value.idr
@@ -20,10 +20,14 @@ mutual
     VNat   : Value
     VNatTr : Nat -> Value
 
+    VPair  : Value -> Value -> Value
+
     VGen   : Nat   -> Value
     VApp   : Value -> Value  -> Value
     VClos  : Ctx n -> Term n -> Value
 
+  infixl 2 `VApp`
+
   public export
   Ctx : Index -> Type
   Ctx i = Vect i Value
@@ -39,6 +43,7 @@ Show Value where
   show VStar       = "VStar"
   show VBot        = "VBot"
   show VNat        = "VNat"
+  show (VPair a b) = "VPair (" ++ show a ++ ") (" ++ show b ++ ")"
   show (VNatTr n)  = "V" ++ show n
   show (VGen i)    = "VGen " ++ show i
   show (VApp f x)  = "VApp (" ++ show f ++ ") (" ++ show x ++ ")"