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

[Thomas Streicher]

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