# 4.1 Quasi-inverses

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

###### Lemma 4.1.1.

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

 $\mathsf{qinv}(f)\simeq\Bigl{(}\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}(x=x)\Bigr{)}.$
###### Proof.

By assumption, $f$ is an equivalence; that is, we have $e:\mathsf{isequiv}(f)$ and so $(f,e):A\simeq B$. By univalence, $\mathsf{idtoeqv}:(A=B)\to(A\simeq B)$ is an equivalence, so we may assume that $(f,e)$ is of the form $\mathsf{idtoeqv}(p)$ for some $p:A=B$. Then by path induction, we may assume $p$ is $\mathsf{refl}_{A}$, in which case $\mathsf{idtoeqv}(p)$ is $\mathsf{id}_{A}$. Thus we are reduced to proving $\mathsf{qinv}(\mathsf{id}_{A})\simeq(\mathchoice{\prod_{x:A}\,}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{% \prod_{(x:A)}}}(x=x))$. Now by definition we have

 $\mathsf{qinv}(\mathsf{id}_{A})\equiv\mathchoice{\sum_{g:A\to A}\,}{\mathchoice% {{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g% :A\to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum% _{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{% \sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}\big{(}(g\sim\mathsf{% id}_{A})\times(g\sim\mathsf{id}_{A})\big{)}.$

By function extensionality, this is equivalent to

 $\mathchoice{\sum_{g:A\to A}\,}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum% _{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle% \sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{% \mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)% }}{\sum_{(g:A\to A)}}}\big{(}(g=\mathsf{id}_{A})\times(g=\mathsf{id}_{A})\big{% )}.$

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

 $\mathchoice{\sum_{h:\mathchoice{\sum_{g:A\to A}\,}{\mathchoice{{\textstyle\sum% _{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{% \mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)% }}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A% \to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}(g=\mathsf{id}_{A})}\,}{% \mathchoice{{\textstyle\sum_{(h:\mathchoice{\sum_{g:A\to A}\,}{\mathchoice{{% \textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A% \to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{% (g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{% \sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}(g=\mathsf{id}_{A}))}% }}{\sum_{(h:\mathchoice{\sum_{g:A\to A}\,}{\mathchoice{{\textstyle\sum_{(g:A% \to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{% \mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)% }}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A% \to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}(g=\mathsf{id}_{A}))}}{\sum_{(h% :\mathchoice{\sum_{g:A\to A}\,}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{% \sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{% \textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A% \to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{% (g:A\to A)}}{\sum_{(g:A\to A)}}}(g=\mathsf{id}_{A}))}}{\sum_{(h:\mathchoice{% \sum_{g:A\to A}\,}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)% }}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A% )}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{% \textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A% \to A)}}}(g=\mathsf{id}_{A}))}}}{\mathchoice{{\textstyle\sum_{(h:\mathchoice{% \sum_{g:A\to A}\,}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)% }}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A% )}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{% \textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A% \to A)}}}(g=\mathsf{id}_{A}))}}}{\sum_{(h:\mathchoice{\sum_{g:A\to A}\,}{% \mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)% }}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A% \to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(% g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}(g=% \mathsf{id}_{A}))}}{\sum_{(h:\mathchoice{\sum_{g:A\to A}\,}{\mathchoice{{% \textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A% \to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{% (g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{% \sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}(g=\mathsf{id}_{A}))}% }{\sum_{(h:\mathchoice{\sum_{g:A\to A}\,}{\mathchoice{{\textstyle\sum_{(g:A\to A% )}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{% \textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A% \to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{% (g:A\to A)}}{\sum_{(g:A\to A)}}}(g=\mathsf{id}_{A}))}}}{\mathchoice{{% \textstyle\sum_{(h:\mathchoice{\sum_{g:A\to A}\,}{\mathchoice{{\textstyle\sum_% {(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{% \mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)% }}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A% \to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}(g=\mathsf{id}_{A}))}}}{\sum_{(% h:\mathchoice{\sum_{g:A\to A}\,}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{% \sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{% \textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A% \to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{% (g:A\to A)}}{\sum_{(g:A\to A)}}}(g=\mathsf{id}_{A}))}}{\sum_{(h:\mathchoice{% \sum_{g:A\to A}\,}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)% }}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A% )}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{% \textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A% \to A)}}}(g=\mathsf{id}_{A}))}}{\sum_{(h:\mathchoice{\sum_{g:A\to A}\,}{% \mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)% }}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A% \to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle\sum_{(% g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}(g=% \mathsf{id}_{A}))}}}(\mathsf{pr}_{1}(h)=\mathsf{id}_{A})$

However, by Lemma 3.11.8 (http://planetmath.org/311contractibility#Thmprelem5), $\mathchoice{\sum_{g:A\to A}\,}{\mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum% _{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{\mathchoice{{\textstyle% \sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)}}}{% \mathchoice{{\textstyle\sum_{(g:A\to A)}}}{\sum_{(g:A\to A)}}{\sum_{(g:A\to A)% }}{\sum_{(g:A\to A)}}}(g=\mathsf{id}_{A})$ is contractible with center $\mathsf{id}_{A}$; therefore by Lemma 3.11.9 (http://planetmath.org/311contractibility#Thmprelem6) this type is equivalent to $\mathsf{id}_{A}=\mathsf{id}_{A}$. And by function extensionality, $\mathsf{id}_{A}=\mathsf{id}_{A}$ is equivalent to $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\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 $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(x=x)$. Thinking of $A$ as a higher groupoid, an inhabitant of $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\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:A$ and $q:a=a$ such that

1. 1.

The type $a=a$ is a set.

2. 2.

For all $x:A$ we have $\mathopen{}\left\|a=x\right\|\mathclose{}$.

3. 3.

For all $p:a=a$ we have $p\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}q=q\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}p$.

Then there exists $f:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}(x=x)$ with $f(a)=q$.

###### Proof.

Let $g:\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:% A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{% \prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x% :A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}\mathopen{}\left\|a=x% \right\|\mathclose{}$ 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)=\mathopen{}\left|p\right|\mathclose{}$ and $g(y)=\mathopen{}\left|q\right|\mathclose{}$ for $p:a=x$ and $q:a=y$. In this case, composing with $p$ and $\mathord{{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 $\mathord{{g(x)}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}q\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}g(x)$, but this does not work because $g(x)$ does not inhabit $a=x$ but rather $\mathopen{}\left\|a=x\right\|\mathclose{}$, 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\mathchoice{\sum_{(r:x=x)}\,}{\mathchoice{{\textstyle\sum_{(r:x% =x)}}}{\sum_{(r:x=x)}}{\sum_{(r:x=x)}}{\sum_{(r:x=x)}}}{\mathchoice{{% \textstyle\sum_{(r:x=x)}}}{\sum_{(r:x=x)}}{\sum_{(r:x=x)}}{\sum_{(r:x=x)}}}{% \mathchoice{{\textstyle\sum_{(r:x=x)}}}{\sum_{(r:x=x)}}{\sum_{(r:x=x)}}{\sum_{% (r:x=x)}}}\mathchoice{\prod_{(s:a=x)}\,}{\mathchoice{{\textstyle\prod_{(s:a=x)% }}}{\prod_{(s:a=x)}}{\prod_{(s:a=x)}}{\prod_{(s:a=x)}}}{\mathchoice{{% \textstyle\prod_{(s:a=x)}}}{\prod_{(s:a=x)}}{\prod_{(s:a=x)}}{\prod_{(s:a=x)}}% }{\mathchoice{{\textstyle\prod_{(s:a=x)}}}{\prod_{(s:a=x)}}{\prod_{(s:a=x)}}{% \prod_{(s:a=x)}}}(r=\mathord{{s}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}q\mathchoice{\mathbin{\raisebox{% 2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}% }{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{% \raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}s).$

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)=\mathopen{}\left|p\right|\mathclose{}$ for some $p:a=x$. Now suppose given $(r,h)$ and $(r^{\prime},h^{\prime})$ in $B(x)$; then we have

 $h(p)\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}\mathord{{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)\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}\mathord{{h^{\prime}(p)}^{-1}}\mathchoice{\mathbin{\raisebox% {2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}% }}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{% \raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}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 $\mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)% }}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}}{\prod% _{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{\textstyle\prod_{(x:A)}}% }{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}B(x)$. Given $x:A$, we may now invoke the induction principle of propositional truncation to assume that $g(x)=\mathopen{}\left|p\right|\mathclose{}$ for $p:a=x$. We define $r:\!\!\equiv\mathord{{p}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}q\mathchoice{\mathbin{\raisebox{% 2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}% }{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{% \raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}p$; to inhabit $B(x)$ it remains to show that for any $s:a=x$ we have $r=\mathord{{s}^{-1}}\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle% \centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1% .075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{% \scriptscriptstyle\,\centerdot\,}}}q\mathchoice{\mathbin{\raisebox{2.15pt}{% \displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}s$. Manipulating paths, this reduces to showing that $q\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{% \raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,% \centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,% }}}(p\mathchoice{\mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{% \mathbin{\raisebox{2.15pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{% \scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle% \,\centerdot\,}}}\mathord{{s}^{-1}})=(p\mathchoice{\mathbin{\raisebox{2.15pt}% {\displaystyle\centerdot}}}{\mathbin{\raisebox{2.15pt}{\centerdot}}}{% \mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}}}{\mathbin{\raisebox% {0.43pt}{\scriptscriptstyle\,\centerdot\,}}}\mathord{{s}^{-1}})\mathchoice{% \mathbin{\raisebox{2.15pt}{\displaystyle\centerdot}}}{\mathbin{\raisebox{2.1% 5pt}{\centerdot}}}{\mathbin{\raisebox{1.075pt}{\scriptstyle\,\centerdot\,}% }}{\mathbin{\raisebox{0.43pt}{\scriptscriptstyle\,\centerdot\,}}}q$. But this is just an instance ofΒ 3. β

###### Theorem 4.1.3.

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

###### Proof.

It suffices to exhibit a type $X$ such that $\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)% }}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod% _{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}% }{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}(x=x)$ is not a mere proposition. Define $X:\!\!\equiv\mathchoice{\sum_{A:\mathcal{U}}\,}{\mathchoice{{\textstyle\sum_{(% A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:% \mathcal{U})}}}{\mathchoice{{\textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:% \mathcal{U})}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U})}}}{\mathchoice{{% \textstyle\sum_{(A:\mathcal{U})}}}{\sum_{(A:\mathcal{U})}}{\sum_{(A:\mathcal{U% })}}{\sum_{(A:\mathcal{U})}}}\mathopen{}\left\|\mathbf{2}=A\right\|\mathclose{}$, as in the proof of Lemma 3.8.5 (http://planetmath.org/38theaxiomofchoice#Thmprelem2). It will suffice to exhibit an $f:\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:% X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}(x=x)$ which is unequal to ${\lambda}x.\,\mathsf{refl}_{x}$.

Let $a:\!\!\equiv(\mathbf{2},\mathopen{}\left|\mathsf{refl}_{\mathbf{2}}\right|% \mathclose{}):X$, and let $q:a=a$ be the path corresponding to the nonidentity equivalence $e:\mathbf{2}\simeq\mathbf{2}$ defined by $e({0_{\mathbf{2}}}):\!\!\equiv{1_{\mathbf{2}}}$ and $e({1_{\mathbf{2}}}):\!\!\equiv{0_{\mathbf{2}}}$. 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(\mathbf{2}\simeq\mathbf{2})$, 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 $\mathbf{2}\simeq\mathbf{2}$ is equal to either $\mathsf{id}_{\mathbf{2}}$ or $e$, so we can showΒ 3 by a four-way case analysis.

Thus, we have $f:\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:% X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{% \prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x% :X)}}}{\prod_{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}(x=x)$ such that $f(a)=q$. Since $e$ is not equal to $\mathsf{id}_{\mathbf{2}}$, $q$ is not equal to $\mathsf{refl}_{a}$, and thus $f$ is not equal to ${\lambda}x.\,\mathsf{refl}_{x}$. Therefore, $\mathchoice{\prod_{x:X}\,}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod_{(x:X)% }}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}}{\prod% _{(x:X)}}{\prod_{(x:X)}}{\prod_{(x:X)}}}{\mathchoice{{\textstyle\prod_{(x:X)}}% }{\prod_{(x:X)}}{\prod_{(x:X)}}{\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 $\mathbb{S}^{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
\metatable