@@ -187,13 +187,16 @@ It’s not a priority, though not a bad idea in the long run. It would be a
187187worthwhile effort in the short term to implement libraries to support
188188self-hosting, such as a good parsing library.
189189
190−Does Idris have Universe Polymorphism? What is the type of ``Type``?
190+Does Idris have universe polymorphism? What is the type of ``Type``?
191191====================================================================
192192
193−Rather than Universe polymorphism, Idris has a cumulative hierarchy of
193+Rather than universe polymorphism, Idris has a cumulative hierarchy of
194194universes; ``Type : Type 1``, ``Type 1 : Type 2``, etc.
195−Cumulativity means that if ``x : Type n`` then also ``x : Type m``,
196−provided that ``n <= m``.
195+Cumulativity means that if ``x : Type n`` and ``n <= m``, then
196+``x : Type m``. Universe levels are always inferred by Idris, and
197+cannot be specified explicitly. The REPL command ``:type Type 1`` will
198+result in an errror, as will attempting to specify the universe level
199+of any type.
197200
198201Why does Idris use ``Float`` and ``Double`` instead of ``Float32`` and ``Float64``?
199202===================================================================================