[Agda] Hanging out with the Lean crowd

[mechvel at scico.botik.ru]

On 2020-08-21 23:21, Martin Escardo wrote:
> You don't think the model in which types are spaces and functions are
> continuous convincing enough? Excluded middle is not continuous.


Too abstruse, unnatural. To perceive this I need to study attentively in 
what
precisely way types correspond to (topological? metric?) spaces, and so 
on.
An artificial thing.
It has sense to consider this only if simpler explanations are not 
found.

I mean a philosophical question about nature, to which it is applied our 
basic
intuition.
This is not a question about topological spaces and continuous maps.
Much simpler: it is about a certain concrete trivial discrete machine.

With Lobachevsky's model for breaking the fifth postulate in geometry, 
it is clear,
the effect is visible. So that none would tell "my intuition does not 
agree".

Now, with excluded middle and a discrete machine F:
it is given a simple machine F the checks (P? n) and searches through 
Nat,
as it has been specified earlier.
"(1) If F stops, then we derive the goal G from this fact.
  (2) If F never stops, then we derive the goal G from this fact in 
another way.
  Hence G is proved
  - despite that it is not given a proof neither for the condition in (1) 
nor for
  the condition in (2).
"
Constructivism says: this is not a proof.
Does it say this?
Constructivism says:
because there are considered only the cases "F stops" and "F never 
stops".
And as any third case is not evidently excluded, not all possibilities 
have been
considered.
Does constructivism say this?

If it does, then let it describe an example:  how can it look any such 
possibility
which differs from (1) and from (2) ?

Lobachevsky's model demonstrates the possibility of breaking the fifth 
postulate
by showing a bunch of different curves which are put "straight lines", 
which
contain the same point and which are parallel to the same "straight 
line"
("parallel" means "does not intersect with").
This picture agrees with our intuition.

Similarly, how may it look the third possibility for F, so that this 
description
will agree with our intuition?

--
SM