I've recently finished Nederpelt and Geuvers Type Theory and Formal Proof, and I remember somewhere in the book the authors mentioned that their $\iota$-descriptors (which are used to refer to the unique members that satisfy some predicates once it's proven) are related to Hilbert's $\varepsilon$-operators, and that they are both weaker than the Axiom of Choice. I believe they stopped at that point and didn't say anything about it ever after.
I didn't give much thoughts to it at the time, but now I'm interested to learn what they meant by that the description operator is weaker than the Axiom of Choice.
I'm going to be sloppy with details here for clarity - in particular, I'm not going to pay attention to exactly how type theory and set theory are interacting. But I don't think this is an issue.
If I understand things correctly, your recollection is off (or the text states things incorrectly) when it comes to the axiom of choice: $\iota$ is unrelated to choice, while $\epsilon$ is actually stronger than choice. (Of course, $\epsilon$ and $\iota$ are related to each other.)
I don't have the book at hand, but I believe $\iota$ behaves roughly as: if there is a unique $a$ such that $\varphi(a)$ holds, then $\iota\varphi(x)$ denotes that $a$, and otherwise $\iota\varphi(x)$ is undefined. This is not related to the axiom of choice, roughly because given $\varphi$ we can tell what $\iota\varphi$ should be in a non-arbitrary way. A bit technically, we can add the $\iota$-operation (in an appropriate way) to ZF without producing any new theorems of set theory.
By contrast, Hilbert's $\epsilon$-operator does not require uniqueness: $\epsilon\varphi(x)$ always denotes an object satisfying $\varphi$ if such an object exists, and is otherwise undefined. Note the fundamental difference between $\epsilon$ and $\iota$: $\epsilon$ has to make nontrivial decisions - namely, whenever we feed it a formula with more than one solution - while $\iota$ doesn't.
Put another way, $\epsilon$ has to make choices, indeed lots of choices, and that's where the connection with the axiom of choice comes from. If we add the $\epsilon$-operator to ZF in a reasonable way, we get full choice back since, given a family $(A_i)_{i\in I}$ of nonempty sets, a choice function is given by $i\mapsto \iota (x\in A_i)$. In fact, $\epsilon$ gives us a strengthening of the axiom of choice, namely global choice: it provides a uniform way to pick an element from a nonempty set.