You can model types as a set and sets as types in many ways, so a number of the basic set theory axioms are pretty simple to express as lemmas from type axioms. IIRC you get constructive set theory easy, but do have to define additional axioms typically for ZFC.
I recall that you really need the "C" from ZFC or you'll end-up with a much less comfy realm of mathematics.
So the "C" from ZFC is "challenging" for type theory? Because, and I think I am not that much overshooting, fundamental axioms are really, really simple, even the "C" from ZFC, and if is "challenging" to express it using some fundamental theory, well, not good omens for that theory, or they can rebuild the realm of classic maths with their own "C"??
The axiom of choice entails the law of excluded middle, i.e. it takes you out of constructive mathematics. Mathematicians seem to really like the extended world of ZFC.
I expect there's an equivalent addition to constructive type theory that yields non-constructive type theory. Adding more axioms isn't necessarily making systems better though.
