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!

The order is not `t : A`

and `A : B`

implies `t : B`

.

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

.

It is also the case that `Type0 : Type1`

and `Type1 : Type2`

but that does not mean that typing can be confused with subtyping.

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`

.

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: Jun 25 2024 at 15:02 UTC