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.
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.
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:
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With