[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
