[TYPES] Meaning explanations and the invalidity of the law of excluded middle

[Andrej Bauer]

> Relatedly, both MLTT and Nuprl's meaning explanations refute Church's
> Thesis if formulated internally (not only does it fail to hold, it is
> false).

Really? How does (pure!) MLTT refute Church's Thesis? Oh, you're
interpreting it like this:

∏ (f : N → N) ∑ (e : N) ∏ (n m : N) (Id(f n, m) ↔ ∑ (k : N) T(e, n, k)
× Id (U k, m) ?

This says: "For every function f there is a machine e, such that f(n)
= m is equivalent to there existing a run k of e on input n which
results in output m." Cruicially, because we're using pies and sigmas,
e depends on f in an extensional way, i.e., we can extract a map

   godel : (N → N) → N

which calculates such an e, given f. But that's not a contradiction
yet. How do you get a contradiction?

With kind regards,

Andrej