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

[Thomas Streicher]

On Tue, Oct 17, 2017 at 05:26:23AM -0700, Jon Sterling wrote:
> Dear Andrej and Thomas,
> 
> I was referring to extensional MLTT (MLTT 1979), not intensional MLTT
> (for which the question is still open, I believe); I believe the result
> is from Troelstra, but I can try and dig up the details.

Sure, one knows that relative to HA_omega the combination of
extensionality, choice and continuity is inconistent simply because
you can't tell a program from an initial segment of the function it
computes.

Thomas