The curry howard isomorphism states that proofs in intuitionist logic can be represented as terms, and theorems as types.
However, I'm wondering: if we add the classical logical axioms like LEM (and the axiom of choice?), is it then possible to do all classical proofs in type theory?
Or are only theorems that are provable from intuitionist logic, provable in type theory?
With both LEM and a type theoretic analogue of the Axiom of Choice, you do end up with a system at least as strong as ZFC. A Coq development demonstrating this is here, created by the author of Sets in types, types in sets. That paper actually claims even more, namely that ZFC+$n$ inaccessible cardinals is encodable into the Calculus of Inductive Constructions (plus the above axioms) with $n+1$ universes. It also goes the other way and encodes CIC with $n$ universes into ZFC + $n$ inaccessible cardinals.
The Coq development actually proves all of the axioms of ZFC except replacement and choice without assuming any axioms (not even LEM). That is, it shows that Coq can encode an intuitionistic variant $Z$ and classical $Z$ if you do include LEM, though CIC(+LEM) is likely quite a bit stronger than $Z$ due to its higher order features. If we assume a type theoretic Axiom of Choice but not LEM, we can prove the Axiom Schema of Collection which is equivalent to the Axiom Schema of Replacement when we add LEM.