diff --git a/lib/Quox/Syntax/Universe.idr b/lib/Quox/Syntax/Universe.idr
index 10d6075..7a84161 100644
--- a/lib/Quox/Syntax/Universe.idr
+++ b/lib/Quox/Syntax/Universe.idr
@@ -21,3 +21,7 @@ export
 PrettyHL Universe where
   prettyM UAny  = pure $ hl Delim "_"
   prettyM (U l) = pure $ hl Free $ pretty l
+
+export %inline
+fromInteger : (x : Integer) -> (0 _ : So (x >= 0)) => Universe
+fromInteger x = U $ fromInteger x