The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Building a bit on Hugo's answer, from a more pragmatic perspective, to me "i ≤ j" means "Coq is allowed to equate i and j at any point if that's what's needed to make a term be well-typed".  However, equating [Set] and [Prop] in an unpredictable manner would be terrible.  Just because I wrote [Definition foo : Set := forall x : Set, x -> x.] somewhere, I don't want Coq to randomly collapse some of my types to [Prop]; this would break elimination principles (there's a special rule that says you can't eliminate a [Prop] when building non-[Prop] things), and it would break extraction (because now some of my things that I told Coq to put in [Set] will end up in [Prop], and thus be erased by extraction).

On Thu, Jan 19, 2017 at 5:59 PM Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:

Hi,

To recenter on the initial question, let us first notice that the
"Prop < Set" mentioned by Matej is printed by the command "Print
Universes". It does not reflect the definition of the logic of Coq but
instead the internal state of the universe-acyclicity algorithm that
Coq uses to ensure that the different occurrences of the anonymous
"Type" in a development can be interpreted within the linear hierarchy
Type(n). (The Type(n) hierarchy is the one which serves as reference
in papers and in particular in Chapter 4 of the reference manual.)

The "Prop < Set" is technical: the universe-acyclicity algorithm
internally needs to consider Prop <> Set to ensure that Prop is not
accidentally equated to Set (*). Matthieu, who introduced this for the
polymorphism of universes, confirmed.

However, at the logical level, there is no constraint that Prop should
be different from Set.

By looking at the rules of the logic of Coq, i.e. at the rules of the
Calculus of Inductive Constructions, one can check that all rules
involving subtyping (Section 4.4 of the reference manual) are
insensitive to whether one sets "Prop < Set" or "Prop <= Set", so why
not to start from "Prop <= Set" which is easier to manipulate since
the general subtyping relation has to be reflexive, hence large, and
that using explicitly a different relation < would just make things
more complicated.

Moreover, not only no rules of the logic is able to state Prop <> Set
but every rule about Prop also remains valid when interpreted in
impredicative Set and every rule about predicative Set remains
derivable as well when interpreted in impredicative Set. This gives
place for models where Set is interpreted impredicatively and Prop is
equated with Set. Thus, thinking at Prop subtype of Set in terms of
the large relation "<=" is the natural expectation in order to support
these models.

The above should be enough to answer yes to Matej's questions about <
vs <= but let me now generalize the discussion and show the basic
different possible models of the universe hierarchy of Coq. Let me
first remind the full hierarchy for typing and subtyping (**):

  Prop               }
  predicative Set    } : Type(1) : Type(2) : ...
  impredicative Set  }

  Prop <= { predicative Set   } <= Type(1) <= Type(2) <= ...  (***)
          { impredicative Set }

This hierarchy is designed so that it can basically support three
models, leading to five models if we distinguish between the theory
with or without option -impredicative-set, the three models depending
on whether Prop is taken proof-relevant or not and whether predicative
Set is "small" or not. In particular, one of the three models
identifies Prop with Set impredicative.

Let me give these "interesting" models. In the set-theoretic view at
them, "<=" is inclusion, "<" is strict inclusion, ":" is belonging and
Type(i) is the i-th inaccessible cardinal, except in the third model
where it is the (i+1)-ith inaccessible cardinal.

1. The "standard" interpretation of option -impredicative-set with
Prop a (two-element) proof-irrelevant universe:

  Prop < (impr) Set < Type(1) < Type(2) < ...
  Prop, (impr) Set  : Type(1) : Type(2) : ...

2. The Prop-relevant interpretation of option -impredicative-set (as
mentioned above):

  Prop = (impr) Set < Type(1) < Type(2) < ...
  Prop = (impr) Set : Type(1) : Type(2) : ...

3. The "standard" interpretation with Prop irrelevant and Set seen as an
extra Type(0) at the bottom of the predicative hierarchy of Type (as
implicitly expected by Abhishek):

  Prop < (pred) Set = Type(0) < Type(1) < Type(2) < ...
  Prop : (pred) Set = Type(0) : Type(1) : Type(2) : ...

4. The interpretation with Prop irrelevant and predicative Set as a
small universe, i.e. as a universe of subsets of terms like
impredicative Set would be; this is basically the equivalent of 1.
without -impredicative-set:

  Prop < (pred-as-impr) Set < Type(1) < Type(2) < ...
  Prop, (pred-as-impr) Set  : Type(1) : Type(2) : ...

5. The Prop-relevant interpretation with predicative Set being
interpreted within impredicative Set; this is the equivalent of 2.
without -impredicative-set:

  Prop = (pred-as-impr) Set < Type(1) < Type(2) < ...
  Prop = (pred-as-impr) Set : Type(1) : Type(2) : ...

Then, regarding the various issues raised in the discusion, we can
state the following properties of the hierarchy:

- Prop and Set are indeed both at the bottom of the typing hierarchy;
- Prop is at the bottom of the subtyping hierarchy;
- impredicative Set is allowed to be thought at the bottom of the
  subtyping hierarchy together with Prop even though the logic does
  not enforce it (thanks to subtyping not being strict);
- all rules about Prop are valid for impredicative Set; in particular,
  any judgement of Coq can be turned into a judgement where Prop and
  impredicative Set are equated;
- all rules about predicative Set are derivable when Set is
  interpreted impredicatively; in particular, even without the option
  -impredicative-set, one can interpret Coq in a model where both Prop
  and Set are impredicative and equated;
- predicative Set is also allowed to be thought at the bottom of the
  subtyping hierarchy together with Prop, both being embedded into the
  same impredicative set, even though the logic does not enforce it;
- as emphasized by Bruno, that Prop is not directly of type Set but of
  type Type(1) is to have a way to ensure that Set can remain small
  enough; this allows to support models 1, 2, 4 and 5.

Anyway, coming back to the initial issue, removing "Prop < Set" from
the display of "Print Universes" would certainly be better to avoid
that such confusion arise again.

This is what I can think of so far.

Hugo

(*) In particular, changing the line "enforce_univ_lt Level.prop
Level.set empty" into "enforce_univ_le Level.prop Level.set empty"
would be incorrect, unless other means are used to ensure that the
algorithm does not eventually incorrectly conclude that Prop = Set is
part of the logic.

(**) Depending on terminology. For instance, at the time of the
Coq'Art, the hierarchy started to number Type from 0 (i.e.
Prop,Set : Type(0) : Type(1) etc.).

(***) One can certainly also contemplate having both predicative Set
and impredicative Set living together in the same system. In this
case, we would have had predicative-set <= impredicative-set, but with
model 3 being excluded.