℩-descriptor and the axiom of choice? 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.
 A: 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.
