What exactly is a Set in Coq

Question

I'm still puzzled what the sort Set means in Coq. When do I use Set and when do I use Type?

In Hott a Set is defined as a type, where identity proofs are unique. But I think in Coq it has a different interpretation.

Laconism

It's sorta-kinda (heh) Type 0, where Type 0 : Type 1 : Type 2 : …. – Nostology

I am confused what Adam Chlipala means by Second, there is the : Set fragment, which declares that we are defining a datatype that should be thought of as a constituent of programs. Later, which I don't understand what it means. Why didn't he just use Type? – Oceanography

Answer 1

Set means rather different things in Coq and HoTT.

In Coq, every object has a type, including types themselves. Types of types are usually referred to as sorts, kinds or universes. In Coq, the (computationally relevant) universes are Set, and Type_i, where i ranges over natural numbers (0, 1, 2, 3, ...). We have the following inclusions:

Set <= Type_0 <= Type_1 <= Type_2 <= ...

These universes are typed as follows:

 Set : Type_i     for any i

Type_i : Type_j  for any i < j

Like in Hott, this stratification is needed to ensure logical consistency. As Antal pointed out, Set behaves mostly like the smallest Type, with one exception: it can be made impredicative when you invoke coqtop with the -impredicative-set option. Concretely, this means that forall X : Set, A is of type Set whenever A is. In contrast, forall X : Type_i, A is of type Type_(i + 1), even when A has type Type_i.

The reason for this difference is that, due to logical paradoxes, only the lowest level of such a hierarchy can be made impredicative. You may then wonder then why Set is not made impredicative by default. This is because an impredicative Set is inconsistent with a strong form of the axiom of the excluded middle:

forall P : Prop, {P} + {~ P}.

What this axiom allows you to do is to write functions that can decide arbitrary propositions. Note that the {P} + {~ P} type lives in Set, and not Prop. The usual form of the excluded middle, forall P : Prop, P \/ ~ P, cannot be used in the same way, because things that live in Prop cannot be used in a computationally relevant way.

Gaddi

Does that imply that I do not need the Set sort if I do not need impredicativity? – Laconism

I would say so, unless there's some weird corner case of the theory I'm not aware of. I always use Type instead. – Gaddi

What is impredicativity? – Oceanography

@CharlieParker In this context, it means that forall T : Set, S T has type Set (instead of Type) whenever S T : Set. – Gaddi

So, by using the option -impredicative-set, one can prove that (forall P : Prop, {P} + {~ P}) -> False, right? How does it work? – Tko

@Tko This deserves to be posted as a separate question! ;) – Gaddi

I'm confused, what is an concrete example that shows when one would want Set and not Type? – Oceanography

To add more context, apologies for two questions in a row hopefully I doesn't make one to be forgotten...but I am confused what Adam Chlipala means by Second, there is the : Set fragment, which declares that we are defining a datatype that should be thought of as a constituent of programs. Later, which I don't understand what it means. Why didn't he just use Type? – Oceanography

@CharlieParker You should ask this as a separate question so that others can help reply to it! – Gaddi

Sounds good! Here it is: #68057478 hopefully the question is not too convoluted. – Oceanography

Answer 2

In addition to Arthur's answer:

From the fact that Set is located at the bottom of the hierarchy,

it follows that Set is the type of the “small” datatypes and function types, i.e. the ones whose values do not directly or indirectly involve types.

That means the following will fail:

Fail Inductive Ts  : Set :=
  | constrS : Set -> Ts.

with this error message:

Large non-propositional inductive types must be in Type.

As the message suggests, we can amend it by using Type:

Inductive Tt : Type :=
  | constrT : Set -> Tt.

Reference:

• The Essence of Coq as a Formal System by B. Jacobs (2013), pdf.

Throe

I am confused what Adam Chlipala means by Second, there is the : Set fragment, which declares that we are defining a datatype that should be thought of as a constituent of programs. Later, which I don't understand what it means. Why didn't he just use Type? (btw really nice link you sent!) – Oceanography

@CharlieParker I guess Adam wanted to be really precise. Type would have worked too. But one needs to keep in mind that Type really means Type@{level} and the typechecker needs to figure out the universe level. but in this case, one would be delegating this decision to the typechecker. Instead, you can fix it apriori. FWIW, Conor McBride puts it like this: Coq stratifies types by ‘size’ into sets-of-values, sets-of-sets-of-values, and so on. – Throe