[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-23 00:21, mechvel at scico.botik.ru wrote:
> Guillaume,
> 
> thank you for explaining things in simple words.
> 
> On 2020-08-22 18:21, Guillaume Brunerie wrote:
>> [..]
> 
>> Not that there is anything wrong with that, you are free to believe
>> whatever you want, but I still find it a bit strange to
>> unconditionally accept the existence of infinite sets given that our
>> entire experience of life is finite.
>> [..]

Personally, I somehow believe in platonism, in that it is set 
independently of our knowledge
for each statement and each interpretation of whether it is true there 
or not,
that, in particular, all this is solved somewhere for infinite objects.

But this is only a belief. And it is a strong assumption.

So that if something can be proved without using excluded middle, it is 
desirable
to do this.
Also everyone will agree with that
      existence proof + algorithm to construct the corresponding object
is essentially more than only an abstract existence proof.

Regards,

--
SM