From 162101e6bc5b3bb33b741ff51e37805ffd624d0d Mon Sep 17 00:00:00 2001
From: Tanaka Akira
Date: Fri, 1 Feb 2019 11:00:19 +0900
Subject: The lowest universe level is 1.

Cic description doesn't describe the lowest universe level clearly.

- "Type(i) for any integer i" seems Type(-1) is possible
- "S = {Prop,Set,Type(i)| i ∈ ℕ }" depends on the definition of "ℕ"
  which is not described.
  It is well known that there are two definitions that ℕ includes 0 or not.
  In Coq, it is natural that ℕ  includes 0 because the inductive type
  nat includes 0.
- "Prop:Type(1), Set:Type(1)" suggests the lowest level is 1.
- AX-Prop and AX-Set describes Prop:Type(1) and Set:Type(1).
  So, Prop and Set are not belongs to Type(0).

Also, CPDT describes that "The type of Set is Type(0)".
http://adam.chlipala.net/cpdt/html/Universes.html

I think the lowest universe level is 1 because AX-Prop and AX-Set.

I'm not certain to fix this problem but
my idea to fix this problem is changing
"Type(i) for any integer i" to
"Type(i) for any integer i ≥ 1".
---
 doc/sphinx/language/cic.rst | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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
-- 
cgit v1.2.3