Stream: Coq users

Topic: [beginner] why Check (3:Set). does not work.


view this post on Zulip 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!

view this post on Zulip Théo Winterhalter (May 26 2021 at 12:39):

The order is not t : A and A : B implies t : B.

view this post on Zulip Théo Winterhalter (May 26 2021 at 12:40):

It's rather that there is hierarchy on universes. Roughly Type0 ≤ Type1 ≤ Type2.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC