diff --git a/src/Quox/Typecheck.idr b/src/Quox/Typecheck.idr
deleted file mode 100644
index 7d0454f..0000000
--- a/src/Quox/Typecheck.idr
+++ /dev/null
@@ -1,152 +0,0 @@
-module Quox.Typecheck
-
-import Quox.Syntax
-import Quox.Error
-import Quox.Context
-
-import Data.Nat
-import Control.Monad.Reader
-import Control.Monad.State
-
-
-%default total
-
-public export
-DContext : Nat -> Type
-DContext = Context Dim
-
-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
-
-
-namespace TContext
-  export
-  pushD : TContext d n -> TContext (S d) n
-  pushD tel = map (/// shift 1) tel
-
-
-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)
-
-
-public export
-data LT : Universe -> Universe -> Type where
-  Fin : k `LT` l -> U k `LT` U l
-  Any : U _ `LT` UAny
-
-
-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 i : Var n) where
-    constructor MkLookup
-    qtys : QOutput n
-    type : Term d from
-    by   : Shift from n
-    0 only : IsOnly qtys i
-    0 look : IsLookup tctx i type by
-
-export
-lookup : (ctx : TContext d n) -> (i : Var n) -> Lookup tctx i
-lookup (ctx :< x) VZ =
-  ?lookup_rhs_3
-lookup (ctx :< x) (VS i) =
-  ?lookup_rhs_4
-
-
-
-mutual
-  public export
-  data HasTypeT :
-      (dctx : DContext d) ->
-      (tctx : TContext d n) ->
-      (qctx : QContext n) ->
-      (subj : Term d n) ->
-      (ty   : Term d n) ->
-      (tmout, tyout : QOutput n) ->
-      Type
-    where
-      TYPE :
-        WfCtx {dctx, tctx, qctx} ->
-        k `LT` l ->
-        (0 _ : IsZero tmout) -> (0 _ : IsZero tyout) ->
-        HasTypeT {dctx, tctx, qctx, subj=(TYPE k), ty=(TYPE l), tmout, tyout}
-
-  public export
-  data HasTypeE :
-      (dctx : DContext d) ->
-      (tctx : TContext d n) ->
-      (qctx : QContext n) ->
-      (subj : Elim d n) ->
-      (ty   : Term d n) ->
-      (tmout, tyout : QOutput n) ->
-      Type
-    where
-
-  public export
-  data WfCtx :
-      (dctx : DContext d) ->
-      (tctx : TContext d n) ->
-      (qctx : QContext n) ->
-      Type
-    where
-      NIL  : WfCtx [<] [<] [<]
-      BIND :
-        WfCtx    {dctx, tctx, qctx} ->
-        HasTypeT {dctx, tctx, qctx, subj=a, ty=(TYPE l), tmout, tyout} ->
-        WfCtx    {dctx, tctx=(tctx :< a), qctx=(qctx :< tmout)}