We have said that is unsatisfactory because it is not a mere proposition, whereas we would rather that a given function can “be an equivalence” in at most one way. However, we have given no evidence that is not a mere proposition. In this section we exhibit a specific counterexample.
If is such that is inhabited, then
By assumption, is an equivalence; that is, we have and so . By univalence, is an equivalence, so we may assume that is of the form for some . Then by path induction, we may assume is , in which case is . Thus we are reduced to proving . Now by definition we have
By function extensionality, this is equivalent to
And by http://planetmath.org/node/87641Exercise 2.10, this is equivalent to
However, by Lemma 3.11.8 (http://planetmath.org/311contractibility#Thmprelem5), is contractible with center ; therefore by Lemma 3.11.9 (http://planetmath.org/311contractibility#Thmprelem6) this type is equivalent to . And by function extensionality, is equivalent to . ∎
We remark that http://planetmath.org/node/87864Exercise 4.3 asks for a proof of the above lemma which avoids univalence.
Thus, what we need is some which admits a nontrivial element of . Thinking of as a higher groupoid, an inhabitant of is a natural transformation from the identity functor of to itself. Such transformations are said to form the center of a category, since the naturality axiom requires that they commute with all morphisms. Classically, if is simply a group regarded as a one-object groupoid, then this yields precisely its center in the usual group-theoretic sense. This provides some motivation for the following.
Suppose we have a type with and such that
The type is a set.
For all we have .
For all we have .
Then there exists with .
Let be as given by 2. First we observe that each type is a set. For since being a set is a mere proposition, we may apply the induction principle of propositional truncation, and assume that and for and . In this case, composing with and yields an equivalence . But is a set by 1, so is also a set.
Now, we would like to define by assigning to each the path , but this does not work because does not inhabit but rather , and the type may not be a mere proposition, so we cannot use induction on propositional truncation. Instead we can apply the technique mentioned in §3.9 (http://planetmath.org/39theprincipleofuniquechoice): we characterize uniquely the object we wish to construct. Let us define, for each , the type
We claim that is a mere proposition for each . Since this claim is itself a mere proposition, we may again apply induction on truncation and assume that for some . Now suppose given and in ; then we have
It remains to show that is identified with when transported along this equality, which by transport in identity types and function types (§2.11 (http://planetmath.org/211identitytype),§2.9 (http://planetmath.org/29pitypesandthefunctionextensionalityaxiom)), reduces to showing
for any . But each side of this is an equality between elements of , so it follows from our above observation that is a set.
Thus, each is a mere proposition; we claim that . Given , we may now invoke the induction principle of propositional truncation to assume that for . We define ; to inhabit it remains to show that for any we have . Manipulating paths, this reduces to showing that . But this is just an instance of 3. ∎
There exist types and and a function such that is not a mere proposition.
It suffices to exhibit a type such that is not a mere proposition. Define , as in the proof of Lemma 3.8.5 (http://planetmath.org/38theaxiomofchoice#Thmprelem2). It will suffice to exhibit an which is unequal to .
Let , and let be the path corresponding to the nonidentity equivalence defined by and . We would like to apply Lemma 4.1.2 (http://planetmath.org/41quasiinverses#Thmprelem2) to build an . By definition of , equalities in subset types (§3.5 (http://planetmath.org/35subsetsandpropositionalresizing)), and univalence, we have , which is a set, so 1 holds. Similarly, by definition of and equalities in subset types we have 2. Finally, http://planetmath.org/node/87644Exercise 2.13 implies that every equivalence is equal to either or , so we can show 3 by a four-way case analysis.
Thus, we have such that . Since is not equal to , is not equal to , and thus is not equal to . Therefore, is not a mere proposition. ∎
More generally, Lemma 4.1.2 (http://planetmath.org/41quasiinverses#Thmprelem2) implies that any “Eilenberg–Mac Lane space” , where is a nontrivial abelian group, will provide a counterexample; see http://planetmath.org/node/87582Chapter 8. The type we used turns out to be equivalent to . In http://planetmath.org/node/87579Chapter 6 we will see that the circle is another easy-to-describe example.
We now move on to describing better notions of equivalence.