diff --git a/abt.cabal b/abt.cabal
--- a/abt.cabal
+++ b/abt.cabal
@@ -1,5 +1,5 @@
 name:                abt
-version:             0.1.0.1
+version:             0.1.0.2
 synopsis:            Abstract binding trees for Haskell
 description:         A Haskell port of the Carnegie Mellon ABT library (SML), with some improvements.
 license:             MIT
@@ -23,6 +23,7 @@
                        Abt.Tutorial
   build-depends:       base >=4.7 && <4.8,
                        vinyl >=0.5,
+                       profunctors >=4.3.2,
                        transformers
   ghc-options:         -Wall
   hs-source-dirs:      src
diff --git a/src/Abt/Class/Abt.hs b/src/Abt/Class/Abt.hs
--- a/src/Abt/Class/Abt.hs
+++ b/src/Abt/Class/Abt.hs
@@ -99,7 +99,7 @@
     oe ← out e
     case oe of
       V v → return [v]
-      v :\ e' → do
+      v :\ e' →
         L.delete v <$>
           freeVars e'
       _ :$ es →
@@ -119,6 +119,7 @@
       v :\ e' → do
         estr ← toString e'
         return $ show v ++ "." ++ estr
+      o :$ RNil → return $ show1 o
       o :$ es → do
         es' ← sequence . recordToList $ Const . toString <<$>> es
         return $ show1 o ++ "[" ++ L.intercalate ";" es' ++ "]"
diff --git a/src/Abt/Class/HEq1.hs b/src/Abt/Class/HEq1.hs
--- a/src/Abt/Class/HEq1.hs
+++ b/src/Abt/Class/HEq1.hs
@@ -1,19 +1,42 @@
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UnicodeSyntax #-}
 
 module Abt.Class.HEq1 where
 
+import Control.Applicative
 import Data.Vinyl
 
+-- | Essentially, Martin-Löf's identity type.
+--
+data a :=: b where
+  Refl ∷ a :=: a
+
+-- | Type constructors are extensional.
+--
+cong ∷ a :=: b → f a :=: f b
+cong Refl = Refl
+
 -- | Uniform variant of 'Eq' for indexed types. This is different from
 -- 'Data.Functor.Eq1' in that it is properly kind polymorphic and crucially
--- heterogeneous, and it places no constraint on the index.
+-- heterogeneous, and it places no constraint on the index. Because it is
+-- heterogeneous, it is useful to project equality in the base space from
+-- equality in the total space.
 --
 class HEq1 f where
+  -- | When both sides are equal, give in addition a proof that their indices
+  -- are equal; otherwise return 'Nothing'.
+  --
+  heq1 ∷ f i → f j → Maybe (i :=: j)
+
+  -- | A boolean version of 'heq1', which must agree with it.
+  --
   (===) ∷ f i → f j → Bool
+  x === y = maybe False (const True) $ heq1 x y
 
 instance HEq1 el ⇒ HEq1 (Rec el) where
-  RNil === RNil = True
-  (x :& xs) === (y :& ys) = x === y && xs === ys
-  _ === _ = False
+  heq1 RNil RNil = Just Refl
+  heq1 (x :& xs) (y :& ys)
+    | Just Refl ← heq1 x y = cong <$> heq1 xs ys
+  heq1 _ _ = Nothing
diff --git a/src/Abt/Concrete/LocallyNameless.hs b/src/Abt/Concrete/LocallyNameless.hs
--- a/src/Abt/Concrete/LocallyNameless.hs
+++ b/src/Abt/Concrete/LocallyNameless.hs
@@ -9,6 +9,7 @@
 module Abt.Concrete.LocallyNameless
 ( Tm(..)
 , Tm0
+, _TmOp
 , Var(..)
 , varName
 , varIndex
@@ -22,6 +23,7 @@
 import Abt.Class.Monad
 
 import Control.Applicative
+import Data.Profunctor
 import Data.Vinyl
 
 -- | A variable is a De Bruijn index, optionally decorated with a display name.
@@ -44,7 +46,7 @@
 -- | A lens for '_varName'.
 --
 -- @
--- varName ∷ Lens' 'Var' ('Maybe' 'String')
+-- 'varName' ∷ Lens' 'Var' ('Maybe' 'String')
 -- @
 --
 varName
@@ -59,7 +61,7 @@
 -- | A lens for '_varIndex'.
 --
 -- @
--- varIndex ∷ Lens' 'Var' 'Int'
+-- 'varIndex' ∷ Lens' 'Var' 'Int'
 -- @
 --
 varIndex
@@ -84,11 +86,13 @@
 type Tm0 o = Tm o Z
 
 instance HEq1 o ⇒ HEq1 (Tm o) where
-  Free v1 === Free v2 = v1 == v2
-  Bound m === Bound n = m == n
-  Abs e1 === Abs e2 = e1 === e2
-  App o1 es1 === App o2 es2 = o1 === o2 && es1 === es2
-  _ === _ = False
+  heq1 (Free v1) (Free v2) | v1 == v2 = Just Refl
+  heq1 (Bound m) (Bound n) | m == n = Just Refl
+  heq1 (Abs e1) (Abs e2) = cong <$> heq1 e1 e2
+  heq1 (App o1 es1) (App o2 es2)
+    | Just Refl ← heq1 o1 o2
+    , Just Refl ← heq1 es1 es2 = Just Refl
+  heq1 _ _ = Nothing
 
 shiftVar
   ∷ Var
@@ -99,7 +103,7 @@
   Free v' → if v == v' then Bound n else Free v'
   Bound m → Bound m
   Abs e → Abs $ shiftVar v (n + 1) e
-  App p es → App p $ rmap (shiftVar v n) es
+  App p es → App p $ shiftVar v n <<$>> es
 
 addVar
   ∷ Var
@@ -110,7 +114,7 @@
   Free v' → Free v'
   Bound m → if m == n then Free v else Bound m
   Abs e → Abs $ addVar v (n + 1) e
-  App p es → App p $ rmap (addVar v n) es
+  App p es → App p $ addVar v n <<$>> es
 
 instance Show1 o ⇒ Abt Var o (Tm o) where
   into = \case
@@ -125,3 +129,23 @@
       v ← fresh
       return $ v :\ addVar v 0 e
     App p es → return $ p :$ es
+
+-- | A prism to extract arguments from a proposed operator.
+--
+-- @
+-- '_TmOp' ∷ 'HEq1' o ⇒ o ns → Prism' ('Tm0' o) ('Rec' ('Tm0' o) ns)
+-- @
+--
+_TmOp
+  ∷ ( Choice p
+    , Applicative f
+    , HEq1 o
+    )
+  ⇒ o ns
+  → p (Rec (Tm o) ns) (f (Rec (Tm o) ns))
+  → p (Tm0 o) (f (Tm0 o))
+_TmOp o = dimap fro (either pure (fmap (App o))) . right'
+  where
+    fro = \case
+      App o' es | Just Refl ← heq1 o o' → Right es
+      e → Left e
diff --git a/src/Abt/Tutorial.hs b/src/Abt/Tutorial.hs
--- a/src/Abt/Tutorial.hs
+++ b/src/Abt/Tutorial.hs
@@ -5,7 +5,9 @@
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE ViewPatterns #-}
 
 module Abt.Tutorial where
 
@@ -16,7 +18,9 @@
 import Control.Applicative
 import Control.Monad.Trans.State.Strict
 import Control.Monad.Trans.Maybe
+import Control.Monad.Trans.Except
 import Data.Vinyl
+import Prelude hiding (pi)
 
 -- | We'll start off with a monad in which to manipulate ABTs; we'll need some
 -- state for fresh variable generation.
@@ -48,19 +52,43 @@
 -- indexed by arities.
 --
 data Lang ns where
-  Lam ∷ Lang '[S Z]
-  Ap ∷ Lang '[Z,Z]
+  LAM ∷ Lang '[S Z]
+  APP ∷ Lang '[Z, Z]
+  PI ∷ Lang '[Z, S Z]
+  UNIT ∷ Lang '[]
+  AX ∷ Lang '[]
 
 instance Show1 Lang where
   show1 = \case
-    Lam → "lam"
-    Ap → "ap"
+    LAM → "lam"
+    APP → "ap"
+    PI → "pi"
+    UNIT → "unit"
+    AX → "<>"
 
 instance HEq1 Lang where
-  Lam === Lam = True
-  Ap === Ap = True
-  _ === _ = False
+  heq1 LAM LAM = Just Refl
+  heq1 APP APP = Just Refl
+  heq1 PI PI = Just Refl
+  heq1 UNIT UNIT = Just Refl
+  heq1 AX AX = Just Refl
+  heq1 _ _ = Nothing
 
+lam ∷ Tm Lang (S Z) → Tm0 Lang
+lam e = LAM $$ e :& RNil
+
+app ∷ Tm0 Lang → Tm0 Lang → Tm0 Lang
+app m n = APP $$ m :& n :& RNil
+
+ax ∷ Tm0 Lang
+ax = AX $$ RNil
+
+unit ∷ Tm0 Lang
+unit = UNIT $$ RNil
+
+pi ∷ Tm0 Lang → Tm Lang (S Z) → Tm0 Lang
+pi α xβ = PI $$ α :& xβ :& RNil
+
 -- | A monad transformer for small step operational semantics.
 --
 newtype StepT m α
@@ -86,12 +114,11 @@
   → StepT M (Tm0 Lang)
 step tm =
   out tm >>= \case
-    Ap :$ m :& n :& RNil →
+    APP :$ m :& n :& RNil →
       out m >>= \case
-        Lam :$ xe :& RNil → xe // n
+        LAM :$ xe :& RNil → xe // n
         _ → app <$> step m <*> pure n <|> app <$> pure m <*> step n
-          where
-            app a b = Ap $$ a :& b :& RNil
+    PI :$ α :& xβ :& RNil → pi <$> step α <*> pure xβ
     _ → stepsExhausted
 
 -- | The reflexive-transitive closure of a small-step operational semantics.
@@ -109,29 +136,87 @@
 eval ∷ Tm0 Lang → Tm0 Lang
 eval = runM . star step
 
+newtype JudgeT m α
+  = JudgeT
+  { runJudgeT ∷ ExceptT String m α
+  } deriving (Monad, Functor, Applicative, Alternative)
+
+instance MonadVar Var m ⇒ MonadVar Var (JudgeT m) where
+  fresh = JudgeT . ExceptT $ Right <$> fresh
+  named str = JudgeT . ExceptT $ Right <$> named str
+
+type Ctx = [(Var, Tm0 Lang)]
+
+raise ∷ Monad m ⇒ String → JudgeT m α
+raise = JudgeT . ExceptT . return . Left
+
+checkTy
+  ∷ Ctx
+  → Tm0 Lang
+  → Tm0 Lang
+  → JudgeT M ()
+checkTy g tm ty = do
+  let ntm = eval tm
+      nty = eval ty
+  (,) <$> out ntm <*> out nty >>= \case
+    (LAM :$ xe :& RNil, PI :$ α :& yβ :& RNil) → do
+      z ← fresh
+      ez ← xe // var z
+      βz ← yβ // var z
+      checkTy ((z,α):g) ez βz
+    (AX :$ RNil, UNIT :$ RNil) → return ()
+    _ → do
+      ty' ← inferTy g tm
+      if ty' === nty
+        then return ()
+        else raise "Type error"
+
+inferTy
+  ∷ Ctx
+  → Tm0 Lang
+  → JudgeT M (Tm0 Lang)
+inferTy g tm = do
+  out (eval tm) >>= \case
+    V v | Just (eval → ty) ← lookup v g → return ty
+        | otherwise → raise "Ill-scoped variable"
+    APP :$ m :& n :& RNil → do
+      inferTy g m >>= out >>= \case
+        PI :$ α :& xβ :& RNil → do
+          checkTy g n α
+          eval <$> xβ // n
+        _ → raise "Expected pi type for lambda abstraction"
+    _ → raise "Only infer neutral terms"
+
 -- | @λx.x@
 --
 identityTm ∷ M (Tm0 Lang)
 identityTm = do
   x ← fresh
-  return $ Lam $$ (x \\ var x) :& RNil
+  return $ lam (x \\ var x)
 
 -- | @(λx.x)(λx.x)@
 --
 appTm ∷ M (Tm0 Lang)
 appTm = do
   tm ← identityTm
-  return $ Ap $$ tm :& tm :& RNil
+  return $ app tm tm
 
 -- | A demonstration of evaluating (and pretty-printing). Output:
 --
 -- @
--- ap[lam[\@2.\@2];lam[\@3.\@3]] ~>* lam[\@2.\@2]
+-- ap[lam[\@2.\@2];lam[\@3.\@3]] ~>* lam[\@4.\@4]
 -- @
 --
 main ∷ IO ()
 main = do
-  let mm = runM $ appTm >>= toString
-      mm' = runM $ appTm >>= toString . eval
-  print $ mm ++ " ~>* " ++ mm'
+  -- Try out the type checker
+  either fail print . runM . runExceptT . runJudgeT $ do
+    x ← fresh
+    checkTy [] (lam (x \\ var x)) (pi unit (x \\ unit))
+
+  print . runM $ do
+    mm ← appTm
+    mmStr ← toString mm
+    mmStr' ← toString $ eval mm
+    return $ mmStr ++ " ~>* " ++ mmStr'
 
diff --git a/src/Abt/Types/View.hs b/src/Abt/Types/View.hs
--- a/src/Abt/Types/View.hs
+++ b/src/Abt/Types/View.hs
@@ -8,10 +8,15 @@
 module Abt.Types.View
 ( View(..)
 , View0
+, _ViewOp
 , mapView
 ) where
 
+import Abt.Class.HEq1
 import Abt.Types.Nat
+
+import Control.Applicative
+import Data.Profunctor
 import Data.Vinyl
 
 -- | @v@ is the type of variables; @o@ is the type of operators parameterized
@@ -39,4 +44,24 @@
 mapView η = \case
   V v → V v
   v :\ e → v :\ η e
-  o :$ es → o :$ rmap η es
+  o :$ es → o :$ η <<$>> es
+
+-- | A prism to extract arguments from a proposed operator.
+--
+-- @
+-- '_ViewOp' ∷ 'HEq1' o ⇒ o ns → Prism' ('View0' v o φ) ('Rec' φ ns)
+-- @
+--
+_ViewOp
+  ∷ ( Choice p
+    , Applicative f
+    , HEq1 o
+    )
+  ⇒ o ns
+  → p (Rec φ ns) (f (Rec φ ns))
+  → p (View0 v o φ) (f (View0 v o φ))
+_ViewOp o = dimap fro (either pure (fmap (o :$))) . right'
+  where
+    fro = \case
+      o' :$ es | Just Refl ← heq1 o o' → Right es
+      e → Left e