Extensionality Versus Constructivity
Silvio Valentini · Mathematical logic quarterly · 2002
We analyze some extensions of Martin-Löf 's constructive type theory by means of extensional set constructors and we show that often the most natural requirements over them lead to classical logic or even to inconsistency.