[ 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
