diff --git a/Figures/AgdaCore.tex b/Figures/AgdaCore.tex
index 713e625..f7b3445 100644
--- a/Figures/AgdaCore.tex
+++ b/Figures/AgdaCore.tex
@@ -4,7 +4,7 @@
     |~& \lambda x \to a & \text{abstraction}\\
     |~& a~a             & \text{application}\\
     |~& (x : a) \to a   & \text{function space}\\
-    |~& Set[n]          & \text{polymorphic universe}\\
+    |~& Set[n]          & \text{universe (at level $n$)}\\
     |~& (a)             & \text{grouping}
 \end{align*}
 \caption{Agda core syntax grammar \citep{agdawiki}.}