Can typecheck universe-polymorphic id

1 files changed, 4 insertions, 4 deletions

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)