# Axiom of Choice in Intuitionistic Type Theory

I read that in Intuitionistic Type Theory the Axiom of Choice is a theorem that can be stated as:

$$(\forall x \in A) (\exists y \in B(x)) C(x,y) \supset (\exists f \in (\Pi x \in A) B(x)) (\forall x \in A) C(x,Ap(f,x))$$ true

What is the meaning of this expression? I know that $$Ap(f,x)$$ is the result of the application of $$f$$ to $$x$$, so in practice it's $$f(x)$$. I suppose that $$\supset$$ means the implication, so if the left hand term is true then the right hand term is true. I'm trying to understand why the whole expression is the Axiom of Choice formulation, so what does it mean?

I'm unsure if you're getting tripped up on notation or are unfamiliar with this version of the axiom. If we eliminate the dependency of $$B$$ on $$A$$, and use more widely used (I think) notation, we'd have:

$$(∀x \in A. ∃y \in B. C(x,y)) → (∃f \in B^A. ∀x \in A. C(x, f(x))$$

which could be read, "for every entire relation, there is a function contained in it."

However, one thing you should know is that the reason this is a theorem in type theory is that the formula is being interpreted in a way that doesn't exactly cohere with how it is thought of elsewhere. Specifically, it is being translated to the type theoretic:

$$(Πx : A. Σy : B. C(x,y)) → (Σf : A → B. Πx:A. C(x, f(x)))$$

The premise is already the type of functions from $$A$$ to $$B$$-such-that-$$C$$. So this is much like a dependently typed version of:

$$(A → B × C) → (A → B) × (A → C)$$

However, as mentioned above, the premise of the axiom of choice in set theory is usually about an entire relation from $$A$$ to $$B$$-such-that-$$C$$. Traditionally, type theory lacks a good way of specifying such things (at least without building up more machinery for a less straight forward interpretation). With something like a squash type, or propositional truncation from homotopy type theory, we can give a more precise interpretation:

$$(Πx:A. \Vert Σy:B. C(x,y)\Vert) →\VertΣf:A→B. Πx:A. C(x,f(x))\Vert$$

This is not a theorem.

Edit: since you asked, another tack we can take is to keep the dependency of $$B$$ on $$A$$, but get rid of $$C$$, or make it vacuous. In set theory, you might write it something like:

$$(∀x \in A. ∃y. y \in B(x)) → (∃f. f \in \prod_{x\in A} B(x))$$

This would be read, "if every fiber of a family $$B$$ is inhabited (nonempty), then there is a value of the product of $$B$$."

When you interpret this in the same manner as the first translation to type theory, you get the very boring:

$$(Πx:A. B(x)) → (Πx:A. B(x))$$

which is satisfied by the identity function. When you use the more nuanced translation, you get:

$$(Πx:A. \Vert B(x) \Vert) → \Vert Πx:A. B(x) \Vert$$

which is, again, not a theorem.

You could keep $$C$$ around, as well, but in some ways it doesn't add anything to this (you could use $$B'(x) = Σy:B(x). C(x,y)$$). The shift from 'relations from $$A$$ to (fibers of) $$B$$' to 'functions from $$A$$ to (fibers of) $$B$$' is the essential aspect that requires an axiom, and interpreting 'relation' as 'function' is why it is a theorem in the naive translation to type theory.

• Thank you! I'm unfamiliar with type theory. Eliminating the dependency of B on A all is clear. But what about the dependency of B on A? Aug 31, 2022 at 16:01