Isn't a value of type `Set`

also a value of type `Type`

?

I did

```
Check nat : Set.
Check nat : Type.
```

and it ran without errors.

But doing

```
Require Import List.
Import ListNotations.
Check [nat; bool]%list : list Set. (* ✓ *)
Check [nat; bool]%list : list Type. (* ✗ *)
(*
The term "[nat; bool]" has type "list Set" while it is expected to have type
"list Type" (universe inconsistency: Cannot enforce Set = tst.2).
*)
```

Why is the error happening in the last line?

a value of type `list Set`

is not a value of type `list Type`

`[nat; bool]`

becomes the kernel term `@cons Set nat (@cons Set bool (@nil Set))`

which has type `list Set`

So `Set`

being `Set : Type`

won't reach down to `@cons Set nat (@cons Set bool (@nil Set))`

being something like a 'subset' of `@cons Type nat (@cons Type bool (@nil Type))`

?

Is there a flag to show implicit args as well while printing terms in coq?

`Set Printing All`

it's not `Set : Type`

that's important, it's `Set <= Type`

`cons Set ...`

produces a `list Set`

, but `list Set`

isn't `<= list Type`

consider also

```
Arguments cons {_} & _ _.
Check [nat; bool]%list : list Type.
```

the `&`

is a bidi hint https://coq.github.io/doc/master/refman/language/extensions/arguments-command.html#bidirectionality-hints which makes it infer `@cons Type ...`

I wasn't sure about the `<=`

but it's mentioned at http://adam.chlipala.net/cpdt/html/Universes.html

So am reading that.

Oh does `Set <= Type`

mean something like `Set ⊆ Type`

?

Intuitively, yes, but <= can be more restrictive

as in the example above where not (list Set <= list Type)

Julin S said:

Oh does

`Set <= Type`

mean something like`Set ⊆ Type`

?

that's what it means

it doesn't go through application

An alternative solution to the bidi hint of Gaëtan is to annotate your terms with types to help the elaboration:

```
Check [nat : Type; bool : Type] : list Type.
```

That way the annotation forces both `nat`

and `bool`

to be coerced to `Type`

(which is possible), and so you do not run into the issue of coercing from `list Set`

to `list Type`

(which is not possible).

Last updated: Feb 06 2023 at 12:04 UTC