From a4c5c1057a59ecd6172c27b42c8f40d37247e813 Mon Sep 17 00:00:00 2001
From: Natalie Perna <nmperna@gmail.com>
Date: Wed, 7 Jun 2017 12:02:32 -0400
Subject: [PATCH] Better universive polymorphism note.

---
 Figures/AgdaCore.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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}.}