From ae603f2423e967c55dfd31b0dec26d19584aa322 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Sat, 23 Dec 2023 23:12:03 +0100
Subject: Can typecheck universe-polymorphic id

---
 src/AST.hs | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'src/AST.hs')

diff --git a/src/AST.hs b/src/AST.hs
index ba018f5..d828e26 100644
--- a/src/AST.hs
+++ b/src/AST.hs
@@ -1,15 +1,15 @@
 module AST where
 
-import Data.Map.Strict (Map)
+import Numeric.Natural
 
+import Data.Map.Strict (Map)
 
-data Nat = Z | S Nat
-  deriving (Show)
 
 type Name = String
 
 data Term
   = TSet Term            -- ^ The n-th universe (n : Level)
+  | TSetw Natural        -- ^ The n-th ω-universe
   | TVar Name            -- ^ variable
   | TPi Name Term Term   -- ^ Pi: (x : A) -> B
   | TLam Name Term Term  -- ^ λ(x : A). B
@@ -36,7 +36,7 @@ data Term
 data Definition = Definition Name (OfType Term Term)
   deriving (Show)
 
-type Env = Map Name Term
+type Env = Map Name (OfType (Maybe Term) Term)
 
 data OfType a b = a :| b
   deriving (Show)
-- 
cgit v1.2.3-70-g09d2