The Type-Theoretic Axiom of Choice

I’ve been reading through the Homotopy Type Theory book [1] recently and it presented a theorem resembling the Axiom of Choice.

Due to the constructive nature of intuitionistic type theory, we get a choice-like theorem for free. For some type universe, \(\mathcal{U}\), types \(A, B\) in this universe and some relation \(R : A \rightarrow B \rightarrow \mathcal{U} \) on elements of these types, we can prove that if for every \(x : A\) there is \(y : B\) such that \(R(x, y)\) holds then there is a function \(f : A \rightarrow B\) such that for all \(x : A\), \(R(x, f(x))\) holds.

Put precisely, the following type is inhabited \[\prod_{A, B : \mathcal{U}} \prod_{R : A \rightarrow B \rightarrow \mathcal{U}} \left(\prod_{x : A} \sum_{y : B} R(x, y) \right) \rightarrow \sum_{f : A \rightarrow B} \prod_{x : A} R(x, f(x)) \]

We show this by constructing a term, \(\mathtt{ac}\), that has this type. Clearly [2] we have

\[\mathtt{ac}_{A, B, R} = \lambda f. \left(\lambda x. \mathtt{pr}_{1}(f(x)), \lambda x. \mathtt{pr}_{2}(f(x))\right) \]

The following theorem involving propositional truncation however does not hold.

\[ \prod_{A, B : \mathcal{U}} \prod_{R : A \rightarrow B \rightarrow \mathcal{U}} \left(\prod_{x : A} \left|\left|\sum_{y : B} R(x, y)\right|\right| \right) \rightarrow \left|\left|\sum_{f : A \rightarrow B} \prod_{x : A} R(x, f(x)) \right|\right| \]

[1]: Homotopy type theory: Univalent foundations of mathematics. The Univalent Foundations Program, Institute for Advanced Study

[2]: This is a joke