leafGecko (May 26 2021 at 12:38): leafGecko (May 26 2021 at 12:38):I was reading Coq Art, on p.40 the author defined an order of types using operator "less or equal". Then it was stated that forall t: A, if A <= B, then t: B also holds. The following code demonstrated the law:
Check (nat->nat: Set).
Check (nat->nat: Type).
However, neither of the following code lines of code work:
Check (3: Set).
Check (3: Type).
If the instances of objects were T0, basic types were T1, Set/Prop sorts were T2, Type(0) were T3 ...
I assume the "less or equal" relationship only applies to T1 and above? If so, is there a reason?
Thanks!
Théo Winterhalter (May 26 2021 at 12:39):The order is not t : A and A : B implies t : B.
Théo Winterhalter (May 26 2021 at 12:40):It's rather that there is hierarchy on universes. Roughly Type0 ≤ Type1 ≤ Type2.
Théo Winterhalter (May 26 2021 at 12:41):It is also the case that Type0 : Type1 and Type1 : Type2 but that does not mean that typing can be confused with subtyping.
Théo Winterhalter (May 26 2021 at 12:42):You can think in terms of subsets if it helps. Set and Type are sets containing types. 3 is not a type but a natural number (3 : nat) so it doesn't belong in either Set or Type.
Enrico Tassi (May 26 2021 at 12:44):Another way to see it: if 3 : Type, then 3 would be a type and you would be allowed to write forall x : 3, ... and that would not mean much.
Last updated: Oct 13 2024 at 01:02 UTC