What's the difference between `Set`

and `Type`

?

I mean, I see that `Set:Type`

and that there type universes (that's what it's called, right) like `Typeᵢ:Typeᵢ₊₁`

.

But can `Set`

do anything that `Type`

can't do?

Or is `Set`

a relic from older coq versions or something?

I was trying

```
Inductive nat': Type :=
| O' : nat'
| S' : nat' -> nat'.
```

and then upon doing

```
Check nat'.
(*
nat'
: Set
*)
```

Though I explicitly asked for `nat'`

to be of type `Type`

, it turned out to be of type `Set`

.

Why is this happening?

(This is probably which has been asked numerous time, but I couldn't find an answer.)

One way to look at it is to identify `Set`

with `Type_0`

. For readability and performance, writing `Set`

is better, but you lose some uniformity with respect to always writing `Type`

.

`Set`

is `Type_0`

it is not strictly necessary but it's more efficient than having bunches of floating universes for things like nat

(it is also used for -impredicative-set but most people don't care about that)

very confusingly `: ... -> Type`

(with possibly empty `... ->`

) for inductive types has the special meaning of "try to find the smallest universe this inductive fits in", so for instance `Inductive empty : Type := . Check empty. (* empty : Prop *)`

if you want to force an inductive to be in Type you can use either an explicit annotation or an indirection:

```
(* the + means you allow for there to be more universes used, in this case there are none
when there are some and you don't use + you get the "unbound universe" error *)
Inductive nat'@{i +} : Type@{i} :=
| O' : nat'
| S' : nat' -> nat'.
Check nat'.
(* nat' : Type *)
(* alternatively *)
Definition typ := Type.
Inductive nat' : typ :=
| O' : nat'
| S' : nat' -> nat'.
```

See also https://proofassistants.stackexchange.com/questions/1551/why-not-have-prop-set-in-coq/1552#1552 for a bit of historical background

My general approach is to always use `Set`

until I discover that moment when my development needs `Type`

, because it's helpful to see when that happens and why.

Last updated: Jun 15 2024 at 08:01 UTC