diff --git a/nbe-test.rkt b/nbe-test.rkt
index 300a90b..68208df 100644
--- a/nbe-test.rkt
+++ b/nbe-test.rkt
@@ -83,7 +83,7 @@
   `(succ ,a))
 
 (check-equal? (normalize `(app ,tm-id ,tm-id)) tm-id)
-(check βη-eq? `(app ,tm-id (U 0)) '(U 0))
+(check βη-eq? `(app ,tm-id U) 'U)
 (check-equal? (normalize `(app (app (app ,tm-pair ,tm-id) ,tm-fst) ,tm-snd)) tm-fst)
 (check-equal? (normalize `(app (app (app ,tm-pair ,tm-id) ,tm-fst) ,tm-fst)) tm-id)
 (check-equal? (normalize (tm-app tm-snd (tm-app tm-pair tm-id tm-fst) tm-fst)) tm-fst)
@@ -97,5 +97,10 @@
               (tm-pnat 12000))
 (check βη-eq? (tm-padd (tm-pnat 10000) (tm-pnat 2000)) (tm-pnat 12000))
 (check βη-eq? (tm-abs (tm-app (tm-var 1) (tm-var 0))) (tm-app tm-id (tm-var 0)))
-(check βη-eq? `(Π (U 0) (Π (var 0) ,(tm-app tm-id '(var 1)))) '(Π (U 0) (Π (var 0) (var 1))))
-(check-false (βη-eq? '(U 0) '(var 0)))
+(check βη-eq? `(Π U (Π (var 0) ,(tm-app tm-id '(var 1)))) '(Π U (Π (var 0) (var 1))))
+(check-false (βη-eq? '(succ zero) '(var 0)))
+(check βη-eq? (tm-app (tm-var 0) (tm-var 1)) (tm-app (tm-var 0) (tm-var 1)))
+(check βη-eq? (tm-ind (tm-var 0) (tm-var 1) (tm-var 2)) (tm-ind (tm-var 0) (tm-var 1) (tm-var 2)))
+(check-false (βη-eq? (tm-abs (tm-app (tm-var 1) (tm-var 0))) (tm-app tm-id (tm-var 1))))
+(check-false (βη-eq? (tm-app (tm-var 0) (tm-var 0)) (tm-ind (tm-var 0) 'zero 'zero)))
+(check-false (βη-eq? 'U '(var 0)))
diff --git a/nbe.rkt b/nbe.rkt
index 2c309dd..cf227be 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -1,9 +1,8 @@
 #lang typed/racket
-;; Grammar (Λ)
-;; t := λ t | app t t | i
 
 (define-type denv (-> V (Promise D)))
 (define-type V Nonnegative-Integer)
+
 (define-type Term (∪ 'zero
                      'nat
                      (List 'succ Term)
@@ -12,14 +11,32 @@
                      (List 'app Term Term)
                      (List 'ind Term Term Term)
                      (List 'Π Term Term)
-                     (List 'U V)))
+                     'U))
+
+(define-type Neu (∪ (List 'ind Neu Norm Norm)
+                    (List 'var V)
+                    (List 'app Neu Norm)))
+
+(define-type Norm (∪ Neu
+                     'zero
+                     'nat
+                     (List 'λ Norm)
+                     'U
+                     (List 'succ Norm)
+                     (List 'Π Norm Norm)))
+
+(: embed (-> Neu Term))
+(define (embed a) a)
+
+(: embed-norm (-> Norm Term))
+(define (embed-norm a) a)
 
 (define-type D (∪ 'zero
                   (List 'Π (Promise D) (-> (Promise D) D))
                   (List 'succ (Promise D))
                   (List 'fun (-> (Promise D) D))
                   (List 'neu D-ne)
-                  (List 'U V)))
+                  'U))
 
 (define-type D-ne (∪ (List 'app D-ne D)
                      (List 'idx V)
@@ -58,7 +75,7 @@
 (: interp (-> Term denv D))
 (define (interp a ρ)
   (match a
-    [`(U ,_) a]
+    ['U a]
     [`(Π ,A ,B) `(Π ,(delay (interp A ρ)) ,(interp-fun B ρ))]
     [`(var ,i) (force (ρ i))]
     ['zero 'zero]
@@ -70,13 +87,46 @@
     [`(λ ,a) (list 'fun (interp-fun a ρ))]
     [`(app ,a ,b) (ap a b ρ)]))
 
-(: reify (-> V D Term))
+(: open-dom (-> V (-> (Promise D) D) D))
+(define (open-dom n f)
+  (f (delay `(neu (idx ,n)))))
+
+(: open-dom2 (-> V (-> (Promise D) (Promise D) D) D))
+(define (open-dom2 n f)
+  (f (delay `(neu (idx ,n))) (delay `(neu (idx ,(add1 n))))))
+
+(: compare (-> V D D Boolean))
+(define (compare n a0 a1)
+  (match (list a0 a1)
+    [`((Π ,A0 ,B0) (Π ,A1 ,B1))
+     (and (compare n (force A0) (force A1))
+          (compare (add1 n) (open-dom n B0) (open-dom n B1)))]
+    ['(nat nat) #t]
+    ['(U U) #t]
+    ['(zero zero) #t]
+    [`((succ ,a) (succ ,b)) (compare n (force a) (force b))]
+    [`((fun ,f) (neu ,u)) (compare (add1 n) (open-dom n f) `(neu (app ,u (neu (idx ,n)))))]
+    [`((neu ,_) (fun ,_)) (compare n a1 a0)]
+    [`((neu ,a) (neu ,b)) (compare-neu n a b)]
+    [_ #f]))
+
+(: compare-neu (-> V D-ne D-ne Boolean))
+(define (compare-neu n a0 a1)
+  (match (list a0 a1)
+    [`((idx ,i) (idx ,j)) (eqv? i j)]
+    [`((app ,u0 ,v0) (app ,u1 ,v1)) (and (compare-neu n u0 u1) (compare n v0 v1))]
+    [`((ind ,a0 ,b0 ,c0) (ind ,a1 ,b1 ,c1)) (and (compare-neu n a0 a1)
+                                                 (compare n b0 b1)
+                                                 (compare (+ n 2) (open-dom2 n c0) (open-dom2 n c1)))]
+    [_ #f]))
+
+(: reify (-> V D Norm))
 (define (reify n a)
   (match a
     [`(Π ,A ,B) `(Π ,(reify n (force A)) ,(reify (+ n 1) (B (delay `(neu (idx ,n))))))]
     ['zero 'zero]
     [`(succ ,a) `(succ ,(reify n (force a)))]
-    [`(U ,_) a]
+    ['U a]
     [`(fun ,f) (list 'λ (reify (+ n 1) (f (delay `(neu (idx ,n))))))]
     [`(neu ,a) (reify-neu n a)]))
 
@@ -87,7 +137,7 @@
         (error "variable to index conversion failed")
         ret)))
 
-(: reify-neu (-> V D-ne Term))
+(: reify-neu (-> V D-ne Neu))
 (define (reify-neu n a)
   (match a
     [`(ind ,a ,b ,c) (list 'ind
@@ -106,7 +156,7 @@
 (define (scope a)
   (match a
     [`(Π ,A ,B) (max (scope A) (- (scope B) 2))]
-    [`(U ,_) 0]
+    ['U 0]
     ['zero 0]
     [`(succ ,a) (scope a)]
     (`(ind ,a ,b ,c) (max (scope a) (scope b) (- (scope c) 2)))
@@ -115,6 +165,10 @@
     [`(app ,a ,b) (max (scope a) (scope b))]
     [`(var ,i) (+ i 1)]))
 
+(: interp-with-scope (-> V Term D))
+(define (interp-with-scope n a)
+  (interp a (λ (x) (delay (idsub n x)))))
+
 (: normalize (-> Term Term))
 (define (normalize a)
   (let ([sa (scope a)])
@@ -127,7 +181,7 @@
 (: subst (-> (-> V Term) Term Term))
 (define (subst ρ a)
   (match a
-    [`(U ,_) a]
+    ['U a]
     [`(Π ,A ,B) `(Π ,(subst ρ A) ,(subst (up 1 ρ) B))]
     [`(var ,i) (ρ i)]
     [`(app ,a ,b) `(app ,(subst ρ a) ,(subst ρ b))]
@@ -143,10 +197,11 @@
   (subst (ext idsub-tm b) a))
 
 ;; Coquand's algorithm but for β-normal forms
+;; Subsumed by the compare function
 (: η-eq? (-> Term Term Boolean))
 (define (η-eq? a b)
   (match (list a b)
-    [`((U ,i) (U ,j)) (eqv? i j) ]
+    ['(U U) #t ]
     [`((Π ,A0 ,B0) (Π ,A1 ,B1))
      (and (η-eq? A0 A1) (η-eq? B0 B1))]
     ['(zero zero) true]
@@ -162,10 +217,11 @@
 
 (: βη-eq? (-> Term Term Boolean))
 (define (βη-eq? a b)
-  (η-eq? (normalize a) (normalize b)))
+  (let ([n (max (scope a) (scope b))])
+    (compare n (interp a (λ (x) (delay (idsub n x)))) (interp b (λ (x) (delay (idsub n x)))))))
 
 (: β-eq? (-> Term Term Boolean))
 (define (β-eq? a b)
   (equal? (normalize a) (normalize b)))
 
-(provide reify interp normalize β-eq? Term D V βη-eq?)
+(provide reify interp normalize β-eq? Term D D-ne V βη-eq? ext subst1 subst idsub-tm)
diff --git a/type-checker.rkt b/type-checker.rkt
new file mode 100644
index 0000000..5b42c9c
--- /dev/null
+++ b/type-checker.rkt
@@ -0,0 +1,34 @@
+#lang typed/racket
+
+(require "nbe.rkt")
+
+(define-type context (Immutable-HashTable V Term))
+
+(: context-len (-> context V))
+(define (context-len Γ)
+  (hash-count Γ))
+
+(: context-ext (-> context Term context))
+(define (context-ext Γ A)
+  (hash-set Γ (context-len Γ) A))
+
+(: context-get (-> context V Term))
+(define (context-get Γ i)
+  (if (< i (context-len Γ))
+      (subst (λ (j) `(var ,(+ i j 1))) (hash-ref Γ (- (context-len Γ) (add1 i))))
+      (error "context-get: out of bound")))
+
+(: context-empty context)
+(define context-empty (hash))
+
+(: synth (-> context Term Term))
+(define (synth Γ a)
+  (match a
+    [`(var ,i) (context-get Γ i)]
+    [`(app ,a ,b)
+     (let ([A (synth Γ a)]
+           [D (interp-with-scope (context-len Γ) A)]))]))
+
+(: check (-> context Term D Boolean))
+(define (check Γ a A)
+  (error "unimplemented"))