diff --git a/src/Curve.hs b/src/Curve.hs
index 47b2476..974ac6e 100644
--- a/src/Curve.hs
+++ b/src/Curve.hs
@@ -1,9 +1,10 @@
-{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances #-}
+{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, FlexibleInstances, UndecidableInstances #-}
 module Curve where
 
 import Data.Functor.Classes
 import qualified Data.List as List
 import qualified Data.Set as Set
+import qualified Data.Map as Map
 
 data Name
   = Local Int
@@ -27,36 +28,36 @@ type Unification' = Unification Expression
 
 -- DSL for constructing terms
 
-type' :: Term'
-type' = Term Type
+type' :: Roll r => r Expression
+type' = roll Type
 
-implicit :: Term'
-implicit = Term Implicit
+implicit :: Roll r => r Expression
+implicit = roll Implicit
 
-variable :: Name -> Term'
-variable = Term . Variable
+variable :: Roll r => Name -> r Expression
+variable = roll . Variable
 
-local :: Int -> Term'
+local :: Roll r => Int -> r Expression
 local = variable . Local
 
-global :: String -> Term'
+global :: Roll r => String -> r Expression
 global = variable . Global
 
 infixl 9 `apply`
 
-apply :: Term' -> Term' -> Term'
-apply a = Term . Application a
+apply :: Roll r => r Expression -> r Expression -> r Expression
+apply a = roll . Application a
 
 infixr `lambda`
 
-lambda :: Term' -> (Term' -> Term') -> Term'
-lambda t f = Term $ Lambda i t body
+lambda :: (Roll r, PartialUnroll r) => r Expression -> (r Expression -> r Expression) -> r Expression
+lambda t f = roll $ Lambda i t body
   where i = maybe 0 succ $ maxBoundVariable body
-        body = f (Term $ Variable $ Local i)
+        body = f (local i)
 
 infixr -->
 
-(-->) :: Term' -> Term' -> Term'
+(-->) :: (Roll r, PartialUnroll r) => r Expression -> r Expression -> r Expression
 a --> b = a `lambda` const b
 
 infixr `pi`
@@ -72,67 +73,127 @@ into term = Unification $ into <$> out term
 
 unified :: Unification' -> Maybe Term'
 unified (Unification expression) = Term <$> traverse unified expression
-unified (Conflict _ _) = Nothing
+unified _ = Nothing
+
+expected :: Unification' -> Term'
+expected (Unification out) = Term $ expected <$> out
+expected (Conflict a _) = a
+
+actual :: Unification' -> Term'
+actual (Unification out) = Term $ actual <$> out
+actual (Conflict _ b) = b
 
 
 -- Binding
 
-rename :: Int -> Int -> Term' -> Term'
+rename :: (Roll r, PartialUnroll r) => Name -> Name -> r Expression -> r Expression
 rename old new term | old == new = term
-rename old new term = Term $ case out term of
-  Variable (Local name) | name == old -> Variable $ Local new
-  Lambda name t b -> if name == old
+rename old new term = case unrollMaybe term of
+  Just (Variable name) | name == old -> variable new
+  Just (Lambda name t b) -> roll $ if Local name == old
     then Lambda name (rename old new t) b
     else Lambda name (rename old new t) (rename old new b)
-  Application a b -> Application (rename old new a) (rename old new b)
-  other -> other
-
-substitute :: Int -> Term' -> Term' -> Term'
-substitute name withTerm inScope = case out inScope of
-  Variable (Local n) | n == name -> withTerm
-  Lambda n inType inBody -> if n == name
-    then Term $ Lambda n (substitute name withTerm inType) inBody
-    else Term $ Lambda n (substitute name withTerm inType) (substitute name withTerm inBody)
-  Application inA inB -> Term $ Application (substitute name withTerm inA) (substitute name withTerm inB)
+  Just (Application a b) -> rename old new a `apply` rename old new b
+  _ -> term
+
+substitute :: (Roll r, PartialUnroll r) => Int -> r Expression -> r Expression -> r Expression
+substitute name withTerm inScope = case unrollMaybe inScope of
+  Just (Variable (Local n)) | n == name -> withTerm
+  Just (Lambda n inType inBody) -> if n == name
+    then roll $ Lambda n (substitute name withTerm inType) inBody
+    else roll $ Lambda n (substitute name withTerm inType) (substitute name withTerm inBody)
+  Just (Application inA inB) -> roll $ Application (substitute name withTerm inA) (substitute name withTerm inB)
   _ -> inScope
 
-unify :: Term' -> Term' -> Unification'
-unify expected actual = case (out expected, out actual) of
-  (_, Implicit) -> into expected
-  (Implicit, _) -> into actual
+applySubstitution :: (Roll r, PartialUnroll r) => r Expression -> r Expression -> r Expression
+applySubstitution withTerm body = case unrollMaybe body of
+  Just (Lambda i _ inScope) -> substitute i withTerm inScope
+  _ -> body
 
-  (Type, Type) -> into expected
 
-  (Variable n1, Variable n2) | n1 == n2 -> Unification $ Variable n2
-  (Application a1 b1, Application a2 b2) -> Unification $ Application (unify a1 a2) (unify b1 b2)
-  (Lambda i1 a1 b1, Lambda i2 a2 b2) | i1 == i2 -> Unification $ Lambda i2 (unify a1 a2) (unify b1 b2)
+freeVariables :: Term' -> Set.Set Name
+freeVariables = cata $ \ expression -> case expression of
+  Variable name -> Set.singleton name
+  Lambda i t b -> Set.delete (Local i) b `Set.union` t
+  Application a b -> a `Set.union` b
+  _ -> mempty
 
-  _ -> Conflict expected actual
+maxBoundVariable :: PartialUnroll r => r Expression -> Maybe Int
+maxBoundVariable = foldl maximal Nothing . unrollMaybe
+  where maximal into (Lambda i t _) = max into $ max (Just i) (maxBoundVariable t)
+        maximal into (Application a b) = max into $ max (maxBoundVariable a) (maxBoundVariable b)
+        maximal into _ = into
 
 
-freeVariables :: Term' -> Set.Set Name
-freeVariables = cata inExpression
-  where inExpression expression = case expression of
-          Variable name -> Set.singleton name
-          Lambda i t b -> Set.delete (Local i) b `Set.union` t
-          Application a b -> a `Set.union` b
-          _ -> mempty
+alphaEquivalent :: Term' -> Term' -> Bool
+alphaEquivalent a b | a == b = True
+alphaEquivalent (Term (Variable _)) (Term (Variable _)) = True
+alphaEquivalent (Term (Application a1 b1)) (Term (Application a2 b2)) = alphaEquivalent a1 a2 && alphaEquivalent b1 b2
+alphaEquivalent (Term (Lambda _ t1 b1)) (Term (Lambda _ t2 b2)) = alphaEquivalent t1 t2 && alphaEquivalent b1 b2
+alphaEquivalent _ _ = False
+
+
+-- Naming
+
+freshBy :: (Name -> Bool) -> Name -> Name
+freshBy isUsed name = if isUsed name then freshBy isUsed (prime name) else name
+
+freshIn :: Set.Set Name -> Name -> Name
+freshIn names = freshBy (`Set.member` names)
+
+prime :: Name -> Name
+prime (Local i) = Local $ succ i
+prime (Global s) = Global $ s ++ "ʹ"
+
+pick :: Set.Set Name -> Name
+pick names = freshIn names (maximum $ Set.insert (Local 0) names)
+
+
+-- Typechecking
+
+type Context = Map.Map Name Term'
+
+infer :: Context -> Term' -> Unification'
+infer = check implicit
+
+check :: Term' -> Context -> Term' -> Unification'
+check expected context term = case (out term, out expected) of
+  (Type, Implicit) -> Unification Type
+
+  (Variable name, Implicit) -> maybe (Conflict implicit implicit) into (Map.lookup name context)
+
+  (Application a b, Implicit) -> let a' = infer context a in case a' of
+    Unification (Lambda _ from to) -> case unified from of
+      Just from -> applySubstitution (check from context b) to
+      _ -> a' `apply` infer context b
+    _ -> a' `apply` infer context b
+
+  (Lambda i t body, Implicit) -> (check type' context t >> into t) `lambda` \ v -> substitute i v (infer (Map.insert (Local i) t context) body)
 
-maxBoundVariable :: Term' -> Maybe Int
-maxBoundVariable = cata (\ expression -> case expression of
-  Lambda n t _ -> max (Just n) t
-  Application a b -> max a b
-  _ -> Nothing)
+  (_, Implicit) -> Conflict implicit implicit
 
+  (Lambda {}, Type) -> check (type' --> type') context term
 
--- Recursion schemes
+  (_, _) -> let unification = infer context term in
+    maybe unification (unify expected) $ unified unification
+  where Unification _ >> b = b
+        a >> _ = a
 
-cata :: Functor f => (f a -> a) -> Term f -> a
-cata f = f . fmap (cata f) . out
 
-para :: Functor f => (f (Term f, a) -> a) -> Term f -> a
-para f = f . fmap fanout . out
-  where fanout a = (a, para f a)
+-- Equality
+
+unify :: Term' -> Term' -> Unification'
+unify expected actual = case (out expected, out actual) of
+  (_, Implicit) -> into expected
+  (Implicit, _) -> into actual
+
+  (Type, Type) -> into expected
+
+  (Variable _, Variable _) -> into expected
+  (Application a1 b1, Application a2 b2) -> unify a1 a2 `apply` unify b1 b2
+  (Lambda i a1 b1, Lambda _ a2 b2) -> Unification $ Lambda i (unify a1 a2) (unify b1 b2)
+
+  _ -> Conflict expected actual
 
 
 -- Numerals
@@ -149,6 +210,23 @@ showNumeral "" _ = ""
 showNumeral alphabet i = List.genericIndex alphabet <$> digits (List.genericLength alphabet) i
 
 
+-- Classes
+
+class Roll g where
+  roll :: f (g f) -> g f
+
+class Unroll r where
+  unroll :: r f -> f (r f)
+
+class PartialUnroll r where
+  unrollMaybe :: r f -> Maybe (f (r f))
+
+class Catamorphable r where
+  cata :: Functor f => (f a -> a) -> r f -> a
+
+  para :: Functor f => (f (r f, a) -> a) -> r f -> a
+
+
 -- Instances
 
 instance Show Name where
@@ -193,3 +271,25 @@ instance Show Unification' where
   show (Unification out) = show out
   show (Conflict a b) = "Expected: " ++ show a ++ "\n"
                      ++ "  Actual: " ++ show b ++ "\n"
+
+instance Roll Term where
+  roll = Term
+
+instance Unroll Term where
+  unroll = out
+
+instance PartialUnroll Term where
+  unrollMaybe = Just . unroll
+
+instance Roll Unification where
+  roll = Unification
+
+instance Unroll r => Catamorphable r where
+  cata f = f . fmap (cata f) . unroll
+
+  para f = f . fmap fanout . unroll
+    where fanout a = (a, para f a)
+
+instance PartialUnroll Unification where
+  unrollMaybe (Unification expression) = Just expression
+  unrollMaybe _ = Nothing
diff --git a/test/Spec.hs b/test/Spec.hs
index 9a74ca9..e858a15 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -1,4 +1,5 @@
 {-# LANGUAGE FlexibleInstances #-}
+import qualified Data.Map as Map
 import qualified Data.Set as Set
 import Test.Hspec
 import Test.Hspec.QuickCheck
@@ -14,7 +15,7 @@ instance Arbitrary (Term Expression) where
               (4, pure (Term Type))
             : (4, pure (Term Implicit))
             : (1, Term <$> (Application <$> inScope names <*> inScope names))
-            : (1, Term <$> (Lambda (length names) <$> inScope names <*> inScope (Local (length names) : names)))
+            : (2, Term <$> (Lambda (length names) <$> inScope names <*> inScope (Local (length names) : names)))
             : ((,) 4 . pure . Term . Variable <$> names)
 
   shrink term = filter (/= term) $ case out term of
@@ -37,6 +38,19 @@ main = hspec $ do
     prop "symmetry" $
       \ a b -> a `unify` b `shouldBe` flipUnification (b `unify` a)
 
+    prop "expected term is recoverable" $
+      \ a b -> expected (replace implicit type' a `unify` b) `shouldSatisfy` alphaEquivalent (replace implicit type' a)
+
+    prop "actual term is recoverable" $
+      \ a b -> actual (a `unify` replace implicit type' b) `shouldSatisfy` alphaEquivalent (replace implicit type' b)
+
+  describe "alphaEquivalent" $ do
+    prop "identical terms are alpha-equivalent" $
+      \ a -> a `alphaEquivalent` a `shouldBe` True
+
+    prop "free variables are alpha-equivalent" $
+      \ n -> variable n `alphaEquivalent` variable (prime n) `shouldBe` True
+
   describe "freeVariables" $ do
     prop "variables are free in themselves" $
       \ name -> freeVariables (variable name) `shouldBe` Set.singleton name
@@ -44,9 +58,34 @@ main = hspec $ do
     prop "lambdas are shadowing" $
       \ name t b -> freeVariables (Term (Lambda name t b)) `shouldSatisfy` Set.notMember (Local name)
 
+  describe "check" $ do
+    prop "checking against implicit is inference" $
+      \ term -> check implicit mempty term `shouldBe` infer mempty term
+
+    prop "infers free variables as conflicts" $
+      \ name -> infer mempty (variable name) `shouldBe` Conflict implicit implicit
+
+    prop "infers bound variables from the context" $
+      \ name t -> infer (Map.singleton name t) (variable name) `shouldBe` into t
+
+    prop "checks inferred types" $
+      \ name t -> check t (Map.singleton name t) (variable name) `shouldBe` into t
+
+    it "infers constant function types" $
+      infer mempty (type' `lambda` const type') `shouldBe` type' --> type'
+
+    it "infers function types" $
+      infer mempty (type' `lambda` id) `shouldBe` type' --> type'
+
+    it "infers identity’s type" $
+      infer mempty (type' `lambda` \ a -> a `lambda` id) `shouldBe` (type' `lambda` \ a -> a --> a)
+
+    it "infers constant’s type" $
+      infer mempty (type' `lambda` \ a -> type' `lambda` \ b -> a `lambda` \ a' -> b `lambda` const a') `shouldBe` (type' `lambda` \ a -> type' `lambda` \ b -> a --> b --> a)
+
   describe "showsLevelPrec" $ do
     prop "parenthesizes right-nested applications" $
-      \ a b c -> show (apply a (apply b c)) `shouldBe` showsPrec 10 a " (" ++ showsPrec 10 (apply b c) ")"
+      \ a b c -> show (apply a (apply b c)) `shouldBe` showsPrec 10 a " (" ++ showsPrec 10 (apply b c :: Term') ")"
 
     prop "shows non-dependent function types with an arrow operator" $
       \ a b -> showsLevelPrec True 0 (Term $ Lambda 0 a b) "" `shouldBe` showsLevelPrec True 1 a " → " ++ showsType b ""
@@ -57,27 +96,43 @@ main = hspec $ do
     prop "shows dependent function types with a binding arrow operator" $
       \ a n -> showsType (Term $ Lambda n a (local n)) "" `shouldBe` "(" ++ shows (Local n) " : " ++ showsType a ") → " ++ showsType (local n) ""
 
-    prop "parentheses left-nested non-dependent function types" $
+    prop "parenthesizes left-nested non-dependent function types" $
       \ a b c -> showsLevelPrec True 0 (Term $ Lambda 0 (Term $ Lambda 1 a b) c) "" `shouldBe` "(" ++ showsLevelPrec True 0 (Term $ Lambda 1 a b) ") → " ++ showsType c ""
 
     prop "pretty-prints Implicit as _ at any level and precedence" $
       \ isType prec -> showsLevelPrec isType prec implicit "" `shouldBe` "_"
 
     prop "pretty-prints local variables alphabetically" $
-      \ i -> show (local i) `shouldBe` showNumeral ['a'..'z'] i
+      \ i -> show (local i :: Term') `shouldBe` showNumeral ['a'..'z'] i
 
     it "should format the identity function appropriately" $
       show (Term $ Lambda 1 type' $ Term $ Lambda 0 (local 1) (local 0)) `shouldBe` "λ b : Type . λ a : b . a"
 
+  describe "rename" $ do
+    prop "shadowed variables are not renamed" $
+      \ i t body -> let name = Local i in rename name (prime name) (Term $ Lambda i t body) `shouldBe` (Term $ Lambda i (rename name (prime name) t) body)
+
+    prop "renaming is injective" $
+      \ n term -> rename (prime n) n (rename n (prime n) term) `shouldBe` (term :: Term')
+
+  describe "prime" $ do
+    prop "injectivity over locals" $
+      \ i -> prime (Local i) `shouldNotBe` Local i
+
+    prop "injectivity over globals" $
+      \ s -> prime (Global s) `shouldNotBe` Global s
+
   describe "DSL" $ do
     prop "apply associates leftwards" $
-      \ a b c -> a `apply` b `apply` c `shouldBe` (a `apply` b) `apply` c
+      \ a b c -> a `apply` b `apply` c `shouldBe` (a `apply` b) `apply` (c :: Term')
 
     prop "--> associates rightwards" $
-      \ a b c -> a --> b --> c `shouldBe` a --> (b --> c)
+      \ a b c -> a --> b --> c `shouldBe` a --> (b --> c :: Term')
 
     it "lambda avoids shadowing" $
-      show (type' `lambda` \ b -> b `lambda` id) `shouldBe` "λ b : Type . λ a : b . a"
+      show (type' `lambda` \ b -> b `lambda` id :: Term') `shouldBe` "λ b : Type . λ a : b . a"
 
   where flipUnification (Conflict a b) = Conflict b a
         flipUnification (Unification out) = Unification $ flipUnification <$> out
+
+        replace needle withTerm inHaystack = if needle == inHaystack then withTerm else Term $ replace needle withTerm <$> out inHaystack