3.9 The principle of unique choice

The following observation is trivial, but very useful.

Lemma 3.9.1.

If $P$ is a mere proposition, then $P\mathrm{\simeq }\mathrm{\parallel }P\mathrm{\parallel }$.

Proof.

Of course, we have $P\to \parallel P\parallel$ by definition.And since $P$ is a mere proposition, the universal property of $\parallel P\parallel$ applied to ${\mathrm{𝗂𝖽}}_P:P\to P$ yields $\parallel P\parallel \to P$.These functions are quasi-inverses by Lemma 3.3.3 (http://planetmath.org/33merepropositions#Thmprelem2).∎

Among its important consequences is the following.

Corollary 3.9.2 (The principle of unique choice).

Suppose a type family $P\mathrm{:}A\mathrm{\to }\mathrm{U}$ such that

1. For each $x$, the type $P(x)$ is a mere proposition, and

2. For each $x$ we have $\parallel P(x)\parallel$.

Then we have ${\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}P\mathit{}\mathrm{(}x\mathrm{)}$.

Proof.

Immediate from the two assumptions and the previous lemma.∎

The corollary also encapsulates a very useful technique of reasoning.Namely, suppose we know that $\parallel A\parallel$, and we want to use this to construct an element of some other type $B$.We would like to use an element of $A$ in our construction of an element of $B$, but this is allowed only if $B$ is a mere proposition, so that we can apply the induction principle for the propositional truncation $\parallel A\parallel$; the most we could hope to do in general is to show $\parallel B\parallel$.Instead, we can extend $B$ with additional data which characterizes uniquely the object we wish to construct.Specifically, we define a predicate $Q:B\to 𝒰$ such that ${\sum }_{(x:B)}Q(x)$ is a mere proposition.Then from an element of $A$ we construct an element $b:B$ such that $Q(b)$, hence from $\parallel A\parallel$ we can construct $\parallel {\sum }_{(x:B)}Q(x)\parallel$, and because $\parallel {\sum }_{(x:B)}Q(x)\parallel$ is equivalent to ${\sum }_{(x:B)}Q(x)$ an element of $B$ may be projected from it.An example can be found in http://planetmath.org/node/87853Exercise 3.19.

A similar issue arises in set-theoretic mathematics, although it manifests slightlydifferently. If we are trying to define a function $f:A\to B$, and depending on anelement $a:A$ we are able to prove mere existence of some $b:B$, we are not done yetbecause we need to actually pinpoint an element of $B$, not just prove its existence.One option is of course to refine the argument to unique existence of $b:B$, as we did in type theory. But in set theory the problem can often be avoided more simply by an application of the axiom of choice, which picks the required elements for us.In homotopy type theory, however, quite apart from any desire to avoid choice, the available forms of choice are simply less applicable, since they require that the domain of choice be a set.Thus, if $A$ is not a set (such as perhaps a universe $𝒰$), there is no consistent form of choice that will allow us to simply pick an element of $B$ for each $a:A$ to use in defining $f(a)$.