Mimicking classic set extensionality in Coq

Question

I am interested in strategies for encoding classical mathematics in Coq as a way of learning more about Coq and getting my hands dirty, so to speak.

To that end, I have found this paper. I have read the paper and I understand its motivation (encoding classical mathematics in Coq in sometimes-tricky ways) to an extent, but I don't understand the paper overall very well.

The very first axiom is given below. Its meaning in English is that elements of sets are sets.

(*** interpret types as being classical sets ***)
Definition E := Type.
(*** elements of a set are themselves sets ***)
Parameter R : forall x : E, x -> E.
Axiom R_inj : forall (x : E) (a b : x), R a = R b -> a = b.

The paper mentions Coq 8.0. I'm using Coq 8.15 and the axiom fails to compile:

sh:1 $ coqc set.v
File "./set.v", line 5, characters 42-43:
Error:
In environment
x : E
a : x
b : x
The term "a" has type "x" while it is expected to have type "E".

To resolve this error in my local environment, I tried inlining the parameter R

(*** interpret types as being classical sets ***)
Definition E := Type.

(* Inline the parameter R *)
Axiom R_inj : forall (r : (forall x : E, x -> E)) (x : E) (a b : x), r a = r b -> a = b.

And annoyingly, I get exactly the same error:

sh:1 $ coqc set.v
File "./set.v", line 5, characters 71-72:
Error:
In environment
r : forall x : E, x -> E
x : E
a : x
b : x
The term "a" has type "x" while it is expected to have type "E".

I tried to fix this issue by insisting via axiom on an explicit "value" for R.

In the code sample below, inject is supposed to take any x such that x : k : Type for some type k and convert it into a k.

sh:1 $ cat set.v
(*** interpret types as being classical sets ***)
Definition E := Type.

Definition SetInjector := forall x : E, x -> E.
Axiom inject : SetInjector.

Definition SetInjectorInjective := forall (x : E) (a b : x), (inject a) = (inject b) -> a = b.

This also fails, in the identical way.

sh:1 $ coqc set.v
File "./set.v", line 7, characters 69-70:
Error:
In environment
x : E
a : x
b : x
The term "a" has type "x" while it is expected to have type "E".

Can someone help me understand what is happening here?

1. Has Coq changed its semantics since 8.0?
2. Is there a way to express the intent of this axiom correctly?

Answer 1

My guess is that the Coq code given in the text is missing some context. Probably, the original file was setting the following flag (off by default):

Set Implicit Arguments.

This lets Coq automatically make some arguments implicit (see the reference manual entry for more details). In your case, this would make the first argument of R implicit, letting Coq infer it automatically under the hood.

Having that first argument implicit seems like a good idea, and you have at least three ways to achieve that. You can set the flag globally as above, or locally reproduce its effect just for R, either directly when declaring it

Parameter R : forall {x : E}, x -> E.

(note the curly braces, Coq's syntax for implicit arguments) or afterwards:

Parameter R : forall x : E, x -> E.
Arguments R {_} _.

(again, the curly braces tell Coq the first argument will now be implicit).

All three options have the exact same effect, and let R_inj type as expected.

Answer 2

I stared at the error message for a bit and came up with a solution that type checks:

(*** interpret types as being classical sets ***)
Definition E := Type.
(*** elements of a set are themselves sets ***)
Parameter R : forall x : E, x -> E.
Axiom R_inj : forall (x : E) (a b : x), R x a = R x b -> a = b.

Adding x as an explicit argument to R, making it into a binary rather than unary function, is sufficient to get our small program to compile.

I still don't understand why x wasn't provided in the original paper, or whether the authors did anything that would enable Coq to infer the x argument.