diff --git a/.gitignore b/.gitignore
index 92dd3e9..0a5e8b5 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,3 @@
 .DS_Store
 .stack-work
-
+tags
diff --git a/Surface.cabal b/Surface.cabal
index c817b6f..c9b7106 100644
--- a/Surface.cabal
+++ b/Surface.cabal
@@ -23,8 +23,11 @@ library
                      , Data.Term
                      , Data.Term.Types
                      , Data.Typing
-                     , Data.Unification
                      , Surface
+                     , Surface.Language
+                     , Surface.Pair
+                     , Surface.Renaming
+                     , Surface.Unification
   build-depends:       base >= 4.7 && < 5
                      , containers
   default-language:    Haskell2010
@@ -44,6 +47,8 @@ test-suite Surface-test
   main-is:             Spec.hs
   other-modules:       Data.Name.Internal.Spec
                      , Data.Term.Spec
+                     , Surface.Language.Spec
+                     , Surface.Pair.Spec
                      , Test.Assertions
   build-depends:       base
                      , Surface
diff --git a/src/Data/Expression.hs b/src/Data/Expression.hs
index a806f9f..b75f360 100644
--- a/src/Data/Expression.hs
+++ b/src/Data/Expression.hs
@@ -1,15 +1,7 @@
 {-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable #-}
 module Data.Expression where
 
-import Data.Unification
-
 data Expression recur
   = Application recur recur
   | Lambda recur recur
   deriving (Functor, Show, Eq, Foldable, Traversable)
-
-instance Unifiable Expression where
-  unifyBy f expected actual = case (expected, actual) of
-    (Application a1 b1, Application a2 b2) -> Just $ Application (f a1 a2) (f b1 b2)
-    (Lambda a1 b1, Lambda a2 b2) -> Just $ Lambda (f a1 a2) (f b1 b2)
-    _ -> Nothing
diff --git a/src/Data/Module.hs b/src/Data/Module.hs
index b4d37e5..63f4736 100644
--- a/src/Data/Module.hs
+++ b/src/Data/Module.hs
@@ -1,7 +1,17 @@
+{-# LANGUAGE FlexibleContexts #-}
 module Data.Module where
 
-import Data.Expression
+import qualified Data.List as List
 import Data.Term.Types
-import qualified Data.Map as Map
+import Surface.Language
 
-data Module = Module (Map.Map String (Term Expression))
+(!) :: Module term -> String -> Definition term
+Module definitions ! key = case List.find ((== key) . symbol) definitions of
+  Just x -> x
+  _ -> error "Expected definition to exist"
+
+checkModule :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Context (Term f) -> Module (Term f) -> Result [Term f]
+checkModule context (Module definitions) = sequence $ checkDefinition context <$> definitions
+
+checkDefinition :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Context (Term f) -> Definition (Term f) -> Result (Term f)
+checkDefinition context (Definition symbol t v) = typeOf t _type' context >> typeOf v t context
diff --git a/src/Data/Term.hs b/src/Data/Term.hs
index 262914d..fca1dbc 100644
--- a/src/Data/Term.hs
+++ b/src/Data/Term.hs
@@ -5,7 +5,8 @@ import Data.Binding
 import Data.Name
 import Data.Typing
 import Data.Term.Types
-import Data.Unification
+import Surface.Renaming
+import Surface.Unification
 import qualified Data.Map as Map
 import qualified Data.Set as Set
 
@@ -21,9 +22,11 @@ abstract f = abstraction name scope
         name = maybe (Local 0) prime $ maxBoundVariable (f $ variable (Local $ negate 1))
 
 -- | Construct the annotation of a term by a type. The term will be checked against this type.
-annotation :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Term f -> Term f -> Term f
+annotation :: Foldable f => Term f -> Term f -> Term f
 annotation term type' = checkedTyping typeChecker $ Annotation term type'
-  where typeChecker against context = typeOf term type' context >>= expectUnifiable against
+  where typeChecker against context = do
+          _ <- typeOf term type' context
+          typeOf term against context
 
 
 checkedAbstraction :: Name -> Checker (Term f) -> Term f -> Term f
@@ -44,18 +47,9 @@ checkedBinding typeChecker = checkedTyping typeChecker . Binding
 checkedExpression :: Foldable f => Checker (Term f) -> f (Term f) -> Term f
 checkedExpression typeChecker = checkedBinding typeChecker . Expression
 
-_type :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Int -> Term f
-_type n = Term mempty (checkInferred $ const $ Right (_type (n + 1))) $ Type n
-
-_type' :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Term f
-_type' = _type 0
-
 implicit :: Term f
 implicit = Term mempty (const . Right) Implicit
 
-expectUnifiable :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Term f -> Term f -> Result (Term f)
-expectUnifiable expected actual = maybe (Left $ "error: Unification failed.\nExpected: '" ++ show expected ++ "'\n  Actual: '" ++ show actual ++ "'.\n") Right $ unified $ unify expected actual
-
 checkInferred :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Inferer (Term f) -> Checker (Term f)
 checkInferred inferer expected context = do
   actual <- inferer context
@@ -71,28 +65,6 @@ maxBoundVariable = cata $ \ t -> case t of
   Binding (Expression e) -> maximum e
   _ -> Nothing
 
-rename :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Name -> Name -> Term f -> Term f
-rename old new (Term freeVariables typeChecker typing) = Term (replace old new freeVariables) typeChecker $ renameTypingBy (rename old new) old new typing
-
-replace :: Ord a => a -> a -> Set.Set a -> Set.Set a
-replace old new set = if Set.member old set then Set.insert new $ Set.delete old set else set
-
-renameUnification :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Name -> Name -> Unification f -> Unification f
-renameUnification old new (Unification freeVariables out) = Unification (replace old new freeVariables) $ renameTypingBy (renameUnification old new) old new out
-renameUnification old new (Conflict expected actual) = Conflict (rename old new expected) (rename old new actual)
-
-renameTypingBy :: Functor f => (g f -> g f) -> Name -> Name -> Typing (Binding f) (g f) -> Typing (Binding f) (g f)
-renameTypingBy _ old new typing | old == new = typing
-renameTypingBy f old new typing = case typing of
-  Binding (Variable name) -> if name == old then Binding (Variable new) else typing
-  Binding (Abstraction name scope) -> if name == old then typing else Binding $ Abstraction name (f scope)
-  Binding (Expression body) -> Binding $ Expression $ f <$> body
-
-  Annotation a b -> Annotation (f a) (f b)
-
-  Type _ -> typing
-  Implicit -> typing
-
 substitute :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Name -> Term f -> Term f -> Term f
 substitute name with term | with == variable name = term
 substitute name with term@(Term _ typeChecker binding) = case binding of
@@ -129,32 +101,3 @@ cata f = f . fmap (cata f) . out
 para :: Functor f => (Typing (Binding f) (Term f, a) -> a) -> Term f -> a
 para f = f . fmap fanout . out
   where fanout a = (a, para f a)
-
-byUnifying :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Checker (Term f) -> Checker (Term f) -> Checker (Term f)
-byUnifying a b against context = do
-  a' <- a against context
-  b' <- b against context
-  maybe (Left "couldn’t unify") Right $ unified $ unify a' b'
-
-unify :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Term f -> Term f -> Unification f
-unify expected actual = case (out expected, out actual) of
-  (a, b) | a == b -> into expected
-
-  (_, Implicit) -> into expected
-  (Implicit, _) -> into actual
-
-  (Type _, Type _) -> into expected
-  (Annotation term1 type1, Annotation term2 type2) -> Unification free (Annotation (unify term1 term2) (unify type1 type2))
-
-  (Binding (Abstraction name1 scope1), Binding (Abstraction name2 scope2)) | name1 == name2 -> Unification free (Binding $ Abstraction name1 (unify scope1 scope2))
-  (Binding (Abstraction name1 scope1), Binding (Abstraction name2 scope2)) -> Unification (Set.delete name1 free) (Binding $ Abstraction name1 (renameUnification name name1 (unify (rename name1 name scope1) (rename name2 name scope2))))
-    where name = pick free
-          free = freeVariables scope1 `Set.union` freeVariables scope2
-
-  (Binding (Abstraction name scope), _) | Set.notMember name (freeVariables scope) -> unify scope actual
-  (_, Binding (Abstraction name scope)) | Set.notMember name (freeVariables scope) -> unify expected scope
-
-  (Binding (Expression e1), Binding (Expression e2)) | Just e <- unifyBy unify e1 e2 -> Unification free $ Binding $ Expression e
-
-  _ -> Conflict expected actual
-  where free = freeVariables expected `Set.union` freeVariables actual
diff --git a/src/Data/Term/Types.hs b/src/Data/Term/Types.hs
index 46a1318..03f231e 100644
--- a/src/Data/Term/Types.hs
+++ b/src/Data/Term/Types.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE StandaloneDeriving, UndecidableInstances #-}
+{-# LANGUAGE UndecidableInstances #-}
 module Data.Term.Types where
 
 import Data.Binding
@@ -9,35 +9,48 @@ import qualified Data.Set as Set
 
 type Result a = Either String a
 
+data Module term = Module [Definition term]
+data Definition term = Definition { symbol :: String, getType :: term, getValue :: term }
+
 type Context term = Map.Map Name term
+type Environment term = Map.Map Name term
 
 type Inferer term = Context term -> Result term
 type Checker term = term -> Context term -> Result term
 
 data Term f = Term { freeVariables :: Set.Set Name, typeOf :: Checker (Term f), out :: Typing (Binding f) (Term f) }
 
-data Unification f = Unification (Set.Set Name) (Typing (Binding f) (Unification f)) | Conflict (Term f) (Term f)
+data Unification f = Unification (Set.Set Name) (Checker (Term f)) (Typing (Binding f) (Unification f)) | Conflict (Term f) (Term f)
+
+class Unifiable e where
+  unifyBy :: (f e -> f e -> Unification e) -> e (f e) -> e (f e) -> Maybe (e (Unification e))
 
 expected :: Functor f => Unification f -> Term f
 expected (Conflict expected _) = expected
-expected (Unification freeVariables out) = Term freeVariables (const . const $ Left "Unification does not preserve typecheckers.\n") (expected <$> out)
+expected (Unification freeVariables typeChecker out) = Term freeVariables typeChecker (expected <$> out)
 
 actual :: Functor f => Unification f -> Term f
 actual (Conflict _ actual) = actual
-actual (Unification freeVariables out) = Term freeVariables (const . const $ Left "Unification does not preserve typecheckers.\n") (actual <$> out)
+actual (Unification freeVariables typeChecker out) = Term freeVariables typeChecker (actual <$> out)
 
 unified :: Traversable f => Unification f -> Maybe (Term f)
 unified (Conflict _ _) = Nothing
-unified (Unification freeVariables out) = do
+unified (Unification freeVariables typeChecker out) = do
   out <- mapM unified out
-  return $ Term freeVariables (const . const $ Left "Unification does not preserve typecheckers.\n") out
+  return $ Term freeVariables typeChecker out
 
 into :: Functor f => Term f -> Unification f
-into term = Unification (freeVariables term) $ into <$> out term
+into term = Unification (freeVariables term) (typeOf term) $ into <$> out term
 
 
 instance Eq (f (Term f)) => Eq (Term f) where
   a == b = freeVariables a == freeVariables b && out a == out b
 
-deriving instance (Eq (Term f), Eq (f (Unification f))) => Eq (Unification f)
-deriving instance (Show (Term f), Show (f (Unification f))) => Show (Unification f)
+instance (Eq (Term f), Eq (f (Unification f))) => Eq (Unification f) where
+  (Unification freeVariablesA _ outA) == (Unification freeVariablesB _ outB) = freeVariablesA == freeVariablesB && outA == outB
+  (Conflict a1 b1) == (Conflict a2 b2) = a1 == a2 && b1 == b2
+  _ == _ = False
+
+instance (Functor f, Show (Term f), Show (f (Unification f))) => Show (Unification f) where
+  show u = "Expected: " ++ show (expected u) ++ "\n"
+        ++ "  Actual: " ++ show (actual u) ++ "\n"
diff --git a/src/Data/Unification.hs b/src/Data/Unification.hs
deleted file mode 100644
index bbc0975..0000000
--- a/src/Data/Unification.hs
+++ /dev/null
@@ -1,6 +0,0 @@
-module Data.Unification where
-
-import Data.Term.Types
-
-class Unifiable e where
-  unifyBy :: (f e -> f e -> Unification e) -> e (f e) -> e (f e) -> Maybe (e (Unification e))
diff --git a/src/Surface.hs b/src/Surface.hs
index 76bb292..5e2deaa 100644
--- a/src/Surface.hs
+++ b/src/Surface.hs
@@ -1,119 +1,14 @@
-{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
 module Surface (
   module Surface',
-  lambda,
-  Surface.pi,
-  (-->),
-  apply,
-  checkHasFunctionType,
-  checkIsFunctionType,
-  checkIsType,
 ) where
 
-import Prelude hiding (pi)
 import Data.Binding as Surface'
 import Data.Expression as Surface'
+import Data.Module as Surface'
 import Data.Name as Surface'
-import Data.Name.Internal
 import Data.Term as Surface'
 import Data.Term.Types as Surface'
 import Data.Typing as Surface'
-import Data.Unification as Surface'
-import Control.Applicative
-import qualified Data.Set as Set
-
-infixr `lambda`
-
--- | Construct a lambda from a type and a function from an argument variable to the resulting term. The variable will be picked automatically. The parameter type will be checked against `Type`, but there are no constraints on the type of the result.
-lambda :: Term Expression -> (Term Expression -> Term Expression) -> Term Expression
-lambda t f = checkedExpression checkType $ Lambda t body
-  where body = abstract f
-        checkType expected context = case out expected of
-          Binding (Expression (Lambda from to)) -> checkTypeAgainst from to context
-          Type _ -> checkTypeAgainst _type' _type' context
-          _ -> checkTypeAgainst implicit implicit context >>= expectUnifiable expected
-        checkTypeAgainst from to context = do
-          _ <- checkIsType t context
-          _ <- expectUnifiable from t
-          bodyType <- inferTypeOf body (extendContext t context body)
-          _ <- expectUnifiable to bodyType
-          return $ case shadowing body bodyType of
-            Just name -> t `pi` \ v -> substitute name v bodyType
-            _ -> t --> bodyType
-
-infixr `pi`
-
--- | Construct a pi type from a type and a function from an argument variable to the resulting type. The variable will be picked automatically. The parameter type will be checked against `Type`, as will the substitution of the parameter type into the body.
-pi :: Term Expression -> (Term Expression -> Term Expression) -> Term Expression
-pi t f = checkedExpression checkType $ Lambda t body
-  where body = abstract f
-        checkType expected context = case out expected of
-          Binding (Expression (Lambda from to)) -> checkTypeAgainst from to context
-          Type _ -> checkTypeAgainst _type' _type' context
-          _ -> checkTypeAgainst implicit implicit context >>= expectUnifiable expected
-        checkTypeAgainst from to context = do
-          _ <- checkIsType t context
-          _ <- expectUnifiable from t
-          bodyType <- checkIsType body (extendContext t context body)
-          _ <- expectUnifiable to bodyType
-          return $ case shadowing body bodyType of
-            Just name -> t `pi` \ v -> substitute name v bodyType
-            _ -> t --> bodyType
-
-infixr -->
-
--- | Construct a non-dependent function type between two types. Both operands will be checked against `Type`.
-(-->) :: Term Expression -> Term Expression -> Term Expression
-a --> b = checkedExpression (checkInferred inferType) $ Lambda a b
-  where inferType context = do
-          a' <- checkIsType a context
-          b' <- checkIsType b context
-          return $ a' --> b'
-
--- | Construct the application of one term to another. The first argument will be checked as a function type, and the second will be checked against that type’s domain. The resulting type will be the substitution of the domain type into the body.
-apply :: Term Expression -> Term Expression -> Term Expression
-apply a b = checkedExpression (checkInferred inferType) $ Application a b
-  where inferType context = do
-          (type', body) <- checkHasFunctionType a context
-          _ <- typeOf b type' context
-          return $ applySubstitution type' body
-
-
-checkHasFunctionType :: Term Expression -> Context (Term Expression) -> Result (Term Expression, Term Expression)
-checkHasFunctionType term context = inferTypeOf term context >>= checkIsFunctionType
-
-checkIsFunctionType :: Term Expression -> Result (Term Expression, Term Expression)
-checkIsFunctionType type' = case out type' of
-  Binding (Expression (Lambda type' body)) -> return (type', body)
-  _ -> Left "Expected function type."
-
-instance Monoid a => Alternative (Either a) where
-  empty = Left mempty
-  Left a <|> Left b = Left $ a `mappend` b
-  Right a <|> _ = Right a
-  _ <|> Right b = Right b
-
-checkIsType :: Term Expression -> Inferer (Term Expression)
-checkIsType term context = typeOf term _type' context <|> typeOf term (_type' --> _type') context
-
-
-instance Show (Term Expression) where
-  show = fst . para (\ b -> case b of
-    Binding (Variable n) -> (show n, maxBound)
-    Binding (Abstraction _ (_, body)) -> body
-
-    Type 0 -> ("Type", maxBound)
-    Type n -> ("Type" ++ showNumeral "₀₁₂₃₄₅₆₇₈₉" n, maxBound)
-
-    Binding (Expression (Application (_, a) (_, b))) -> (wrap 4 (<=) a ++ " " ++ wrap 4 (<) b, 4)
-
-    Binding (Expression (Lambda (_, type') (Term _ _ (Binding (Abstraction name term)), body))) | Set.member name (freeVariables term) -> ("λ " ++ show name ++ " : " ++ wrap 3 (<) type' ++ " . " ++ wrap 3 (<=) body, 3)
-    Binding (Expression (Lambda (_, type') (Term _ _ (Binding (Abstraction _ _)), body))) -> ("λ _ : " ++ wrap 3 (<) type' ++ " . " ++ wrap 3 (<=) body, 3)
-    Binding (Expression (Lambda (_, type') (_, body))) -> (wrap 3 (<) type' ++ " → " ++ wrap 3 (<=) body, 3)
-
-    Implicit -> ("_", maxBound)
-    Annotation (_, term) (_, type') -> (wrap 3 (<=) term ++ " : " ++ wrap 3 (<) type', 3)
-
-    :: (String, Int))
-    where wrap i op (s, j) | i `op` j = s
-          wrap _ _ (s, _) = "(" ++ s ++ ")"
+import Surface.Language as Surface'
+import Surface.Renaming as Surface'
+import Surface.Unification as Surface'
diff --git a/src/Surface/Language.hs b/src/Surface/Language.hs
new file mode 100644
index 0000000..0e17003
--- /dev/null
+++ b/src/Surface/Language.hs
@@ -0,0 +1,141 @@
+{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}
+module Surface.Language where
+
+import Control.Applicative
+import Data.Binding
+import Data.Expression
+import Data.Name.Internal
+import Data.Term
+import Data.Term.Types
+import Data.Typing
+import Surface.Unification
+import Prelude hiding (pi)
+import qualified Data.Map as Map
+import qualified Data.Set as Set
+
+type Term' = Term Expression
+
+_type :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Int -> Term f
+_type n = Term mempty typeCheck $ Type n
+  where typeCheck expected _ = case out expected of
+          Implicit -> Right $ _type (n + 1)
+          Type _ -> Right expected
+          _ -> Left "Nope"
+
+_type' :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Term f
+_type' = _type 0
+
+
+infixr `lambda`
+
+-- | Construct a lambda from a type and a function from an argument variable to the resulting term. The variable will be picked automatically. The parameter type will be checked against `Type`, but there are no constraints on the type of the result.
+lambda :: Term' -> (Term' -> Term') -> Term'
+lambda t f = checkedExpression (checkFunctionType checkTypeAgainst) $ Lambda t body
+  where body = abstract f
+        checkTypeAgainst from to context = do
+          _ <- checkIsType t context
+          _ <- expectUnifiable from t
+          bodyType <- inferTypeOf body (extendContext t context body)
+          _ <- expectUnifiable to bodyType
+          return $ case shadowing body bodyType of
+            Just name -> t `pi` \ v -> substitute name v bodyType
+            _ -> t --> bodyType
+
+
+infixr `pi`
+
+-- | Construct a pi type from a type and a function from an argument variable to the resulting type. The variable will be picked automatically. The parameter type will be checked against `Type`, as will the substitution of the parameter type into the body.
+pi :: Term' -> (Term' -> Term') -> Term'
+pi t f = checkedExpression (checkFunctionType checkTypeAgainst) $ Lambda t body
+  where body = abstract f
+        checkTypeAgainst from to context = do
+          _ <- checkIsType t context
+          _ <- typeOf t from context
+          bodyType <- checkIsType body (extendContext t context body)
+          _ <- typeOf bodyType to context
+          return $ case shadowing body bodyType of
+            Just name -> t `pi` \ v -> substitute name v bodyType
+            _ -> t --> bodyType
+
+
+infixr -->
+
+-- | Construct a non-dependent function type between two types. Both operands will be checked against `Type`.
+(-->) :: Term' -> Term' -> Term'
+a --> b = checkedExpression (checkFunctionType checkTypeAgainst) $ Lambda a b
+  where checkTypeAgainst from to context = do
+          a' <- checkIsType a context
+          _ <- typeOf a from context
+          b' <- checkIsType b context
+          _ <- typeOf b to context
+          return $ a' --> b'
+
+-- | Construct the application of one term to another. The first argument will be checked as a function type, and the second will be checked against that type’s domain. The resulting type will be the substitution of the domain type into the body.
+apply :: Term' -> Term' -> Term'
+apply a b = checkedExpression (checkInferred inferType) $ Application a b
+  where inferType context = do
+          (type', body) <- checkHasFunctionType a context
+          _ <- typeOf b type' context
+          return $ applySubstitution type' body
+
+
+checkIsType :: Term' -> Inferer Term'
+checkIsType term = typeOf term _type'
+
+
+checkHasFunctionType :: Term' -> Context Term' -> Result (Term', Term')
+checkHasFunctionType term context = inferTypeOf term context >>= checkIsFunctionType
+
+checkIsFunctionType :: Term' -> Result (Term', Term')
+checkIsFunctionType type' = case out type' of
+  Binding (Expression (Lambda type' body)) -> return (type', body)
+  _ -> Left "Expected function type."
+
+
+checkFunctionType :: (Term' -> Term' -> Context Term' -> Result Term') -> Checker Term'
+checkFunctionType check expected context = case out expected of
+  Binding (Abstraction _ scope) -> checkFunctionType check scope context
+  Binding (Expression (Lambda from to)) -> check from to context
+  Type _ -> check _type' _type' context
+  _ -> check implicit implicit context >>= expectUnifiable expected
+
+
+weakHeadNormalForm :: Environment Term' -> Term' -> Term'
+weakHeadNormalForm environment term@(Term freeVariables typeChecker _) = case out term of
+  Binding (Variable name) -> case Map.lookup name environment of
+    Just v -> v
+    _ -> term
+
+  Binding (Expression (Application a b)) -> let normal = weakHeadNormalForm environment a in case out normal of
+    (Binding (Expression (Lambda _ body))) -> weakHeadNormalForm environment $ applySubstitution b body
+    _ -> Term freeVariables typeChecker $ Binding $ Expression $ Application normal b
+
+  _ -> term
+
+instance Monoid a => Alternative (Either a) where
+  empty = Left mempty
+  Left a <|> Left b = Left $ a `mappend` b
+  Right a <|> _ = Right a
+  _ <|> Right b = Right b
+
+
+instance Show Term' where
+  show = fst . para (\ b -> case b of
+    Binding (Variable n) -> (show n, maxBound)
+    Binding (Abstraction _ (_, body)) -> body
+
+    Type 0 -> ("Type", maxBound)
+    Type n -> ("Type" ++ showNumeral "₀₁₂₃₄₅₆₇₈₉" n, maxBound)
+
+    Binding (Expression (Application (_, a) (_, b))) -> (wrap 4 (<=) a ++ " " ++ wrap 4 (<) b, 4)
+
+    Binding (Expression (Lambda (_, type') (Term _ _ (Binding (Abstraction name term)), body))) | Set.member name (freeVariables term) -> ("λ " ++ show name ++ " : " ++ wrap 3 (<) type' ++ " . " ++ wrap 3 (<=) body, 3)
+    Binding (Expression (Lambda (_, type') (Term _ _ (Binding (Abstraction _ _)), body))) -> ("λ _ : " ++ wrap 3 (<) type' ++ " . " ++ wrap 3 (<=) body, 3)
+    Binding (Expression (Lambda (_, type') (_, body))) -> (wrap 3 (<) type' ++ " → " ++ wrap 3 (<=) body, 3)
+
+    Implicit -> ("_", maxBound)
+    Annotation (_, term) (_, type') -> (wrap 3 (<=) term ++ " : " ++ wrap 3 (<) type', 3)
+
+    :: (String, Int))
+    where wrap i op (s, j) | i `op` j = s
+          wrap _ _ (s, _) = "(" ++ s ++ ")"
diff --git a/src/Surface/Pair.hs b/src/Surface/Pair.hs
new file mode 100644
index 0000000..ae87e6a
--- /dev/null
+++ b/src/Surface/Pair.hs
@@ -0,0 +1,11 @@
+module Surface.Pair where
+
+import Data.Term.Types
+import Surface.Language
+
+_module :: Module Term'
+_module = Module [
+    Definition "Pair"
+      (_type' --> _type' --> _type')
+      (_type' `lambda` \ a -> _type' `lambda` \ b -> _type' `lambda` \ motive -> (a --> b --> motive) --> motive)
+  ]
diff --git a/src/Surface/Renaming.hs b/src/Surface/Renaming.hs
new file mode 100644
index 0000000..103b760
--- /dev/null
+++ b/src/Surface/Renaming.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE FlexibleContexts #-}
+module Surface.Renaming where
+
+import Data.Binding
+import Data.Name
+import Data.Term.Types
+import Data.Typing
+import qualified Data.Set as Set
+
+rename :: Functor f => Name -> Name -> Term f -> Term f
+rename old new (Term freeVariables typeChecker typing) = Term (replace old new freeVariables) typeChecker $ renameTypingBy (rename old new) old new typing
+
+replace :: Ord a => a -> a -> Set.Set a -> Set.Set a
+replace old new set = if Set.member old set then Set.insert new $ Set.delete old set else set
+
+renameUnification :: Functor f => Name -> Name -> Unification f -> Unification f
+renameUnification old new (Unification freeVariables typeChecker out) = Unification (replace old new freeVariables) typeChecker $ renameTypingBy (renameUnification old new) old new out
+renameUnification old new (Conflict expected actual) = Conflict (rename old new expected) (rename old new actual)
+
+renameTypingBy :: Functor f => (g f -> g f) -> Name -> Name -> Typing (Binding f) (g f) -> Typing (Binding f) (g f)
+renameTypingBy _ old new typing | old == new = typing
+renameTypingBy f old new typing = case typing of
+  Binding (Variable name) -> if name == old then Binding (Variable new) else typing
+  Binding (Abstraction name scope) -> if name == old then typing else Binding $ Abstraction name (f scope)
+  Binding (Expression body) -> Binding $ Expression $ f <$> body
+
+  Annotation a b -> Annotation (f a) (f b)
+
+  Type _ -> typing
+  Implicit -> typing
diff --git a/src/Surface/Unification.hs b/src/Surface/Unification.hs
new file mode 100644
index 0000000..fe82027
--- /dev/null
+++ b/src/Surface/Unification.hs
@@ -0,0 +1,48 @@
+{-# LANGUAGE FlexibleContexts #-}
+module Surface.Unification where
+
+import Data.Binding
+import Data.Expression
+import Data.Name
+import Data.Term.Types
+import Data.Typing
+import qualified Data.Set as Set
+import Surface.Renaming
+
+instance Unifiable Expression where
+  unifyBy f expected actual = case (expected, actual) of
+    (Application a1 b1, Application a2 b2) -> Just $ Application (f a1 a2) (f b1 b2)
+    (Lambda a1 b1, Lambda a2 b2) -> Just $ Lambda (f a1 a2) (f b1 b2)
+    _ -> Nothing
+
+byUnifying :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Checker (Term f) -> Checker (Term f) -> Checker (Term f)
+byUnifying a b against context = do
+  a' <- a against context
+  b' <- b against context
+  expectUnifiable a' b'
+
+unify :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Term f -> Term f -> Unification f
+unify expected actual = case (out expected, out actual) of
+  (a, b) | a == b -> into expected
+
+  (_, Implicit) -> into expected
+  (Implicit, _) -> into actual
+
+  (Type _, Type _) -> into expected
+  (Annotation term1 type1, Annotation term2 type2) -> Unification free (byUnifying (typeOf expected) (typeOf actual)) (Annotation (unify term1 term2) (unify type1 type2))
+
+  (Binding (Abstraction name1 scope1), Binding (Abstraction name2 scope2)) | name1 == name2 -> Unification free (byUnifying (typeOf expected) (typeOf actual)) (Binding $ Abstraction name1 (unify scope1 scope2))
+  (Binding (Abstraction name1 scope1), Binding (Abstraction name2 scope2)) -> Unification (Set.delete name1 free) (byUnifying (typeOf expected) (typeOf actual)) (Binding $ Abstraction name1 (renameUnification name name1 (unify (rename name1 name scope1) (rename name2 name scope2))))
+    where name = pick free
+          free = freeVariables scope1 `Set.union` freeVariables scope2
+
+  (Binding (Abstraction name scope), _) | Set.notMember name (freeVariables scope) -> unify scope actual
+  (_, Binding (Abstraction name scope)) | Set.notMember name (freeVariables scope) -> unify expected scope
+
+  (Binding (Expression e1), Binding (Expression e2)) | Just e <- unifyBy unify e1 e2 -> Unification free (byUnifying (typeOf expected) (typeOf actual)) $ Binding $ Expression e
+
+  _ -> Conflict expected actual
+  where free = freeVariables expected `Set.union` freeVariables actual
+
+expectUnifiable :: (Show (Term f), Unifiable f, Traversable f, Eq (f (Term f))) => Term f -> Term f -> Result (Term f)
+expectUnifiable expected actual = maybe (Left $ "error: Unification failed.\nExpected: '" ++ show expected ++ "'\n  Actual: '" ++ show actual ++ "'.\n") Right $ unified $ unify expected actual
diff --git a/stack.yaml b/stack.yaml
index d90b53b..143f078 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,7 +1,7 @@
 # For more information, see: https://github.com/commercialhaskell/stack/blob/release/doc/yaml_configuration.md
 
 # Specifies the GHC version and set of packages available (e.g., lts-3.5, nightly-2015-09-21, ghc-7.10.2)
-resolver: lts-3.15
+resolver: lts-4.0
 
 # Local packages, usually specified by relative directory name
 packages:
@@ -19,8 +19,6 @@ extra-package-dbs: []
 # Control whether we use the GHC we find on the path
 # system-ghc: true
 
-compiler-check: newer-minor
-
 # Require a specific version of stack, using version ranges
 # require-stack-version: -any # Default
 # require-stack-version: >= 0.1.10.0
diff --git a/test/Spec.hs b/test/Spec.hs
index 42ea78c..a6aa34c 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -1,49 +1,13 @@
-import Surface
 import qualified Data.Name.Internal.Spec
 import qualified Data.Term.Spec
-import qualified Data.Either as Either
-import Test.Assertions
+import qualified Surface.Language.Spec
+import qualified Surface.Pair.Spec
 import Test.Hspec
-import Test.Hspec.QuickCheck
+
 
 main :: IO ()
 main = hspec . parallel $ do
   describe "Data.Name.Internal" Data.Name.Internal.Spec.spec
   describe "Data.Term" Data.Term.Spec.spec
-
-  describe "lambda" $ do
-    it "produces binding abstractions" $
-      lambda _type' id `shouldBe` Term mempty (typeOf implicit) (Binding $ Expression $ Lambda _type' (abstraction (Local 0) $ variable (Local 0)))
-
-    it "picks fresh names" $
-      (_type' `lambda` const (_type' `lambda` const _type')) `shouldBe` Term mempty (typeOf implicit) (Binding $ Expression $ Lambda _type' $ abstraction (Local 1) $ Term mempty (typeOf implicit) $ Binding $ Expression $ Lambda _type' $ abstraction (Local 0) _type')
-
-    it "rejects non-Type types" $
-      inferTypeOf (lambda _type' $ \ a -> lambda a $ \ a' -> lambda a' $ const _type') mempty `shouldSatisfy` Either.isLeft
-
-  describe "apply" $ do
-    it "rejects non-function operators" $
-      inferTypeOf (apply _type' _type') mempty `shouldSatisfy` Either.isLeft
-
-    it "typechecks as its operator’s return type" $
-      inferTypeOf (apply (_type' `lambda` \ t -> t `lambda` id) _type') mempty `shouldResult` _type 0 --> _type 0
-
-  describe "-->" $ do
-    it "rejects non-Type parameter types" $
-      inferTypeOf (lambda _type' $ \ a -> lambda a $ \ a' -> a' --> a) mempty `shouldSatisfy` Either.isLeft
-
-    it "rejects non-Type return types" $
-      inferTypeOf (lambda _type' $ \ a -> lambda a $ \ a' -> a --> a') mempty `shouldSatisfy` Either.isLeft
-
-    it "associates to the right" $
-      _type' --> _type' --> _type' `shouldBe` _type' --> (_type' --> _type')
-
-    it "is not associative" $
-      (_type' --> _type') --> _type' `shouldNotBe` _type' --> (_type' --> _type')
-
-  describe "checkIsType" $ do
-    prop "matches Type" $
-      \ n -> checkIsType (_type n) mempty `shouldResult` _type'
-
-    prop "matches function types" $
-      \ m n -> checkIsType (_type m --> _type n) mempty `shouldResult` (_type' --> _type')
+  describe "Surface.Language" Surface.Language.Spec.spec
+  describe "Surface.Pair" Surface.Pair.Spec.spec
diff --git a/test/Surface/Language/Spec.hs b/test/Surface/Language/Spec.hs
new file mode 100644
index 0000000..437187e
--- /dev/null
+++ b/test/Surface/Language/Spec.hs
@@ -0,0 +1,46 @@
+module Surface.Language.Spec where
+
+import Surface
+import qualified Data.Either as Either
+import Test.Assertions
+import Test.Hspec
+import Test.Hspec.QuickCheck
+
+spec :: Spec
+spec = do
+  describe "lambda" $ do
+    it "produces binding abstractions" $
+      lambda _type' id `shouldBe` Term mempty (typeOf implicit) (Binding $ Expression $ Lambda _type' (abstraction (Local 0) $ variable (Local 0)))
+
+    it "picks fresh names" $
+      (_type' `lambda` const (_type' `lambda` const _type')) `shouldBe` Term mempty (typeOf implicit) (Binding $ Expression $ Lambda _type' $ abstraction (Local 1) $ Term mempty (typeOf implicit) $ Binding $ Expression $ Lambda _type' $ abstraction (Local 0) _type')
+
+    it "rejects non-Type types" $
+      inferTypeOf (_type' `lambda` \ b -> b `lambda` \ a -> a `lambda` const _type') mempty `shouldSatisfy` Either.isLeft
+
+  describe "apply" $ do
+    it "rejects non-function operators" $
+      inferTypeOf (apply _type' _type') mempty `shouldSatisfy` Either.isLeft
+
+    it "typechecks as its operator’s return type" $
+      inferTypeOf (apply (_type' `lambda` \ t -> t `lambda` id) _type') mempty `shouldResult` _type 0 --> _type 0
+
+  describe "-->" $ do
+    it "rejects non-Type parameter types" $
+      inferTypeOf (_type' `lambda` \ a -> a `lambda` \ a' -> a' --> a) mempty `shouldSatisfy` Either.isLeft
+
+    it "rejects non-Type return types" $
+      inferTypeOf (_type' `lambda` \ a -> a `lambda` \ a' -> a --> a') mempty `shouldSatisfy` Either.isLeft
+
+    it "associates to the right" $
+      _type' --> _type' --> _type' `shouldBe` _type' --> (_type' --> _type')
+
+    it "is not associative" $
+      (_type' --> _type') --> _type' `shouldNotBe` _type' --> (_type' --> _type')
+
+  describe "checkIsType" $ do
+    prop "matches Type" $
+      \ n -> checkIsType (_type n) mempty `shouldResult` _type'
+
+    prop "matches function types" $
+      \ m n -> checkIsType (_type m --> _type n) mempty `shouldResult` (_type' --> _type')
diff --git a/test/Surface/Pair/Spec.hs b/test/Surface/Pair/Spec.hs
new file mode 100644
index 0000000..650cd6f
--- /dev/null
+++ b/test/Surface/Pair/Spec.hs
@@ -0,0 +1,19 @@
+module Surface.Pair.Spec where
+
+import Prelude hiding (pi)
+import qualified Data.Either as Either
+import Surface
+import Surface.Pair
+import Test.Hspec
+
+spec :: Spec
+spec = do
+  describe "_module" $ do
+    it "typechecks" $
+      checkModule mempty _module `shouldSatisfy` Either.isRight
+
+  describe "Pair" $ do
+    it "has an inferable type" $
+      inferTypeOf (getValue _Pair) mempty `shouldSatisfy` Either.isRight
+
+  where _Pair = _module ! "Pair"