diff options
| author | Théo Zimmermann | 2019-02-06 15:37:07 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-06 15:37:07 +0100 |
| commit | 177a438806f811901ad0aeab4ed69014e9d2af26 (patch) | |
| tree | 5331e522a6c69fda7731150b8c068c3fc9b4e6e6 /doc | |
| parent | c1123f1c05943b8d09245b8fa9d90664344c054d (diff) | |
| parent | 162101e6bc5b3bb33b741ff51e37805ffd624d0d (diff) | |
Merge PR #9456: The lowest universe level is 1.
Reviewed-by: Zimmi48
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 |