diff --git a/src/Quox/Typechecker.idr b/src/Quox/Typechecker.idr
new file mode 100644
index 0000000..ec73f8f
--- /dev/null
+++ b/src/Quox/Typechecker.idr
@@ -0,0 +1,168 @@
+module Quox.Typechecker
+
+import public Quox.Syntax
+import public Quox.Typing
+import Quox.Error
+
+import Data.Nat
+import Data.SortedMap
+import Control.Monad.Reader
+import Control.Monad.State
+import Syntax.WithProof
+
+%default total
+
+
+public export
+data Error : Type where
+  ExpectedType : (subj, ty : Term d n) -> Error
+  UniverseInconsistency : (lo, hi : Universe) -> Error
+  GlobalNotInScope : Name -> Error
+
+public export
+record CheckResult
+  {0 d, n : Nat}
+  (0 ctx : WfContext d n)
+  (0 subj, ty : Term d n)
+where
+  constructor MkCheckResult
+  tmout, tyout : QOutput n
+  hasType : HasTypeT {ctx = ctx.ctx, subj, ty, tmout, tyout}
+
+
+public export
+record InferResult
+  {0 d, n : Nat}
+  (0 ctx : WfContext d n)
+  (0 subj : Elim d n)
+where
+  constructor MkInferResult
+  tmout, tyout : QOutput n
+  ty : Term d n
+  hasType : HasTypeE {ctx = ctx.ctx, subj, ty, tmout, tyout}
+
+
+public export
+zeroCtx : Globals -> TyContext 0 0
+zeroCtx globals = MkTyContext {globals, dctx = DNil, tctx = [<], qctx = [<]}
+
+public export
+zeroWfCtx : Globals -> WfContext 0 0
+zeroWfCtx globals = MkWfContext (zeroCtx globals) NIL
+
+public export
+Check0 : (globals : Globals) -> (subj, ty : Term 0 0) -> Type
+Check0 globals subj ty =
+  HasTypeT {ctx = zeroCtx globals, subj, ty, tmout = [<], tyout = [<]}
+
+public export
+record Infer0 (globals : Globals) (subj : Elim 0 0) where
+  constructor MkInfer0
+  ty : Term 0 0
+  hasType : HasTypeE {ctx = zeroCtx globals, subj, ty, tmout = [<], tyout = [<]}
+
+
+export
+0 isTypeZeroTyout : HasTypeT {ty = TYPE _, tyout, _} -> IsZero tyout
+isTypeZeroTyout (TYPE  {zty, _}) = zty
+isTypeZeroTyout (Pi    {zty, _}) = zty
+isTypeZeroTyout (PushT {})   = ?isTypeZeroTyout_PushT
+
+
+parameters {auto _ : MonadThrow Error m} mutual
+  private
+  checkUniverse : (lo, hi : Universe) -> m (lo `LT` hi)
+  checkUniverse lo hi with (lo `isLT` hi)
+    _ | Yes lt = pure lt
+    _ | No  _  = throw $ UniverseInconsistency {lo, hi}
+
+  private
+  expectType : (subj, ty : Term d n) ->
+               m (l : Universe ** ty = TYPE l)
+  expectType _    (TYPE l) = pure (l ** Refl)
+  expectType subj ty       = throw $ ExpectedType {subj, ty}
+
+  private
+  checkType : (ctx : WfContext d n) ->
+              (l : Universe) -> (ty : Term d n) ->
+              m (CheckResult ctx (TYPE l) ty)
+  checkType (MkWfContext {ctx, wf}) l ty = do
+    (l' ** eq) <- expectType (TYPE l) ty; let Refl = eq
+    lt <- checkUniverse l l'
+    let Element _ zprf = zero ctx.qctx
+    pure $ MkCheckResult {hasType = TYPE {wf, lt, ztm = zprf, zty = zprf}, _}
+
+  private
+  checkPi : (ctx : WfContext d n) ->
+            (qtm, qty : Qty) ->
+            (x : Name) ->
+            (arg : Term d n) ->
+            (res : Term d (S n)) ->
+            (ty  : Term d n) ->
+            m (CheckResult ctx (Pi qtm qty x arg res) ty)
+  checkPi (MkWfContext {ctx, wf}) qtm qty x arg res ty = do
+    let whole = Pi qtm qty x arg res
+    (l' ** eq) <- expectType whole ty; let Refl = eq
+    ?checkPi_rhs
+
+
+  private
+  inferFree : (ctx : WfContext {}) -> (x : Name) -> m (InferResult ctx (F x))
+  inferFree (MkWfContext {ctx, wf}) x =
+    case @@ lookup x ctx.globals of
+      (Just g ** eq) =>
+        let Element _ zprf = zero ctx.tctx
+            hasType = F {wf, g, eq, ztm = zprf, zty = zprf}
+        in
+        pure $ MkInferResult {hasType, _}
+      _ => throw $ GlobalNotInScope x
+
+  private
+  inferBound : (ctx : WfContext _ n) -> (i : Var n) -> m (InferResult ctx (B i))
+  inferBound (MkWfContext {ctx, wf}) i =
+    pure $ MkInferResult {hasType = B {wf, look = lookup ctx i, eq = Refl}, _}
+
+  private
+  inferAnn : (ctx : WfContext d n) -> (tm, ty : Term d n) ->
+             m (InferResult ctx (tm :# ty))
+  inferAnn ctx tm ty = do
+    ignore $ check ctx ty (TYPE UAny)
+    MkCheckResult {hasType, _} <- check ctx tm ty
+    pure $ MkInferResult {hasType = Ann hasType, _}
+
+
+  export
+  check : (ctx : WfContext d n) -> (subj, ty : Term d n) ->
+          m (CheckResult ctx subj ty)
+  check ctx subj ty = case subj of
+    TYPE l               => checkType ctx l ty
+    Pi qtm qty x arg res => checkPi ctx qtm qty x arg res ty
+    Lam x body           => ?check_rhs_3
+    E e                  => ?check_rhs_4
+    CloT  s th           => ?check_rhs_5
+    DCloT s th           => ?check_rhs_6
+
+  export
+  infer : (ctx : WfContext d n) -> (subj : Elim d n) ->
+          m (InferResult ctx subj)
+  infer ctx subj = case subj of
+    F x        => inferFree ctx x
+    B i        => inferBound ctx i
+    fun :@ arg => ?infer_rhs_3
+    tm :# ty   => inferAnn ctx tm ty
+    CloE  e th => ?infer_rhs_5
+    DCloE e th => ?infer_rhs_6
+
+
+parameters {auto _ : MonadThrow Error m} (globals : Globals)
+  public export
+  check0 : (subj, ty : Term 0 0) -> m (Check0 globals subj ty)
+  check0 subj ty = pure $
+    case !(check (zeroWfCtx globals) subj ty) of
+      MkCheckResult [<] [<] prf => prf
+
+  public export
+  infer0 : (subj : Elim 0 0) -> (ty : Term 0 0) -> m (Infer0 globals subj)
+  infer0 subj ty = pure $
+    case !(infer (zeroWfCtx globals) subj) of
+      MkInferResult [<] [<] ty prf => MkInfer0 ty prf
diff --git a/src/Quox/Typing.idr b/src/Quox/Typing.idr
new file mode 100644
index 0000000..4a4ae31
--- /dev/null
+++ b/src/Quox/Typing.idr
@@ -0,0 +1,280 @@
+module Quox.Typing
+
+import public Quox.Syntax
+import public Quox.Context
+
+import Data.Nat
+import Data.SortedMap
+import Control.Monad.Reader
+import Control.Monad.State
+
+
+%default total
+
+public export
+data DContext : Nat -> Type where
+  DNil  : DContext 0
+  DBind : DContext d -> DContext (S d)
+  DEq   : Dim d -> Dim d -> DContext d -> DContext d
+
+public export
+TContext : Nat -> Nat -> Type
+TContext d = Context (Term d)
+
+public export
+QContext : Nat -> Type
+QContext = Triangle' Qty
+
+public export
+QOutput : Nat -> Type
+QOutput = Context' Qty
+
+
+public export
+record Global where
+  constructor MkGlobal
+  type, term : forall d, n. Term d n
+
+public export
+Globals : Type
+Globals = SortedMap Name Global
+
+
+public export
+record TyContext (d, n : Nat) where
+  constructor MkTyContext
+  globals : Globals
+  dctx : DContext d
+  tctx : TContext d n
+  qctx : QContext n
+
+%name TyContext ctx
+
+
+namespace TContext
+  export
+  pushD : TContext d n -> TContext (S d) n
+  pushD tel = map (/// shift 1) tel
+
+
+namespace TyContext
+  export
+  extendTy : Term d n -> QOutput n -> TyContext d n -> TyContext d (S n)
+  extendTy s rhos = {tctx $= (:< s), qctx $= (:< rhos)}
+
+  export
+  extendDim : TyContext d n -> TyContext (S d) n
+  extendDim = {dctx $= DBind, tctx $= pushD}
+
+  export
+  eqDim : Dim d -> Dim d -> TyContext d n -> TyContext d n
+  eqDim p q = {dctx $= DEq p q}
+
+
+
+namespace QOutput
+  export
+  (+) : QOutput n -> QOutput n -> QOutput n
+  (+) = zipWith (+)
+
+  export
+  (*) : Qty -> QOutput n -> QOutput n
+  (*) pi = map (pi *)
+
+
+namespace Zero
+  public export
+  data IsZero : QOutput n -> Type where
+    LinZ  : IsZero [<]
+    SnocZ : IsZero qctx -> IsZero (qctx :< Zero)
+
+  export
+  isZeroIrrel : {qctx : _} -> (0 _ : IsZero qctx) -> IsZero qctx
+  isZeroIrrel {qctx = [<]}    LinZ      = LinZ
+  isZeroIrrel {qctx = _ :< _} (SnocZ x) = SnocZ $ isZeroIrrel x
+
+  export
+  zero : Context _ n -> Subset (QOutput n) IsZero
+  zero [<]        = Element [<] LinZ
+  zero (ctx :< _) = let zeroN = zero ctx in
+                    Element (zeroN.fst :< Zero) (SnocZ zeroN.snd)
+
+
+namespace Only
+  public export
+  data IsOnly : QOutput n -> Var n -> Type where
+    Here  : IsZero qctx   -> IsOnly (qctx :< One) VZ
+    There : IsOnly qctx i -> IsOnly (qctx :< Zero) (VS i)
+
+  export
+  isOnlyIrrel : {qctx, i : _} -> (0 _ : IsOnly qctx i) -> IsOnly qctx i
+  isOnlyIrrel {i = VZ}     (Here  z) = Here  $ isZeroIrrel z
+  isOnlyIrrel {i = (VS i)} (There o) = There $ isOnlyIrrel o
+
+  export
+  only : Context _ n -> (i : Var n) ->
+         Subset (QOutput n) (\qctx => IsOnly qctx i)
+  only (ctx :< _) VZ     =
+    let zeroN = zero ctx in
+    Element (zeroN.fst :< One) (Here zeroN.snd)
+  only (ctx :< _) (VS i) =
+    let onlyN = only ctx i in
+    Element (onlyN.fst :< Zero) (There onlyN.snd)
+
+
+namespace Universe
+  public export
+  data LT : Universe -> Universe -> Type where
+    Fin : k `LT` l -> U k `LT` U l
+    Any : U _ `LT` UAny
+
+  export
+  Uninhabited (UAny `LT` j) where
+    uninhabited _ impossible
+
+  export
+  isLT : (i, j : Universe) -> Dec (i `LT` j)
+  isLT (U i) (U j) with (i `isLT` j)
+    _ | Yes prf   = Yes $ Fin prf
+    _ | No contra = No  $ \(Fin prf) => contra prf
+  isLT (U _) UAny = Yes Any
+  isLT UAny  _    = No uninhabited
+
+
+namespace Lookup
+  public export
+  data IsLookup :
+      (tctx : TContext d n) ->
+      (i    : Var n) ->
+      (ty   : Term d from) ->
+      (by   : Shift from n) -> Type
+    where
+      Here  : IsLookup {tctx=(tctx :< ty), i=VZ, ty, by=(SS SZ)}
+      There : IsLookup {tctx, i, ty, by} ->
+              IsLookup {tctx=(tctx :< ty'), i=(VS i), ty, by=(SS by)}
+
+  public export
+  record Lookup'
+    {0 d, n : Nat}
+    (0 tctx : TContext d n)
+    (0 qctx : QContext n)
+    (0 i : Var n)
+  where
+    constructor MkLookup
+    tmout, tyout : QOutput n
+    type : Term d from
+    by   : Shift from n
+    0 only : IsOnly tmout i
+    0 look : IsLookup tctx i type by
+
+  public export
+  lookup' : (tctx : TContext d n) -> (qctx : QContext n) ->
+            (i : Var n) -> Lookup' tctx qctx i
+  lookup' tctx@(_ :< _) (_ :< tyout) VZ =
+    MkLookup {only = (only tctx VZ).snd, look = Here,
+              tyout = tyout :< Zero, _}
+  lookup' (tctx :< _) (qctx :< _) (VS i) =
+    let inner = lookup' tctx qctx i in
+    MkLookup {only = There inner.only, look = There inner.look,
+              tyout = inner.tyout :< Zero, _}
+
+
+  public export %inline
+  Lookup : TyContext d n -> Var n -> Type
+  Lookup ctx i = Lookup' ctx.tctx ctx.qctx i
+
+  public export %inline
+  lookup : (ctx : TyContext d n) -> (i : Var n) -> Lookup ctx i
+  lookup ctx = lookup' ctx.tctx ctx.qctx
+
+
+
+mutual
+  public export
+  data HasTypeT :
+      {0 d, n : Nat} ->
+      (ctx  : TyContext d n) ->
+      (subj : Term d n) ->
+      (ty   : Term d n) ->
+      (tmout, tyout : QOutput n) ->
+      Type
+    where
+      TYPE :
+        (0 wf : IsWf ctx) ->
+        (lt : k `LT` l) ->
+        (0 ztm : IsZero tmout) -> (0 zty : IsZero tyout) ->
+        HasTypeT {ctx, subj = TYPE k, ty = TYPE l, tmout, tyout}
+      Pi :
+        (tyA : HasTypeT {ctx, subj = a, ty = TYPE l, tmout = tmoutA, tyout}) ->
+        (tyB : HasTypeT {ctx = extendTy a tmoutA ctx, subj = b, ty = TYPE l,
+                         tmout = tmoutB :< qty, tyout = tyout :< Zero}) ->
+        (0 zty : IsZero tyout) ->
+        HasTypeT {ctx, subj = Pi qtm qty x a b, ty = TYPE l,
+                  tmout = tmoutA + tmoutB, tyout}
+      PushT :
+        (0 eq : ty' = pushSubstsT' ty) ->
+        (j : HasTypeT {ctx, subj, ty = ty', tmout, tyout}) ->
+        HasTypeT {ctx, subj, ty, tmout, tyout}
+
+  public export
+  data HasTypeE :
+      {0 d, n : Nat} ->
+      (ctx  : TyContext d n) ->
+      (subj : Elim d n) ->
+      (ty   : Term d n) ->
+      (tmout, tyout : QOutput n) ->
+      Type
+    where
+      F :
+        (0 wf : IsWf ctx) ->
+        (g : Global) ->
+        (0 eq : lookup x ctx.globals = Just g) ->
+        (0 ztm : IsZero tmout) -> (0 zty : IsZero tyout) ->
+        HasTypeE {ctx, subj = F x, ty = g.type, tmout, tyout}
+      B :
+        {0 ctx : TyContext d n} ->
+        (0 wf : IsWf ctx) ->
+        (look : Lookup ctx i) ->
+        (0 eq : ty = look.type // look.by) ->
+        HasTypeE {ctx, subj = B i, ty, tmout = look.tmout, tyout = look.tyout}
+      Ann :
+        HasTypeT {ctx, subj = tm,       ty, tmout, tyout} ->
+        HasTypeE {ctx, subj = tm :# ty, ty, tmout, tyout}
+      PushE :
+        (0 eq : ty' = pushSubstsT' ty) ->
+        HasTypeE {ctx, subj, ty = ty', tmout, tyout} ->
+        HasTypeE {ctx, subj, ty, tmout, tyout}
+
+  public export
+  data IsWf' :
+      (globals : Globals) ->
+      (dctx : DContext d) ->
+      (tctx : TContext d n) ->
+      (qctx : QContext n) -> Type
+    where
+      NIL  : IsWf' globals dctx [<] [<]
+      BIND :
+        IsWf' {globals, dctx, tctx, qctx} ->
+        HasTypeT {ctx = MkTyContext {globals, dctx, tctx, qctx},
+                  subj, ty = TYPE l, tmout, tyout} ->
+        IsWf' {globals, dctx, tctx = tctx :< subj, qctx = qctx :< tmout}
+
+  public export %inline
+  IsWf : TyContext d n -> Type
+  IsWf (MkTyContext {globals, dctx, tctx, qctx}) =
+    IsWf' {globals, dctx, tctx, qctx}
+
+public export
+record WfContext (d, n : Nat) where
+  constructor MkWfContext
+  ctx  : TyContext d n
+  0 wf : IsWf ctx
+
+
+public export
+record TypeTerm {0 d, n : Nat} (ctx : TyContext d n) where
+  constructor MkTypeTerm
+  term : Term d n
+  univ : Universe
+  tmout, tyout : QOutput n
+  isType : HasTypeT {ctx, subj = term, ty = TYPE univ, tmout, tyout}