In intuitionistic mathematics, an axiom of choice of the form
$$ \forall x \exists y R(x,y) \rightarrow \exists f \forall x R(x, fx) $$
is valid by the meaning of the quantifiers (comp. Dummett, Elements of Intuitionism, 2000).
In intuitionistic type theory, it is possible to actually prove the axiom of choice. For example,
$$ (\lambda z)((\lambda x) p_{left}(z(x)),(\lambda x)p_{right}(z(x))) $$
is a proof-object for an axiom of choice of the form
$$ (\Pi x:A)(\Sigma y:B)R \rightarrow (\Sigma f :(\Pi x:A)B)(\Pi x:A)R(f(x)/y), $$ where $p_{left}$ and $p_{right}$ are the projection-functions (comp. Martin-Löf, "Constructive Mathematics and Computer Programming", 1982).
What I am interest in is the precise relationship between predicate logic and type theory. Can the axiom of choice be proved in the former, or is the more expressive language of type theory necessary, which can refer to proof-objects and constructions directly? According to Dummett, in intuitionistic logic, the axiom of choice is true due to the constructivist meaning of the quantifiers. But this does not correspond to a formal proof within the system, but a meta-theoretical result.
Now, my feeling is the following: predicate logic cannot properly represent constructions or proof-objects. But in Martin-Löf's proof of the choice axiom, proof-objects are directly operated on. Therefore, while in intuitionistic predicate logic, the axiom of choice is an axiom properly so-called, i.e. an unprovable principle that we accept due to our informal understanding, it becomes provable in the more expressive system of intuitionistic type theory. Am I correct here, or is this a misunderstanding?