diff --git a/Sit.cabal b/Sit.cabal
--- a/Sit.cabal
+++ b/Sit.cabal
@@ -1,5 +1,5 @@
 name:            Sit
-version:         0.2017.05.01
+version:         0.2017.05.02
 build-type:      Simple
 cabal-version:   >= 1.8
 license:         OtherLicense
@@ -45,10 +45,6 @@
                     containers >= 0.3 && < 1.0,
                     data-lens-light >= 0.1.2.2 && < 0.2,
                     mtl >= 2.2.1 && < 3.0
-
---  -- The lexer and parser are shipped as .hs files, thus, no tools necessary.
---  build-tools:      happy >= 1.15 && < 2,
---                    alex >= 3.0 && < 4
 
   extensions:       MultiParamTypeClasses
                     FunctionalDependencies
diff --git a/src/Evaluation.hs b/src/Evaluation.hs
--- a/src/Evaluation.hs
+++ b/src/Evaluation.hs
@@ -3,7 +3,6 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TemplateHaskell #-}
 {-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}
--- {-# LANGUAGE FunctionalDependencies, UndecidableInstances #-}
 
 -- | Values and weak head evaluation
 
@@ -47,13 +46,10 @@
   | VSuc VSize Val
   | VInfty
   | VPi (Dom VType) VClos
-  -- Functions
   | -- | Lambda abstraction
     VLam VClos
   | -- | @\ x -> x e@ for internal use in fix.
     VElimBy VElim
-  -- -- | -- | Constant function
-  -- --   VConst Val
   | -- | Neutrals.
     VUp VType VNe
   | -- | Type annotation for readback (normal form).
@@ -191,7 +187,6 @@
     Zero a   -> VZero <$> eval (unArg a)
     Suc a t  -> liftA2 VSuc (eval $ unArg a) (eval t)
     Pi u t   -> liftA2 VPi (eval u) (eval t)
-    -- Lam ai (NoAbs x t) -> VConst <$> eval t
     Lam ai t -> VLam <$> eval t
     Var x -> eval x
     Def f -> lift $ getDef f
@@ -222,7 +217,7 @@
     (_        , Apply u     ) -> apply v u
     (VZero _  , Case _ u _ _) -> return u
     (VSuc _ n , Case _ _ _ f) -> apply f $ defaultArg n
-    (VZero a  , Fix t tf f  ) -> unfoldFix t tf f a v -- apply f $ e : map (Apply . defaultArg) [ v , VZero ]
+    (VZero a  , Fix t tf f  ) -> unfoldFix t tf f a v
     (VSuc a n , Fix t tf f  ) -> unfoldFix t tf f a v
     (VUp (VNat a) n , _)      -> elimNeNat a n e
     _ -> __IMPOSSIBLE__
diff --git a/src/Internal.hs b/src/Internal.hs
--- a/src/Internal.hs
+++ b/src/Internal.hs
@@ -128,15 +128,6 @@
 suc :: Size -> Term -> Term
 suc = Suc . Arg Irrelevant
 
--- var :: Index -> Term
--- var i = Var i []
-
--- app :: Term -> Arg Term -> Maybe Term
--- app t u = case t of
---   Var x es -> Just $ Var x $ es ++ [ Apply u ]
---   Def f es -> Just $ Def f $ es ++ [ Apply u ]
---   _ -> Nothing
-
 defaultArg :: a -> Arg a
 defaultArg = Arg Relevant
 
diff --git a/src/Substitute.hs b/src/Substitute.hs
--- a/src/Substitute.hs
+++ b/src/Substitute.hs
@@ -111,79 +111,6 @@
 raise :: Substitute a => Int -> a -> a
 raise n = subst (wkS n)
 
-{- TODO!?
-
--- | Application
-
-class Substitute a => Apply a where
-  applyE     :: a -> Elims -> a
-  applyE t [] = t
-  applyE t es = substApply t idS es
-
-  substApply :: a -> Subst -> Elims -> a
-  substApply t s es = subst s t `applyE` es
-
-instance Apply a => Apply [a] where
-  applyE ts es       = map (`applyE` es) ts
-  substApply ts s es = map (\ t -> substApply t s es) ts
-
-instance Apply a => Apply (Dom a) where
-  applyE ts es       = fmap (`applyE` es) ts
-  substApply ts s es = fmap (\ t -> substApply t s es) ts
-
-instance Apply a => Apply (Arg a) where
-  applyE ts es       = fmap (`applyE` es) ts
-  substApply ts s es = fmap (\ t -> substApply t s es) ts
-
-instance Apply a => Apply (Elim' a) where
-  applyE ts es       = fmap (`applyE` es) ts
-  substApply ts s es = fmap (\ t -> substApply t s es) ts
-
-instance Apply Term where
-  substApply t s es = case t of
-    -- Eliminations
-    Var i   -> lookupS s i `applyE` es
-    Def f   -> foldl App (Def f) es
-    App t u -> substApply t s $ Apply (subst s u) : es
-    -- Eliminateables
-
-    -- Types & non-eliminateables
-    Type l
-      | null es   -> Type $ subst s l
-      | otherwise -> __IMPOSSIBLE__
-    Size
-      | null es   -> Size
-      | otherwise -> __IMPOSSIBLE__
-    Nat a
-      | null es   -> Nat $ subst s a
-      | otherwise -> __IMPOSSIBLE__
-    Zero
-      | null es   -> Zero
-      | otherwise -> __IMPOSSIBLE__
-    Suc t
-      | null es   -> Suc $ subst s t
-      | otherwise -> __IMPOSSIBLE__
-    Infty
-      | null es   -> Infty
-      | otherwise -> __IMPOSSIBLE__
-    Pi u t
-      | null es   -> Pi (subst s u) $ subst s t
-      | otherwise -> __IMPOSSIBLE__
-
-instance Apply (Abs Term) where
-
-  substApply (Abs x t) s = \case
-    (Apply (Arg _ u) : es) -> substApply t (consS u s) es
-    _ -> __IMPOSSIBLE__
-
-  substApply (NoAbs x t) s = \case
-    (Apply _ : es) -> substApply t s es
-    _ -> __IMPOSSIBLE__
-
-
--}
-
-
 
 -- | Construct the type of the functional for fix.
 --
diff --git a/src/TypeChecker.hs b/src/TypeChecker.hs
--- a/src/TypeChecker.hs
+++ b/src/TypeChecker.hs
@@ -208,12 +208,6 @@
 
 checkSize :: A.Exp -> Check Size
 checkSize e = checkExp e VSize
--- checkSize = \case
---   A.Infty        -> return Infty
---   A.LZero        -> return $ sZero
---   A.App A.LSuc e -> sSuc <$> checkSize e
---   e@(A.Var x)    -> checkExp e VSize
---   e -> throwError $ "Not a valid size expression: " ++ printTree e
 
 checkLevel :: A.Exp -> Check Level
 checkLevel = \case
@@ -222,10 +216,6 @@
   e@(A.Var x)    -> checkExp e VSize
   e -> throwError $ "Not a valid level expression: " ++ printTree e
 
--- maxLevel :: A.Exp -> VLevel -> VLevel -> Check VLevel
--- maxLevel e l1 l2 = maybe failure return $ maxSize l1 l2
---   where failure = throwError $ "Cannot assign a universe level to type " ++ printTree e
-
 checkExp :: A.Exp -> VType -> Check Term
 checkExp e0 t = do
   case e0 of
@@ -250,8 +240,6 @@
           -- Infer the type of the case expression
           tt <- reifyType t
           -- Make sure that b is a successor size
-          -- let failNotSuc = throwError $ "Splitting Nat is only possible at successor size, when checking " ++ printTree e
-          -- a  <- maybe failNotSuc return $ sizePred b
           let a = fromMaybe __IMPOSSIBLE__ $ sizePred b
           ta <- reifySize a
           tz <- checkExp ez =<< applyClosure cl (VZero a)
@@ -270,7 +258,6 @@
     e -> do
       (u, ti) <- inferExp e
       coerce u ti t
-    -- e -> nyi $ "checking " ++ printTree e
 
 -- | Infers neutrals, natural numbers, types.
 
@@ -323,11 +310,6 @@
     u <- checkSize e
     return (sPlus u k, VSize)
 
-  -- (A.Plus x k, _) -> do
-  --   (u, t) <- inferId x
-  --   subType t VSize
-  --   return (sPlus u k, t)
-
   (A.Var A.Under, _) -> throwError "Illegal expression: _"
   (A.Var (A.Id x), _) -> inferId x
 
@@ -608,11 +590,6 @@
      traceM $ "lowerSemi " ++ show k ++ "  " ++ show t
      __IMPOSSIBLE__
 
--- antitone :: VGen -> VType -> Check Bool
--- antitone k t = do
---   traceM $ "\nantitone " ++ show k ++ "  " ++ show t
---   return True
-
 monotone :: VGen -> Bool -> VType -> Check Bool
 monotone k b t = do
   debug (if b then "monotone" else "antitone") k t
@@ -625,15 +602,6 @@
     VType a -> monotoneSize k b a
     VNat  a -> monotoneSize k b a
     VSize   -> return True
-    -- VInfty  -> return True
-    -- VZero _ -> return True
-    -- VSuc _ v -> monotone k b v
-    -- VLam cl  -> addContext ("#", VSize) $ do
-    --   u <- lastVal
-    --   monotone k b =<< applyClosure cl u
-    -- VUp _ (VNe k' es)
-    --   | k == k'   -> return b
-    --   | otherwise -> return True
     VUp (VType _) _ -> return True
     _ -> __IMPOSSIBLE__