From c6528de647e55df9d78f0294edfbd9c44e2ea634 Mon Sep 17 00:00:00 2001
From: Yiyun Liu <yliu8e5f7@protonmail.com>
Date: Tue, 13 May 2025 19:13:44 -0400
Subject: [PATCH] Remove levels from the universe

---
 nbe-test.rkt |  6 +++---
 nbe.rkt      | 16 ++++++++--------
 2 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/nbe-test.rkt b/nbe-test.rkt
index 25c5b04..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,10 +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 βη-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 0) '(var 0)))
+(check-false (βη-eq? 'U '(var 0)))
diff --git a/nbe.rkt b/nbe.rkt
index 67745d9..86f2917 100644
--- a/nbe.rkt
+++ b/nbe.rkt
@@ -10,14 +10,14 @@
                      (List 'app Term Term)
                      (List 'ind Term Term Term)
                      (List 'Π Term Term)
-                     (List 'U V)))
+                     'U))
 
 (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)
@@ -56,7 +56,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]
@@ -83,7 +83,7 @@
      (and (compare n (force A0) (force A1))
           (compare (add1 n) (open-dom n B0) (open-dom n B1)))]
     ['(nat nat) #t]
-    [`((U ,i) (U ,j)) (eqv? i j)]
+    ['(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)))))]
@@ -107,7 +107,7 @@
     [`(Π ,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)]))
 
@@ -137,7 +137,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)))
@@ -162,7 +162,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))]
@@ -182,7 +182,7 @@
 (: η-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]