diff --git a/src/MiniJuvix/Syntax/Concrete/Language.hs b/src/MiniJuvix/Syntax/Concrete/Language.hs
index 98a4ffe62..cee8c6a5b 100644
--- a/src/MiniJuvix/Syntax/Concrete/Language.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Language.hs
@@ -624,7 +624,9 @@ deriving stock instance
 -- Universe expression
 --------------------------------------------------------------------------------
 
-newtype Universe = Universe Natural
+newtype Universe = Universe {
+  universeLevel :: Maybe Natural
+  }
   deriving stock (Show, Eq, Ord, Lift)
 
 --------------------------------------------------------------------------------
diff --git a/src/MiniJuvix/Syntax/Concrete/Parser.hs b/src/MiniJuvix/Syntax/Concrete/Parser.hs
index 291de3b4c..53cba214e 100644
--- a/src/MiniJuvix/Syntax/Concrete/Parser.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Parser.hs
@@ -181,11 +181,10 @@ letBlock = do
 -- Universe expression
 --------------------------------------------------------------------------------
 
-defaultUniverse :: Universe
-defaultUniverse = Universe 0
-
 universe :: MonadParsec e Text m => m Universe
-universe = defaultUniverse <$ kwType
+universe = do
+  kwType
+  Universe <$> optional decimal
 
 -------------------------------------------------------------------------------
 -- Type signature declaration
diff --git a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
index 02d4145dc..ce9f378e6 100644
--- a/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
+++ b/src/MiniJuvix/Syntax/Concrete/Scoped/Pretty/Base.hs
@@ -309,7 +309,7 @@ ppFunction Function {..} = do
           return $ parens (paramName' <+> ppUsage paramUsage <+> paramType')
 
 ppUniverse :: Members '[Reader Options] r => Universe -> Sem r (Doc Ann)
-ppUniverse (Universe n) = return $ kwType <+> pretty n
+ppUniverse (Universe n) = return $ kwType <+?> (pretty <$> n)
 
 ppLetBlock :: forall r. Members '[Reader Options] r => LetBlock 'Scoped -> Sem r (Doc Ann)
 ppLetBlock LetBlock {..} = do