Axiom of Choice - Type Theory (Proof)

Background

In Intuitionistic Type Theory (p. 27-28), Martin Löf provides a proof of the axiom of choice that is constructively valid. This version is considerably weaker than the ordinary set theory version, since there are no quotient types. Now, quotients can to a certain extent be simulated using setoids, and thus the axiom of choice may be reformulated to what Martin Löf (2004) calls Zermelo's axiom of choice. This axiom is non-constructive, as it implies PEM (Diaconescu's theorem). Nonetheless, there are special cases of Zermelo's axiom of choice, which are provable in type theory. I have heard that one of these is the so-called axiom of dependent choice, which can be stated as:

For every set $A$ and for every binary relation $R$ on $A$: \begin{equation} (\forall x:A)(\exists y:A)R(x,y) \supset (\forall x:A)(\exists f:N \to A)I(A,\text{Ap}(f,0),x) \land (\forall n:N)R(\text{Ap}(f,n),\text{Ap}(f,S(n))) \end{equation}

Now, my question is how exactly would one go about proving this result constructively? Would it be to any help to use the version of axiom of choice which Martin Löf proved in Intuitionistic Type Theory?

We want to find a proof term for the following type: $$ (\forall x: A. \exists y: A. R(x,y)) \to \forall x: A. \exists f: \mathbb{N} \to A. f(0) = x \,\land\, \forall n: \mathbb{N}. R(f(n), f(\mathsf{succ}(n)))$$

Let $h: \forall x: A. \exists y: A. R(x, y)$, and $x : A$. We need to exhibit a function $f: \mathbb{N} \to A$ and a proof term for the required property. Intuitively, we want $f$ such that

$$\left\{\begin{array}{l} f(0) = x\\ f(\mathsf{succ}(n)) = \pi_1 (h(f(n))) \end{array}\right.$$

therefore we let $f = \lambda n: \mathbb{N}. \mathsf{natrec}(n,\,x,\, \lambda n': \mathbb{N}. \lambda y: A. \pi_1 (h(y)))$. Then you have that $f(0)$ normalizes to $x$, and so $\mathsf{id}(x)$ is a proof of $f(0) = x$. Now, let $n: \mathbb{N}$. We want to prove that $R(f(n),f(\mathsf{succ}(n)))$. But this is given precisely by $\pi_2 (h(f(n)))$, since $f(\mathsf{succ}(n))$ normalizes to $\pi_1 (h(f(n)))$. In conclusion, a proof term for the proposition would be:

$$\lambda h: \forall x: A. \exists y: A. R(x, y). \lambda x: A.\\ \langle \lambda n: \mathbb{N}. \mathsf{natrec}(n,\,x,\, \lambda n': \mathbb{N}. \lambda y: A. \pi_1 (h(y))),\\ \langle \mathsf{id}(x), \lambda n: \mathbb{N}. \pi_2 (h(\mathsf{natrec}(n,\,x,\, \lambda n': \mathbb{N}. \lambda y: A. \pi_1 (h(y))))) \rangle \rangle $$