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

[Jon Sterling]

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.

Best,
Jon


On Tue, Oct 17, 2017, at 03:05 AM, Thomas Streicher wrote:
> Of course, for various reasons CT is not derivable in MLTT. It's
> rather the opposite which is an open question, namely whether
> intensional MLTT is consistent with CT formulated via a \Sigma-type.
> 
> This question has been brought up quite some time ago by Milly Maietti
> and is still open.
> 
> Thomas