4.1 Quasi-inverses

We have said that $\mathrm{𝗊𝗂𝗇𝗏}(f)$ 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 $\mathrm{𝗊𝗂𝗇𝗏}(f)$ is not a mere proposition. In this section we exhibit a specific counterexample.

Lemma 4.1.1.

If $f\mathrm{:}A\mathrm{\to }B$ is such that $\mathrm{qinv}\mathit{}\mathrm{(}f\mathrm{)}$ is inhabited, then

$$\mathrm{𝗊𝗂𝗇𝗏}(f)\simeq \left(\prod _{x:A}(x=x)\right).$$

Proof.

By assumption, $f$ is an equivalence; that is, we have $e:\mathrm{𝗂𝗌𝖾𝗊𝗎𝗂𝗏}(f)$ and so $(f,e):A\simeq B$. By univalence, $\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}:(A=B)\to (A\simeq B)$ is an equivalence, so we may assume that $(f,e)$ is of the form $\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}(p)$ for some $p:A=B$. Then by path induction, we may assume $p$ is ${\mathrm{𝗋𝖾𝖿𝗅}}_A$, in which case $\mathrm{𝗂𝖽𝗍𝗈𝖾𝗊𝗏}(p)$ is ${\mathrm{𝗂𝖽}}_A$. Thus we are reduced to proving $\mathrm{𝗊𝗂𝗇𝗏}({\mathrm{𝗂𝖽}}_A)\simeq ({\prod }_{(x:A)}(x=x))$. Now by definition we have

$$\mathrm{𝗊𝗂𝗇𝗏}({\mathrm{𝗂𝖽}}_A)\equiv \sum _{g:A\to A}((g\sim {\mathrm{𝗂𝖽}}_A)\times (g\sim {\mathrm{𝗂𝖽}}_A)).$$

By function extensionality, this is equivalent to

$$\sum _{g:A\to A}((g={\mathrm{𝗂𝖽}}_A)\times (g={\mathrm{𝗂𝖽}}_A)).$$

And by http://planetmath.org/node/87641Exercise 2.10, this is equivalent to

$$\sum _{h:{\sum }_{(g:A\to A)}(g={\mathrm{𝗂𝖽}}_A)}({\mathrm{𝗉𝗋}}_1(h)={\mathrm{𝗂𝖽}}_A)$$

However, by Lemma 3.11.8 (http://planetmath.org/311contractibility#Thmprelem5), ${\sum }_{(g:A\to A)}(g={\mathrm{𝗂𝖽}}_A)$ is contractible with center ${\mathrm{𝗂𝖽}}_A$; therefore by Lemma 3.11.9 (http://planetmath.org/311contractibility#Thmprelem6) this type is equivalent to ${\mathrm{𝗂𝖽}}_A={\mathrm{𝗂𝖽}}_A$. And by function extensionality, ${\mathrm{𝗂𝖽}}_A={\mathrm{𝗂𝖽}}_A$ is equivalent to ${\prod }_{(x:A)}x=x$. ∎

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 $A$ which admits a nontrivial element of ${\prod }_{(x:A)}(x=x)$. Thinking of $A$ as a higher groupoid, an inhabitant of ${\prod }_{(x:A)}(x=x)$ is a natural transformation from the identity functor of $A$ 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 $A$ 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 $A$ with $a\mathrm{:}A$ and $q\mathrm{:}a\mathrm{=}a$ such that

1. The type $a=a$ is a set.

2. For all $x:A$ we have $\parallel a=x\parallel$.

3. For all $p:a=a$ we have $pq=qp$.

Then there exists $f\mathrm{:}{\mathrm{\prod }}_{\mathrm{(}x\mathrm{:}A\mathrm{)}}\mathrm{(}x\mathrm{=}x\mathrm{)}$ with $f\mathit{}\mathrm{(}a\mathrm{)}\mathrm{=}q$.

Proof.

Let $g:{\prod }_{(x:A)}\parallel a=x\parallel$ be as given by 2. First we observe that each type $x{=}_{A}y$ is a set. For since being a set is a mere proposition, we may apply the induction principle of propositional truncation, and assume that $g(x)=\left|p\right|$ and $g(y)=\left|q\right|$ for $p:a=x$ and $q:a=y$. In this case, composing with $p$ and $q^{-1}$ yields an equivalence $(x=y)\simeq (a=a)$. But $(a=a)$ is a set by 1, so $(x=y)$ is also a set.

Now, we would like to define $f$ by assigning to each $x$ the path $g{(x)}^{-1}qg(x)$, but this does not work because $g(x)$ does not inhabit $a=x$ but rather $\parallel a=x\parallel$, and the type $(x=x)$ 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 $x:A$, the type

$$B(x):\equiv \sum _{(r:x=x)}\prod _{(s:a=x)}(r=s^{-1}qs).$$

We claim that $B(x)$ is a mere proposition for each $x:A$. Since this claim is itself a mere proposition, we may again apply induction on truncation and assume that $g(x)=\left|p\right|$ for some $p:a=x$. Now suppose given $(r,h)$ and $(r^{\prime },h^{\prime })$ in $B(x)$; then we have

$$h(p)h^{\prime }{(p)}^{-1}:r=r^{\prime }.$$

It remains to show that $h$ is identified with $h^{\prime }$ 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

$$h(s)=h(p)h^{\prime }{(p)}^{-1}{h}^{\prime }(s)$$

for any $s:a=x$. But each side of this is an equality between elements of $(x=x)$, so it follows from our above observation that $(x=x)$ is a set.

Thus, each $B(x)$ is a mere proposition; we claim that ${\prod }_{(x:A)}B(x)$. Given $x:A$, we may now invoke the induction principle of propositional truncation to assume that $g(x)=\left|p\right|$ for $p:a=x$. We define $r:\equiv p^{-1}qp$; to inhabit $B(x)$ it remains to show that for any $s:a=x$ we have $r=s^{-1}qs$. Manipulating paths, this reduces to showing that $q(p{s}^{-1})=(p{s}^{-1})q$. But this is just an instance of 3. ∎

Theorem 4.1.3.

There exist types $A$ and $B$ and a function $f\mathrm{:}A\mathrm{\to }B$ such that $\mathrm{qinv}\mathit{}\mathrm{(}f\mathrm{)}$ is not a mere proposition.

Proof.

It suffices to exhibit a type $X$ such that ${\prod }_{(x:X)}(x=x)$ is not a mere proposition. Define $X:\equiv {\sum }_{(A:𝒰)}\parallel \mathrm{𝟐}=A\parallel$, as in the proof of Lemma 3.8.5 (http://planetmath.org/38theaxiomofchoice#Thmprelem2). It will suffice to exhibit an $f:{\prod }_{(x:X)}(x=x)$ which is unequal to $\lambda x.{\mathrm{𝗋𝖾𝖿𝗅}}_x$.

Let $a:\equiv (\mathrm{𝟐},\left|{\mathrm{𝗋𝖾𝖿𝗅}}_{\mathrm{𝟐}}\right|):X$, and let $q:a=a$ be the path corresponding to the nonidentity equivalence $e:\mathrm{𝟐}\simeq \mathrm{𝟐}$ defined by $e(0_{\mathrm{𝟐}}):\equiv 1_{\mathrm{𝟐}}$ and $e(1_{\mathrm{𝟐}}):\equiv 0_{\mathrm{𝟐}}$. We would like to apply Lemma 4.1.2 (http://planetmath.org/41quasiinverses#Thmprelem2) to build an $f$. By definition of $X$, equalities in subset types (§3.5 (http://planetmath.org/35subsetsandpropositionalresizing)), and univalence, we have $(a=a)\simeq (\mathrm{𝟐}\simeq \mathrm{𝟐})$, which is a set, so 1 holds. Similarly, by definition of $X$ and equalities in subset types we have 2. Finally, http://planetmath.org/node/87644Exercise 2.13 implies that every equivalence $\mathrm{𝟐}\simeq \mathrm{𝟐}$ is equal to either ${\mathrm{𝗂𝖽}}_{\mathrm{𝟐}}$ or $e$, so we can show 3 by a four-way case analysis.

Thus, we have $f:{\prod }_{(x:X)}(x=x)$ such that $f(a)=q$. Since $e$ is not equal to ${\mathrm{𝗂𝖽}}_{\mathrm{𝟐}}$, $q$ is not equal to ${\mathrm{𝗋𝖾𝖿𝗅}}_a$, and thus $f$ is not equal to $\lambda x.{\mathrm{𝗋𝖾𝖿𝗅}}_x$. Therefore, ${\prod }_{(x:X)}(x=x)$ is not a mere proposition. ∎

More generally, Lemma 4.1.2 (http://planetmath.org/41quasiinverses#Thmprelem2) implies that any “Eilenberg–Mac Lane space” $K(G,1)$, where $G$ is a nontrivial abelian group, will provide a counterexample; see http://planetmath.org/node/87582Chapter 8. The type $X$ we used turns out to be equivalent to $K({\mathbb{Z}}_2,1)$. In http://planetmath.org/node/87579Chapter 6 we will see that the circle ${𝕊}^1=K(\mathbb{Z},1)$ is another easy-to-describe example.

We now move on to describing better notions of equivalence.

Title	4.1 Quasi-inverses