diff --git a/library/library.md b/library/library.md
index 1be3cf41d..708c1c036 100644
--- a/library/library.md
+++ b/library/library.md
@@ -20,6 +20,7 @@ following packages:
 Lean's default logical framework is a version of the Calculus of Constructions with:
 
 * an impredicative, proof-irrelevant type `Prop` of propositions
+* univerve polymorphism
 * a non-cumulative hierarchy of universes, `Type 1`, `Type 2`, ... above `Prop`
 * inductively defined types