diff --git a/lib/Check.hs b/lib/Check.hs
index 55ecce0..106167d 100644
--- a/lib/Check.hs
+++ b/lib/Check.hs
@@ -16,11 +16,11 @@ matchPi x mt =
         (Pi _ a b) -> pure (a, b)
         t -> throwError $ ExpectedPiType x t
 
-matchProd :: Expr -> Expr -> ReaderT Env Result (Expr, Expr)
-matchProd x mt =
+matchSigma :: Expr -> Expr -> ReaderT Env Result (Expr, Expr)
+matchSigma x mt =
     whnf mt >>= \case
-        (Prod a b) -> pure (a, b)
-        t -> throwError $ ExpectedProdType x t
+        (Sigma _ a b) -> pure (a, b)
+        t -> throwError $ ExpectedSigmaType x t
 
 findLevel :: Context -> Expr -> ReaderT Env Result Integer
 findLevel g a = do
@@ -78,17 +78,17 @@ findType g e@(Let _ (Just t) v b) = do
     _ <- findType g t
     betaEquiv' e t res
     pure t
-findType g (Prod a b) = do
+findType g (Sigma _ a b) = do
     aSort <- findType g a
     bSort <- findType g b
     liftEither $ compSort a b aSort bSort
 findType g (Pair a b) = do
     aType <- findType g a
     bType <- findType g b
-    validateType g $ Prod aType bType
-    pure $ Prod aType bType
-findType g (Pi1 x) = fst <$> (findType g x >>= matchProd x)
-findType g (Pi2 x) = snd <$> (findType g x >>= matchProd x)
+    validateType g $ Sigma "" aType bType
+    pure $ Sigma aType bType
+findType g (Pi1 x) = fst <$> (findType g x >>= matchSigma x)
+findType g (Pi2 x) = snd <$> (findType g x >>= matchSigma x)
 
 checkType :: Env -> Expr -> Result Expr
 checkType env t = runReaderT (findType [] t) env
diff --git a/lib/Elaborator.hs b/lib/Elaborator.hs
index b0cc77d..6d13cb3 100644
--- a/lib/Elaborator.hs
+++ b/lib/Elaborator.hs
@@ -116,7 +116,7 @@ usedVars (I.Let name ascr value body) = saveState $ do
     ascr' <- traverse usedVars ascr
     removeName name
     S.union (ty' `S.union` (ascr' ?: S.empty)) <$> usedVars body
-usedVars (I.Prod m n) = S.union <$> usedVars m <*> usedVars n
+usedVars (I.Sigma m n) = S.union <$> usedVars m <*> usedVars n
 usedVars (I.Pair m n) = S.union <$> usedVars m <*> usedVars n
 usedVars (I.Pi1 x) = usedVars x
 usedVars (I.Pi2 x) = usedVars x
@@ -146,7 +146,7 @@ traverseBody (I.Let name ascr value body) = saveState $ do
     value' <- traverseBody value
     removeName name
     I.Let name ascr' value' <$> traverseBody body
-traverseBody (I.Prod m n) = I.Prod <$> traverseBody m <*> traverseBody n
+traverseBody (I.Sigma m n) = I.Sigma <$> traverseBody m <*> traverseBody n
 traverseBody (I.Pair m n) = I.Pair <$> traverseBody m <*> traverseBody n
 traverseBody (I.Pi1 x) = I.Pi1 <$> traverseBody x
 traverseBody (I.Pi2 x) = I.Pi2 <$> traverseBody x
@@ -214,7 +214,7 @@ elaborate ir = evalState (elaborate' ir) []
         ty' <- elaborate' ty
         modify (name :)
         E.Let name (Just ty') val' <$> elaborate' body
-    elaborate' (I.Prod m n) = E.Prod <$> elaborate' m <*> elaborate' n
+    elaborate' (I.Sigma m n) = E.Sigma <$> elaborate' m <*> elaborate' n
     elaborate' (I.Pair m n) = E.Pair <$> elaborate' m <*> elaborate' n
     elaborate' (I.Pi1 x) = E.Pi1 <$> elaborate' x
     elaborate' (I.Pi2 x) = E.Pi2 <$> elaborate' x
diff --git a/lib/Errors.hs b/lib/Errors.hs
index 298f4d5..949f022 100644
--- a/lib/Errors.hs
+++ b/lib/Errors.hs
@@ -9,7 +9,7 @@ data Error
     = UnboundVariable Text
     | NotASort Expr
     | ExpectedPiType Expr Expr
-    | ExpectedProdType Expr Expr
+    | ExpectedSigmaType Expr Expr
     | NotEquivalent Expr Expr Expr
     | PNMissingType Text
     | DuplicateDefinition Text
@@ -19,7 +19,7 @@ instance Pretty Error where
     pretty (UnboundVariable x) = "Unbound variable: '" <> pretty x <> "'"
     pretty (NotASort x) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> "is not a type"
     pretty (ExpectedPiType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a function, instead is type" <> line <> pretty t)
-    pretty (ExpectedProdType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a pair, instead is type" <> line <> pretty t)
+    pretty (ExpectedSigmaType x t) = group $ hang 4 ("Term:" <> line <> pretty x) <> line <> hang 4 ("is not a pair, instead is type" <> line <> pretty t)
     pretty (NotEquivalent a a' e) =
         group $
             hang 4 ("Cannot unify" <> line <> pretty a)
diff --git a/lib/Eval.hs b/lib/Eval.hs
index 51d4060..87f8a1c 100644
--- a/lib/Eval.hs
+++ b/lib/Eval.hs
@@ -45,7 +45,7 @@ subst k s (App m n) = App (subst k s m) (subst k s n)
 subst k s (Abs x m n) = Abs x (subst k s m) (subst (k + 1) (incIndices s) n)
 subst k s (Pi x m n) = Pi x (subst k s m) (subst (k + 1) (incIndices s) n)
 subst k s (Let x t v b) = Let x t (subst k s v) (subst (k + 1) (incIndices s) b)
-subst k s (Prod m n) = Prod (subst k s m) (subst k s n)
+subst k s (Sigma x m n) = Sigma x (subst k s m) (subst (k + 1) (incIndices s) n)
 subst k s (Pair m n) = Pair (subst k s m) (subst k s n)
 subst k s (Pi1 x) = Pi1 (subst k s x)
 subst k s (Pi2 x) = Pi2 (subst k s x)
@@ -63,7 +63,7 @@ reduce (Abs x t v) = Abs x <$> reduce t <*> reduce v
 reduce (Pi x t v) = Pi x <$> reduce t <*> reduce v
 reduce (Free n) = envLookupVal n
 reduce (Let _ _ v b) = pure $ subst 0 v b
-reduce (Prod a b) = Prod <$> reduce a <*> reduce b
+reduce (Sigma x a b) = Sigma x <$> reduce a <*> reduce b
 reduce (Pair a b) = Pair <$> reduce a <*> reduce b
 reduce (Pi1 (Pair a _)) = pure a
 reduce (Pi2 (Pair _ b)) = pure b
@@ -121,7 +121,7 @@ betaEquiv e1 e2
             (Pi _ t1 v1, Pi _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2
             (Let _ _ v b, e) -> betaEquiv (subst 0 v b) e
             (e, Let _ _ v b) -> betaEquiv (subst 0 v b) e
-            (Prod a b, Prod a' b') -> (&&) <$> betaEquiv a a' <*> betaEquiv b b'
+            (Sigma _ a b, Sigma _ a' b') -> (&&) <$> betaEquiv a a' <*> betaEquiv b b'
             (Pair a b, Pair a' b') -> (&&) <$> betaEquiv a a' <*> betaEquiv b b'
             (Pi1 x, Pi1 x') -> betaEquiv x x'
             (Pi2 x, Pi2 x') -> betaEquiv x x'
diff --git a/lib/Expr.hs b/lib/Expr.hs
index 5fce231..77bb85a 100644
--- a/lib/Expr.hs
+++ b/lib/Expr.hs
@@ -15,7 +15,7 @@ data Expr where
     Abs :: Text -> Expr -> Expr -> Expr
     Pi :: Text -> Expr -> Expr -> Expr
     Let :: Text -> Maybe Expr -> Expr -> Expr -> Expr
-    Prod :: Expr -> Expr -> Expr
+    Sigma :: Text -> Expr -> Expr -> Expr
     Pair :: Expr -> Expr -> Expr
     Pi1 :: Expr -> Expr
     Pi2 :: Expr -> Expr
@@ -34,7 +34,7 @@ instance Eq Expr where
     (Abs _ t1 b1) == (Abs _ t2 b2) = t1 == t2 && b1 == b2
     (Pi _ t1 b1) == (Pi _ t2 b2) = t1 == t2 && b1 == b2
     (Let _ _ v1 b1) == (Let _ _ v2 b2) = v1 == v2 && b1 == b2
-    (Prod x1 y1) == (Prod x2 y2) = x1 == x2 && y1 == y2
+    (Sigma _ x1 y1) == (Sigma _ x2 y2) = x1 == x2 && y1 == y2
     (Pair x1 y1) == (Pair x2 y2) = x1 == x2 && y1 == y2
     (Pi1 x) == (Pi1 y) = x == y
     (Pi2 x) == (Pi2 y) = x == y
@@ -50,7 +50,7 @@ occursFree n (App a b) = on (||) (occursFree n) a b
 occursFree n (Abs _ a b) = occursFree n a || occursFree (n + 1) b
 occursFree n (Pi _ a b) = occursFree n a || occursFree (n + 1) b
 occursFree n (Let _ _ v b) = occursFree n v || occursFree (n + 1) b
-occursFree n (Prod x y) = occursFree n x || occursFree n y
+occursFree n (Sigma _ x y) = occursFree n x || occursFree n y
 occursFree n (Pair x y) = occursFree n x || occursFree n y
 occursFree n (Pi1 x) = occursFree n x
 occursFree n (Pi2 x) = occursFree n x
@@ -67,7 +67,7 @@ shiftIndices d c (App m n) = App (shiftIndices d c m) (shiftIndices d c n)
 shiftIndices d c (Abs x m n) = Abs x (shiftIndices d c m) (shiftIndices d (c + 1) n)
 shiftIndices d c (Pi x m n) = Pi x (shiftIndices d c m) (shiftIndices d (c + 1) n)
 shiftIndices d c (Let x t v b) = Let x t (shiftIndices d c v) (shiftIndices d (c + 1) b)
-shiftIndices d c (Prod m n) = Prod (shiftIndices d c m) (shiftIndices d c n)
+shiftIndices d c (Sigma x m n) = Sigma x (shiftIndices d c m) (shiftIndices d c n)
 shiftIndices d c (Pair m n) = Pair (shiftIndices d c m) (shiftIndices d c n)
 shiftIndices d c (Pi1 x) = Pi1 (shiftIndices d c x)
 shiftIndices d c (Pi2 x) = Pi2 (shiftIndices d c x)
@@ -222,7 +222,8 @@ prettyExpr k expr = case expr of
       where
         (binds, body) = collectLets expr
         bindings = sep $ map pretty binds
-    (Prod x y) -> parens $ parens (pretty x) <+> "×" <+> parens (pretty y)
+    (Sigma "" x y) -> parens $ parens (pretty x) <+> "×" <+> parens (pretty y)
+    (Sigma x t m) -> parens $ "Σ" <+> pretty x <+> ":" <+> pretty t <> "," <+> pretty m
     (Pair x y) -> parens $ pretty x <> "," <+> pretty y
     (Pi1 x) -> parens $ "π₁" <+> parens (pretty x)
     (Pi2 x) -> parens $ "π₂" <+> parens (pretty x)
diff --git a/lib/IR.hs b/lib/IR.hs
index c0c45e2..923aa3a 100644
--- a/lib/IR.hs
+++ b/lib/IR.hs
@@ -27,7 +27,7 @@ data IRExpr
         , letValue :: IRExpr
         , letBody :: IRExpr
         }
-    | Prod
+    | Sigma
         { prodLeft :: IRExpr
         , prodRight :: IRExpr
         }
diff --git a/lib/Parser.hs b/lib/Parser.hs
index e0605ef..5d97836 100644
--- a/lib/Parser.hs
+++ b/lib/Parser.hs
@@ -174,11 +174,11 @@ pSort = lexeme $ pStar <|> pSquare
 pOpSection :: Parser IRExpr
 pOpSection = lexeme $ parens $ Var <$> pSymbol
 
-pProd :: Parser IRExpr
-pProd = lexeme $ between (char '{') (char '}') $ do
+pSigma :: Parser IRExpr
+pSigma = lexeme $ between (char '{') (char '}') $ do
     left <- pIRExpr
     _ <- symbol "×"
-    Prod left <$> pIRExpr
+    Sigma left <$> pIRExpr
 
 pPair :: Parser IRExpr
 pPair = lexeme $ between (char '<') (char '>') $ do
@@ -193,7 +193,7 @@ pPi2 :: Parser IRExpr
 pPi2 = lexeme $ symbol "π₂" >> Pi2 <$> pIRExpr
 
 pTerm :: Parser IRExpr
-pTerm = lexeme $ label "term" $ choice [pSort, pPi1, pPi2, pPureVar, pVar, pProd, pPair, try pOpSection, parens pIRExpr]
+pTerm = lexeme $ label "term" $ choice [pSort, pPi1, pPi2, pPureVar, pVar, pSigma, pPair, try pOpSection, parens pIRExpr]
 
 pInfix :: Parser IRExpr
 pInfix = parseWithPrec 0