[Agda] Hanging out with the Lean crowd

[Martin Escardo]

On 20/08/2020 21:28, mechvel at scico.botik.ru wrote:
> Probably the majority of people keep in mind a bit another thing:
>   a possibility to use a non-constructive proof, when failed to provide
>   a constructive one.
> 
> Does Agda support such a possibility?
Yes. You can define a type EM that explains what excluded middle is and
then prove e.g. EM -> Cantor-Schroeder-Bernstein.

You can define a type Choice that explains what choice is, and prove
that Choice -> EM. (That type Choice is not the one with the same name
that just happens to hold.)

You can define a type Global-Choice that explains what global choice is
and prove Global-Choice -> ¬ Univalence. But Univalence, Choice and EM
live happily together.

And so on.

I want to use any assumption I like, but also I don't like to be forced
to use assumptions I don't want all the time. I may also want to
occasionally work with assumptions that falsify EM (and hence Choice),
such as "all functions are continuous". It depends on what I am trying
to achieve and what I am talking about (i.e. in what model of type
theory my types live in). If I want my types to be spaces, of course all
functions will be continuous. If I want my types to be recursively
presented sets, of course all functions will be computable. If I want my
types to be classical sets, of course excluded middle and choice will
hold. And so on.

Excluded middle is like parallel postulate in Euclidean geometry: if you
assert it, you get one kind of geometry, and if you negate it you get
another kind. It is meaningless to ask whether the parallel postulate is
true. What you can ask is whether it is true in the particular geometry
you are interested in. The same goes for EM and other classical creatures.

Martin