3.9 The principle of unique choice
The following observation is trivial, but very useful.
If is a mere proposition, then .
Among its important consequences is the following.
Corollary 3.9.2 (The principle of unique choice).
Suppose a type family such that
For each , the type is a mere proposition, and
For each we have .
Then we have .
Immediate from the two assumptions and the previous lemma. ∎
The corollary also encapsulates a very useful technique of reasoning. Namely, suppose we know that , and we want to use this to construct an element of some other type . We would like to use an element of in our construction of an element of , but this is allowed only if is a mere proposition, so that we can apply the induction principle for the propositional truncation ; the most we could hope to do in general is to show . Instead, we can extend with additional data which characterizes uniquely the object we wish to construct. Specifically, we define a predicate such that is a mere proposition. Then from an element of we construct an element such that , hence from we can construct , and because is equivalent to an element of 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 slightly differently. If we are trying to define a function , and depending on an element we are able to prove mere existence of some , we are not done yet because we need to actually pinpoint an element of , not just prove its existence. One option is of course to refine the argument to unique existence of , 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 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 for each to use in defining .
|Title||3.9 The principle of unique choice|