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

Thomas Streicher <streicher-H0bhvm5RIPJmTlJ5tp4iNa5Fl2EJEGXphC4ANOJQIlc@public.gmane.org>
Newsgroups gmane.comp.science.types
Message-ID <[email protected]> 
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

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
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.