> An interesting example is the Axiom of Choice which is, naively encoded, a theorem of intuitionistic logic.

Naïvely encoded in Martin-Löf type theory, that is.