What is Set in COQ

Question

I am still puzzled by what Install in COQ means. When do I use Install and when do I use Type ?

The Hott Set is defined as a type where evidence of identity is unique. But I think that Kok has a different interpretation.

Answer 1

Set means quite different things in Coq and HoTT.

In Coq, every object has a type, including the types themselves. Type types are commonly called varieties, species, or universes. In Coq, all (all relevantly computable) universes Setand Type_i, where the inatural numbers (0, 1, 2, 3, ...) run through. The following inclusions are available:

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

These universes print as follows:

 Set : Type_i     for any i

Type_i : Type_j  for any i < j

As in Hott, this stratification is necessary to ensure logical consistency. As Antal noted, it Setbehaves basically as the smallest Type, with one exception: it can be made unclean when you call coqtopwith the option -impredicative-set. Specifically, this means that it forall X : Set, Ahas a type Setwhenever A. On the contrary, it forall X : Type_i, Ahas a type Type_(i + 1), even if it Ahas a type Type_i.

, - . , Set . , Set :

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

, , , . , {P} + {~ P} Set, Prop. forall P : Prop, P \/ ~ P , , Prop, .

Answer 2

:

, Set ,

, Set - "" , .. , .

, :

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

:

Type.

, , Type:

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

:

• Coq . . (2013), pdf.