What exactly is a Set in COQ

问题:

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.

回答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.

回答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.