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".

0 files changed, 0 insertions, 0 deletions