diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 67683902cd..962d2a94e3 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -51,7 +51,7 @@ function types over these data types. Consequently they also have a type. Because assuming simply that :math:`\Set` has type :math:`\Set` leads to an inconsistent theory :cite:`Coq86`, the language of |Cic| has infinitely many sorts. There are, in addition to :math:`\Set` and :math:`\Prop` -a hierarchy of universes :math:`\Type(i)` for any integer :math:`i`. +a hierarchy of universes :math:`\Type(i)` for any integer :math:`i ≥ 1`. Like :math:`\Set`, all of the sorts :math:`\Type(i)` contain small sets such as booleans, natural numbers, as well as products, subsets and function |