The Coq mailing list

[Eddy Westbrook <westbrook AT kestrel.edu>]

Arnaud,

Yes, I think this is right. Having what I called “SS0” as an axiom does not mean that when you project the first element of an (exists x, P x) that you get what you put into it. In fact, nothing about this axiom prevents it from, say, returning the same value for x for all values of type (exists x, P x). Thus the type (exists (A:Type) (P:A->A->Prop), True) is not really a universal system of notations, even with the SS0 axiom, because you may not be able to get all types A by projecting them out of this type.

-E

On Apr 30, 2014, at 2:05 PM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

After some thought: the statement [exists _:(forall A P, (exists x, P x)->{x|P x}), True] is equiconsistent with than [forall A P, (exists x, P x)->{x|P x}]. But I realise now that the reason why [(exists x, P x)->{x|P x}] is consistent (per Werner), is that the result by Coquand is that the first projection of (exists x, P x) is inconsistent, but a projection comes with an equality rule, which is not the case of the axiom. And I guess that the equality rule matters for the inconsistency result.

So: my bad.

On 28 April 2014 21:05, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

My guess (it's really a guess) is that TTDA is equivalent to (exists _:SS0, True) ( ||SS0|| in the notations of HoTT ). But both of them are sufficiently weaker (as they don't allow to leave Prop) than SS0 so as to be consistent, whereas SS0 isn't. Really not sure though.

On 28 April 2014 20:06, Eddy Westbrook <westbrook AT kestrel.edu> wrote:

Arnaud,

Wait a second, this cannot be quite right. I have been looking at Werner’s “Sets in Types, Types in Sets” paper, where he proves that ZF with inaccessible cardinals is equi-consistent with Coq plus a few axioms, including propositional excluded middle (pEM) and the type-theoretic description axiom (TTDA). I have shown that pEM and TTDA imply the existence of a strong sum axiom that you describe. Specifically, I have shown (in Coq) that

pEM -> TTDA_(i+1) -> (exists _:SS_i , True)

where TTDA_i is TTDA at level i and SS_i is strong sums at level i. (I have attached the Coq file below, so you can double-check that I have gotten everything right.) In fact, I have shown the converse as well, i.e., that the consistency of strong sums is equivalent to that of TTDA at one level higher: it turns out that both of these are equivalent to excluded middle for Type at the same level as the strong sums.

Of course, this seems to contradict part of Coquand’s paper, so I looked back over it again and I think maybe I found an issue in his definition of A_0 for strong sums. Specifically, he defines

A_0 = Sigma (C : Prop) (C -> C -> Prop)

which I do not think satisfies his definition of a universal system of notations, at least not in the Coq type system, because C here has to be a Prop, not an arbitrary type. And, of course, if we switch to

A_0 = Sigma (C : Type) (C -> C -> Prop)

for some given type universe i, then his WF well-roundedness relation moves up to the next universe, and so cannot be captured inside of A_0. Does this seem right to you, or am I missing something?

Thanks,

-Eddy

On Apr 28, 2014, at 1:03 AM, Arnaud Spiwack <aspiwack AT lix.polytechnique.fr> wrote:

Coq is believed to be consistent with the axiom [exists x, P x -> { x | P x }].

For the records, assuming I am parsing this correctly as [ (exists x, P x) -> { x | P x } ]. This is known to be inconsistent in general (you can use it to encode system U). It is a very strong property (because of impredicativity). See, Coquand's An Analysis of Girard's Paradox (LICS 1986).

/Arnaud