axiom of choice and Martin-Löf Intuitionistic Set Theory

[juan_gandhi]

So, I took a look at this clarification from Stanford texts.

And so, it seems like yes, the axiom of choice as formulated in his so-called intuitionistic set theory is actually the corollary of what one could call axiomatics of the intuitionistic set theory if there were one. What there is is a set of vague intuitive assumptions.

Intuitive is not intuitionistic, you know.

And AC implies Boolean logic, in case you did not know.

So, I think now that it is all wrong.

Basically, there's no such thing as Intuitionistic Set Theory.

But a funny, although hardly provable, corollary of all this is that dependent types imply booleanness. In the form it is now popularized.

Personally, I don't believe it. I believe we still can have dependent types (objects of the form ΠA_{x) without having to have Boolean logic.}