Address n in Set[n].

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{universe}\\
+    |~& Set[n]          & \text{polymorphic universe}\\
     |~& (a)             & \text{grouping}
 \end{align*}
 \caption{Agda core syntax grammar \citep{agdawiki}.}