4.1 Quasi-inverses
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.
Lemma 4.1.1.
If is such that is inhabited, then
Proof.
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.
Lemma 4.1.2.
Suppose we have a type with and such that
- 1.
The type is a set.
- 2.
For all we have .
- 3.
For all we have .
Then there exists with .
Proof.
Let be as given by 2. First weobserve that each type is a set. For since being a set is a mereproposition, 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 isa 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 applythe technique mentioned in §3.9 (http://planetmath.org/39theprincipleofuniquechoice): we characterizeuniquely the object we wish to construct. Let us define, for each , thetype
We claim that is a mere proposition for each .Since this claim is itself a mere proposition, we may again apply induction ontruncation 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.∎
Theorem 4.1.3.
There exist types and and a function such that is not a mere proposition.
Proof.
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.