equivalences.tex

\chapter{Equivalences}
\label{cha:equivalences}

We now study in more detail the notion of \emph{equivalence of types} that was introduced briefly in \cref{sec:basics-equivalences}.
Specifically, we will give several different ways to define a type $\isequiv(f)$ having the properties mentioned there.
Recall that we wanted $\isequiv(f)$ to have the following properties, which we restate here:
\begin{enumerate}
\item $\qinv(f) \to \isequiv (f)$.\label{item:beb1}
\item $\isequiv (f) \to \qinv(f)$.\label{item:beb2}
\item $\isequiv(f)$ is a mere proposition.\label{item:beb3}
\end{enumerate}
Here $\qinv(f)$ denotes the type of quasi-inverses to $f$:
\begin{equation*}
  \sm{g:B\to A} \big((f \circ g \htpy \idfunc[B]) \times (g\circ f \htpy \idfunc[A])\big).
\end{equation*}
By function extensionality, it follows that $\qinv(f)$ is equivalent to the type
\begin{equation*}
  \sm{g:B\to A} \big((f \circ g = \idfunc[B]) \times (g\circ f = \idfunc[A])\big).
\end{equation*}
We will define three different types having properties~\ref{item:beb1}--\ref{item:beb3}, which we call
\begin{itemize}
\item half adjoint equivalences,
\item bi-invertible maps,
  \index{function!bi-invertible}
  and
\item contractible functions.
\end{itemize}
We will also show that all these types are equivalent.
These names are intentionally somewhat cumbersome, because after we know that they are all equivalent and have properties~\ref{item:beb1}--\ref{item:beb3}, we will revert to saying simply ``equivalence'' without needing to specify which particular definition we choose.
But for purposes of the comparisons in this chapter, we need different names for each definition.

Before we examine the different notions of equivalence, however, we give a little more explanation of why a different concept than quasi-invertibility is needed.

\section{Quasi-inverses}
\label{sec:quasi-inverses}

\index{quasi-inverse|(}%
We have said that $\qinv(f)$ is unsatisfactory because it is not a mere proposition, whereas we would rather that a given function could ``be an equivalence'' in at most one way.
However, we have given no evidence that $\qinv(f)$ is not a mere proposition.
In this section we exhibit a specific counterexample.

\begin{lem}\label{lem:qinv-autohtpy}
  If $f:A\to B$ is such that $\qinv (f)$ is inhabited, then
  \[\eqv{\qinv(f)}{\Parens{\prd{x:A}(x=x)}}.\]
\end{lem}
\begin{proof}
  By assumption, $f$ is an equivalence; that is, we have $e:\isequiv(f)$ and so $(f,e):\eqv A B$.
  By univalence, $\idtoeqv:(A=B) \to (\eqv A B)$ is an equivalence, so we may assume that $(f,e)$ is of the form $\idtoeqv(p)$ for some $p:A=B$.
  Then by path induction, we may assume $p$ is $\refl{A}$, in which case $f$ is $\idfunc[A]$.
  Thus we are reduced to proving $\eqv{\qinv(\idfunc[A])}{(\prd{x:A}(x=x))}$.
  Now by definition we have
  \[ \qinv(\idfunc[A]) \jdeq
  \sm{g:A\to A} \big((g \htpy \idfunc[A]) \times (g \htpy \idfunc[A])\big).
  \]
  By function extensionality, this is equivalent to
  \[ \sm{g:A\to A} \big((g = \idfunc[A]) \times (g = \idfunc[A])\big).
  \]
  And by \cref{ex:sigma-assoc}, this is equivalent to
  \[ \sm{h:\sm{g:A\to A} (g = \idfunc[A])} (\proj1(h) = \idfunc[A])
  \]
  However, by \cref{thm:contr-paths}, $\sm{g:A\to A} (g = \idfunc[A])$ is contractible with center $(\idfunc[A],\refl{\idfunc[A]})$; therefore by \cref{thm:omit-contr} this type is equivalent to $\idfunc[A] = \idfunc[A]$.
  And by function extensionality, $\idfunc[A] = \idfunc[A]$ is equivalent to $\prd{x:A} x=x$.
\end{proof}

\noindent
We remark that \cref{ex:qinv-autohtpy-no-univalence} asks for a proof of the above lemma which avoids univalence.

Thus, what we need is some $A$ which admits a nontrivial element of $\prd{x:A}(x=x)$.
Thinking of $A$ as a higher groupoid, an inhabitant of $\prd{x:A}(x=x)$ is a natural transformation\index{natural!transformation} from the identity functor of $A$ to itself.
Such transformations are said to form the \define{center of a category},
\index{center!of a category}%
\index{category!center of}%
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.

\begin{lem}\label{lem:autohtpy}
  Suppose we have a type $A$ with $a:A$ and $q:a=a$ such that
  \begin{enumerate}
  \item The type $a=a$ is a set.\label{item:autohtpy1}
  \item For all $x:A$ we have $\brck{a=x}$.\label{item:autohtpy2}
  \item For all $p:a=a$ we have $p\ct q = q \ct p$.\label{item:autohtpy3}
  \end{enumerate}
  Then there exists $f:\prd{x:A} (x=x)$ with $f(a)=q$.
\end{lem}
\begin{proof}
  Let $g:\prd{x:A} \brck{a=x}$ be as given by~\ref{item:autohtpy2}.  First we
  observe that each type $\id[A]xy$ 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)=\bproj
  p$ and $g(y)=\bproj{p'}$ for $p:a=x$ and $p':a=y$.  In this case, composing with
  $p$ and $\opp{p'}$ yields an equivalence $\eqv{(x=y)}{(a=a)}$.  But $(a=a)$ is
  a set by~\ref{item:autohtpy1}, so $(x=y)$ is also a set.

  Now, we would like to define $f$ by assigning to each $x$ the path $\opp{g(x)}
  \ct q \ct g(x)$, but this does not work because $g(x)$ does not inhabit $a=x$
  but rather $\brck{a=x}$, 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 \cref{sec:unique-choice}: we characterize
  uniquely the object we wish to construct.  Let us define, for each $x:A$, the
  type
  \[ B(x) \defeq \sm{r:x=x} \prd{s:a=x} (r = \opp s \ct q\ct 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) = \bproj p$ for some $p:a=x$.
  Now suppose given $(r,h)$ and $(r',h')$ in $B(x)$; then we have
  \[ h(p) \ct \opp{h'(p)} : r = r'. \]
  It remains to show that $h$ is identified with $h'$ when transported along this equality, which by transport in identity types and function types (\cref{sec:compute-paths,sec:compute-pi}), reduces to showing
  \[ h(s) = h(p) \ct \opp{h'(p)} \ct h'(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 $\prd{x:A} B(x)$.
  Given $x:A$, we may now invoke the induction principle of propositional truncation to assume that $g(x) = \bproj p$ for $p:a=x$.
  We define $r \defeq \opp p \ct q \ct p$; to inhabit $B(x)$ it remains to show that for any $s:a=x$ we have
  $r = \opp s \ct q \ct s$.
  Manipulating paths, this reduces to showing that $q\ct (p\ct \opp s) = (p\ct \opp s) \ct q$.
  But this is just an instance of~\ref{item:autohtpy3}.
\end{proof}

\begin{thm}\label{thm:qinv-notprop}
  There exist types $A$ and $B$ and a function $f:A\to B$ such that $\qinv(f)$ is not a mere proposition.
\end{thm}
\begin{proof}
  It suffices to exhibit a type $X$ such that $\prd{x:X} (x=x)$ is not a mere proposition.
  Define $X\defeq \sm{A:\type} \brck{\bool=A}$, as in the proof of \cref{thm:no-higher-ac}.
  It will suffice to exhibit an $f:\prd{x:X} (x=x)$ which is unequal to $\lam{x} \refl{x}$.

  Let $a \defeq (\bool,\bproj{\refl{\bool}}) : X$, and let $q:a=a$ be the path corresponding to the nonidentity equivalence $e:\eqv\bool\bool$ defined by $e(\bfalse)\defeq\btrue$ and $e(\btrue)\defeq\bfalse$.
  We would like to apply \cref{lem:autohtpy} to build an $f$.
  By definition of $X$, equalities in subset types (\cref{subsec:prop-subsets}), and univalence, we have $\eqv{(a=a)}{(\eqv{\bool}{\bool})}$, which is a set, so~\ref{item:autohtpy1} holds.
  Similarly, by definition of $X$ and equalities in subset types we have~\ref{item:autohtpy2}.
  Finally, \cref{ex:eqvboolbool} implies that every equivalence $\eqv\bool\bool$ is equal to either $\idfunc[\bool]$ or $e$, so we can show~\ref{item:autohtpy3} by a four-way case analysis.

  Thus, we have $f:\prd{x:X} (x=x)$ such that $f(a) = q$.
  Since $e$ is not equal to $\idfunc[\bool]$, $q$ is not equal to $\refl{a}$, and thus $f$ is not equal to $\lam{x} \refl{x}$.
  Therefore, $\prd{x:X} (x=x)$ is not a mere proposition.
\end{proof}

More generally, \cref{lem:autohtpy} implies that any ``Eilenberg--Mac Lane space'' $K(G,1)$, where $G$ is a nontrivial abelian\index{group!abelian} group, will provide a counterexample; see \cref{cha:homotopy}.
The type $X$ we used turns out to be equivalent to $K(\mathbb{Z}_2,1)$.
In \cref{cha:hits} we will see that the circle $\Sn^1 = K(\mathbb{Z},1)$ is another easy-to-describe example.

We now move on to describing better notions of equivalence.

\index{quasi-inverse|)}%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Half adjoint equivalences}
\label{sec:hae}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\index{equivalence!half adjoint|(defstyle}%
\index{half adjoint equivalence|(defstyle}%
\index{adjoint!equivalence!of types, half|(defstyle}%

In \cref{sec:quasi-inverses} we concluded that $\qinv(f)$ is equivalent to $\prd{x:A} (x=x)$ by discarding a contractible type.
Roughly, the type $\qinv(f)$ contains three data $g$, $\eta$, and $\epsilon$, of which two ($g$ and $\eta$) could together be seen to be contractible when $f$ is an equivalence.
The problem is that removing these data left one remaining ($\epsilon$).
In order to solve this problem, the idea is to add one \emph{additional} datum which, together with $\epsilon$, forms a contractible type.

\begin{defn}\label{defn:ishae}
  A function $f:A\to B$ is a \define{half adjoint equivalence}
  if there are $g:B\to A$ and homotopies $\eta: g \circ f \htpy \idfunc[A]$ and $\epsilon:f \circ g \htpy \idfunc[B]$ such that there exists a homotopy
  \[\tau : \prd{x:A} \map{f}{\eta x} = \epsilon(fx).\]
\end{defn}

Thus we have a type $\ishae(f)$, defined to be
\begin{equation*}
  \sm{g:B\to A}{\eta: g \circ f \htpy \idfunc[A]}{\epsilon:f \circ g \htpy \idfunc[B]} \prd{x:A} \map{f}{\eta x} = \epsilon(fx).
\end{equation*}
Note that in the above definition, the coherence\index{coherence} condition relating $\eta$ and $\epsilon$ only involves $f$.
We might consider instead an analogous coherence condition involving $g$:
\[\upsilon : \prd{y:B} \map{g}{\epsilon y} = \eta(gy)\]
and a resulting analogous definition $\ishae'(f)$.

Fortunately, it turns out each of the conditions implies the other one:

\begin{lem}\label{lem:coh-equiv}
For functions $f : A \to B$ and $g:B\to A$ and homotopies $\eta: g \circ f \htpy \idfunc[A]$ and $\epsilon:f \circ g \htpy \idfunc[B]$, the following conditions are logically equivalent:
\begin{itemize}
\item $\prd{x:A} \map{f}{\eta x} = \epsilon(fx)$
\item $\prd{y:B} \map{g}{\epsilon y} = \eta(gy)$
\end{itemize}
\end{lem}
\begin{proof}
  It suffices to show one direction; the other one is obtained by replacing $A$, $f$, and $\eta$ by $B$, $g$, and $\epsilon$ respectively.
  Let $\tau : \prd{x:A}\;\map{f}{\eta x} = \epsilon(fx)$.
  Fix $y : B$.
  Using naturality of $\epsilon$ and applying $g$, we get the following commuting diagram of paths:
\[\uppercurveobject{{ }}\lowercurveobject{{ }}\twocellhead{{ }}
  \xymatrix@C=3pc{gfgfgy \ar@{=}^-{gfg(\epsilon y)}[r] \ar@{=}_{g(\epsilon (fgy))}[d] & gfgy \ar@{=}^{g(\epsilon y)}[d] \\ gfgy \ar@{=}_{g(\epsilon y)}[r] & gy
  }\]
Using $\tau(gy)$ on the left side of the diagram gives us
\[\uppercurveobject{{ }}\lowercurveobject{{ }}\twocellhead{{ }}
  \xymatrix@C=3pc{gfgfgy \ar@{=}^-{gfg(\epsilon y)}[r] \ar@{=}_{gf(\eta (gy))}[d] & gfgy \ar@{=}^{g(\epsilon y)}[d] \\ gfgy \ar@{=}_{g(\epsilon y)}[r] & gy
  }\]
Using the commutativity of $\eta$ with $g \circ f$ (\cref{cor:hom-fg}), we have
\[\uppercurveobject{{ }}\lowercurveobject{{ }}\twocellhead{{ }}
  \xymatrix@C=3pc{gfgfgy \ar@{=}^-{gfg(\epsilon y)}[r] \ar@{=}_{\eta (gfgy)}[d] & gfgy \ar@{=}^{g(\epsilon y)}[d] \\ gfgy \ar@{=}_{g(\epsilon y)}[r] & gy
  }\]
However, by naturality of $\eta$ we also have
\[\uppercurveobject{{ }}\lowercurveobject{{ }}\twocellhead{{ }}
  \xymatrix@C=3pc{gfgfgy \ar@{=}^-{gfg(\epsilon y)}[r] \ar@{=}_{\eta (gfgy)}[d] & gfgy \ar@{=}^{\eta(gy)}[d] \\ gfgy \ar@{=}_{g(\epsilon y)}[r] & gy
  }\]
Thus, canceling all but the right-hand homotopy, we have $g(\epsilon y) = \eta(g y)$ as desired.
\end{proof}

However, it is important that we do not include \emph{both} $\tau$ and $\upsilon$ in the definition of $\ishae (f)$ (whence the name ``\emph{half} adjoint equivalence'').
If we did, then after canceling contractible types we would still have one remaining datum --- unless we added another higher coherence condition.
In general, we expect to get a well-behaved type if we cut off after an odd number of coherences.

Of course, it is obvious that $\ishae(f) \to\qinv(f)$: simply forget the coherence datum.
The other direction is a version of a standard argument from homotopy theory and category theory.

\begin{thm}\label{thm:equiv-iso-adj}
  For any $f:A\to B$ we have $\qinv(f)\to\ishae(f)$.
\end{thm}
\begin{proof}
Suppose that $(g,\eta,\epsilon)$ is a quasi-inverse for $f$. We have to provide
a quadruple $(g',\eta',\epsilon',\tau)$ witnessing that $f$ is a half adjoint equivalence. To
define $g'$ and $\eta'$, we can just make the obvious choice by setting $g'
\defeq g$ and $\eta'\defeq \eta$. However, in the definition of $\epsilon'$ we
need start worrying about the construction of $\tau$, so we cannot just follow our nose
and take $\epsilon'$ to be $\epsilon$. Instead, we take
\begin{equation*}
\epsilon'(b) \defeq \opp{\epsilon(f(g(b)))}\ct (\ap{f}{\eta(g(b))}\ct \epsilon(b)).
\end{equation*}
Now we need to find
\begin{equation*}
\tau(a): \ap{f}{\eta(a)}=\opp{\epsilon(f(g(f(a))))}\ct (\ap{f}{\eta(g(f(a)))}\ct \epsilon(f(a))).
\end{equation*}
Note first that by \cref{cor:hom-fg}, we have
%$\eta(g(f(a)))\ct\eta(a)=\ap{g}{\ap{f}{\eta(a)}}\ct\eta(a)$ and hence it follows that
$\eta(g(f(a)))=\ap{g}{\ap{f}{\eta(a)}}$. Therefore, we can apply
\cref{lem:htpy-natural} to compute
\begin{align*}
\ap{f}{\eta(g(f(a)))}\ct \epsilon(f(a))
& = \ap{f}{\ap{g}{\ap{f}{\eta(a)}}}\ct \epsilon(f(a))\\
& = \epsilon(f(g(f(a))))\ct \ap{f}{\eta(a)}
\end{align*}
from which we get the desired path $\tau(a)$.
\end{proof}

Combining this with \cref{lem:coh-equiv} (or symmetrizing the proof), we also have $\qinv(f)\to\ishae'(f)$.

It remains to show that $\ishae(f)$ is a mere proposition.
For this, we will need to know that the fibers of an equivalence are contractible.

\begin{defn}\label{defn:homotopy-fiber}
  The \define{fiber}
  \indexdef{fiber}%
  \indexsee{function!fiber of}{fiber}%
  of a map $f:A\to B$ over a point $y:B$ is
  \[ \hfib f y \defeq \sm{x:A} (f(x) = y).\]
\end{defn}

In homotopy theory, this is what would be called the \emph{homotopy fiber} of $f$.
The path lemmas in \cref{sec:computational} yield the following characterization of paths in fibers:

\begin{lem}\label{lem:hfib}
  For any $f : A \to B$, $y : B$, and $(x,p),(x',p') : \hfib{f}{y}$, we have
  \[ \big((x,p) = (x',p')\big) \eqvsym \Parens{\sm{\gamma : x = x'} f(\gamma) \ct p' = p} \qedhere\]
\end{lem}

\begin{thm}\label{thm:contr-hae}
  If $f:A\to B$ is a half adjoint equivalence, then for any $y:B$ the fiber $\hfib f y$ is contractible.
\end{thm}
\begin{proof}
  Let $(g,\eta,\epsilon,\tau) : \ishae(f)$, and fix $y : B$.
  As our center of contraction for $\hfib{f}{y}$ we choose $(gy, \epsilon y)$.
  Now take any $(x,p) : \hfib{f}{y}$; we want to construct a path from $(gy, \epsilon y)$ to $(x,p)$.
  By \cref{lem:hfib}, it suffices to give a path $\gamma : \id{gy}{x}$ such that $\ap f\gamma \ct p = \epsilon y$.
  We put $\gamma \defeq \opp{g(p)} \ct \eta x$.
  Then we have
  \begin{align*}
    f(\gamma) \ct p & = \opp{fg(p)} \ct f (\eta x) \ct p \\
    & = \opp{fg(p)} \ct \epsilon(fx) \ct p \\
    & = \epsilon y
  \end{align*}
  where the second equality follows by $\tau x$ and the third equality is naturality of $\epsilon$.
\end{proof}

We now define the types which encapsulate contractible pairs of data.
The following types put together the quasi-inverse $g$ with one of the homotopies.

\begin{defn}\label{defn:linv-rinv}
  Given a function $f:A\to B$, we define the types
    \begin{align*}
      \linv(f) &\defeq \sm{g:B\to A} (g\circ f\htpy \idfunc[A])\\
      \rinv(f) &\defeq \sm{g:B\to A} (f\circ g\htpy \idfunc[B])
    \end{align*}
  of \define{left inverses}
  \indexdef{left!inverse}%
  \indexdef{inverse!left}%
  and \define{right inverses}
  \indexdef{right!inverse}%
  \indexdef{inverse!right}%
  to $f$, respectively.
  We call $f$ \define{left invertible}
  \indexdef{function!left invertible}%
  \indexdef{function!right invertible}%
  if $\linv(f)$ is inhabited, and similarly \define{right invertible}
  \indexdef{left!invertible function}%
  \indexdef{right!invertible function}%
  if $\rinv(f)$ is inhabited.
\end{defn}

\begin{lem}\label{thm:equiv-compose-equiv}
  If $f:A\to B$ has a quasi-inverse, then so do
  \begin{align*}
    (f\circ \blank) &: (C\to A) \to (C\to B)\\
    (\blank\circ f) &: (B\to C) \to (A\to C).
  \end{align*}
\end{lem}
\begin{proof}
  If $g$ is a quasi-inverse of $f$, then $(g\circ \blank)$ and $(\blank\circ g)$ are quasi-inverses of $(f\circ \blank)$ and $(\blank\circ f)$ respectively.
\end{proof}

\begin{lem}\label{lem:inv-hprop}
  If $f : A \to B$ has a quasi-inverse, then the types $\rinv(f)$ and $\linv(f)$ are contractible.
\end{lem}
\begin{proof}
  By function extensionality, we have
  \[\eqv{\linv(f)}{\sm{g:B\to A} (g\circ f = \idfunc[A])}.\]
  But this is the fiber of $(\blank\circ f)$ over $\idfunc[A]$, and so
  by \cref{thm:equiv-compose-equiv,thm:equiv-iso-adj,thm:contr-hae}, it is contractible.
  Similarly, $\rinv(f)$ is equivalent to the fiber of $(f\circ \blank)$ over $\idfunc[B]$ and hence contractible.
\end{proof}

Next we define the types which put together the other homotopy with the additional coherence datum.\index{coherence}%

\begin{defn}\label{defn:lcoh-rcoh}
For $f : A \to B$, a left inverse $(g,\eta) : \linv(f)$, and a right inverse $(g,\epsilon) : \rinv(f)$, we denote
\begin{align*}
\lcoh{f}{g}{\eta} & \defeq \sm{\epsilon : f\circ g \htpy \idfunc[B]} \prd{y:B} g(\epsilon y) = \eta (gy), \\
\rcoh{f}{g}{\epsilon} & \defeq \sm{\eta : g\circ f \htpy \idfunc[A]} \prd{x:A} f(\eta x) = \epsilon (fx).
\end{align*}
\end{defn}

\begin{lem}\label{lem:coh-hfib}
For any $f,g,\epsilon,\eta$, we have
\begin{align*}
\lcoh{f}{g}{\eta} & \eqvsym {\prd{y:B} \id[\hfib{g}{gy}]{(fgy,\eta(gy))}{(y,\refl{gy})}}, \\
\rcoh{f}{g}{\epsilon} & \eqvsym {\prd{x:A} \id[\hfib{f}{fx}]{(gfx,\epsilon(fx))}{(x,\refl{fx})}}.
\end{align*}
\end{lem}
\begin{proof}
Using \cref{lem:hfib}.
\end{proof}

\begin{lem}\label{lem:coh-hprop}
  If $f$ is a half adjoint equivalence, then for any $(g,\epsilon) : \rinv(f)$, the type $\rcoh{f}{g}{\epsilon}$ is contractible.
\end{lem}
\begin{proof}
  By \cref{lem:coh-hfib} and the fact that dependent function types preserve contractible spaces, it suffices to show that for each $x:A$, the type $\id[\hfib{f}{fx}]{(gfx,\epsilon(fx))}{(x,\refl{fx})}$ is contractible.
  But by \cref{thm:contr-hae}, $\hfib{f}{fx}$ is contractible, and any path space of a contractible space is itself contractible.
\end{proof}

\begin{thm}\label{thm:hae-hprop}
  For any $f : A \to B$, the type $\ishae(f)$ is a mere proposition.
\end{thm}
\begin{proof}
  By \cref{ex:prop-inhabcontr} it suffices to assume $f$ to be a half adjoint equivalence and show that $\ishae(f)$ is contractible.
  Now by associativity of $\Sigma$ (\cref{ex:sigma-assoc}), the type $\ishae(f)$ is equivalent to
  \[\sm{u : \rinv(f)} \rcoh{f}{\proj{1}(u)}{\proj{2}(u)}.\]
  But by \cref{lem:inv-hprop,lem:coh-hprop} and the fact that $\Sigma$ preserves contractibility, the latter type is also contractible.
\end{proof}

Thus, we have shown that $\ishae(f)$ has all three desiderata for the type $\isequiv(f)$.
In the next two sections we consider a couple of other possibilities.

\index{equivalence!half adjoint|)}%
\index{half adjoint equivalence|)}%
\index{adjoint!equivalence!of types, half|)}%

\section{Bi-invertible maps}
\label{sec:biinv}

\index{function!bi-invertible|(defstyle}%
\index{bi-invertible function|(defstyle}%
\index{equivalence!as bi-invertible function|(defstyle}%

Using the language introduced in \cref{sec:hae}, we can restate the definition proposed in \cref{sec:basics-equivalences} as follows.

\begin{defn}\label{defn:biinv}
  We say $f:A\to B$ is \define{bi-invertible}
  if it has both a left inverse and a right inverse:
  \[ \biinv (f) \defeq \linv(f) \times \rinv(f). \]
\end{defn}

In \cref{sec:basics-equivalences} we proved that $\qinv(f)\to\biinv(f)$ and $\biinv(f)\to\qinv(f)$.
What remains is the following.

\begin{thm}\label{thm:isprop-biinv}
  For any $f:A\to B$, the type $\biinv(f)$ is a mere proposition.
\end{thm}
\begin{proof}
  We may suppose $f$ to be bi-invertible and show that $\biinv(f)$ is contractible.
  But since $\biinv(f)\to\qinv(f)$, by \cref{lem:inv-hprop} in this case both $\linv(f)$ and $\rinv(f)$ are contractible, and the product of contractible types is contractible.
\end{proof}

Note that this also fits the proposal made at the beginning of \cref{sec:hae}: we combine $g$ and $\eta$ into a contractible type and add an additional datum which combines with $\epsilon$ into a contractible type.
The difference is that instead of adding a \emph{higher} datum (a 2-dimensional path) to combine with $\epsilon$, we add a \emph{lower} one (a right inverse that is separate from the left inverse).

\begin{cor}\label{thm:equiv-biinv-isequiv}
  For any $f:A\to B$ we have $\eqv{\biinv(f)}{\ishae(f)}$.
\end{cor}
\begin{proof}
  We have $\biinv(f) \to \qinv(f) \to \ishae(f)$ and $\ishae(f) \to \qinv(f) \to \biinv(f)$.
  Since both $\ishae(f)$ and $\biinv(f)$ are mere propositions, the equivalence follows from \cref{lem:equiv-iff-hprop}.
\end{proof}

\index{function!bi-invertible|)}%
\index{bi-invertible function|)}%
\index{equivalence!as bi-invertible function|)}%

\section{Contractible fibers}
\label{sec:contrf}

\index{function!contractible|(defstyle}%
\index{contractible!function|(defstyle}%
\index{equivalence!as contractible function|(defstyle}%

Note that our proofs about $\ishae(f)$ and $\biinv(f)$ made essential use of the fact that the fibers of an equivalence are contractible.
In fact, it turns out that this property is itself a sufficient definition of equivalence.

\begin{defn}[Contractible maps] \label{defn:equivalence}
  A map $f:A\to B$ is \define{contractible}
  if for all $y:B$, the fiber $\hfib f y$ is contractible.
\end{defn}

Thus, the type $\iscontr(f)$ is defined to be
\begin{align}
  \iscontr(f) &\defeq \prd{y:B} \iscontr(\hfib f y)\label{eq:iscontrf}
  % \\
  % &\defeq \prd{y:B} \iscontr (\setof{x:A | f(x) = y}).
\end{align}
Note that in \cref{sec:contractibility} we defined what it means for a \emph{type} to be contractible.
Here we are defining what it means for a \emph{map} to be contractible.
Our terminology follows the general homotopy-theoretic practice of saying that a map has a certain property if all of its (homotopy) fibers have that property.
Thus, a type $A$ is contractible just when the map $A\to\unit$ is contractible.
From \cref{cha:hlevels} onwards we will also call contractible maps and types \emph{$(-2)$-truncated}.

We have already shown in \cref{thm:contr-hae} that $\ishae(f) \to \iscontr(f)$.
Conversely:

\begin{thm}\label{thm:lequiv-contr-hae}
For any $f:A\to B$ we have ${\iscontr(f)} \to {\ishae(f)}$.
\end{thm}
\begin{proof}
Let $P : \iscontr(f)$. We define an inverse mapping $g : B \to A$ by sending each $y : B$ to the center of contraction of the fiber at $y$:
\[ g(y) \defeq \proj{1}(\proj{1}(Py)). \]
We can thus define the homotopy $\epsilon$ by mapping $y$ to the witness that $g(y)$ indeed belongs to the fiber at $y$:
\[ \epsilon(y) \defeq \proj{2}(\proj{1}(P y)). \]
It remains to define $\eta$ and $\tau$. This of course amounts to giving an element of $\rcoh{f}{g}{\epsilon}$. By \cref{lem:coh-hfib}, this is the same as giving for each $x:A$ a path from $(gfx,\epsilon(fx))$ to $(x,\refl{fx})$ in the fiber of $f$ over $fx$. But this is easy: for any $x : A$, the type $\hfib{f}{fx}$
is contractible by assumption, hence such a path must exist. We can construct it explicitly as
\[\opp{\big(\proj{2}(P(fx))(gfx,\epsilon(fx))\big)} \ct \big(\proj{2}(P(fx)) (x,\refl{fx})\big). \qedhere \]
\end{proof}

It is also easy to see:

\begin{lem}\label{thm:contr-hprop}
  For any $f$, the type $\iscontr(f)$ is a mere proposition.
\end{lem}
\begin{proof}
  By \cref{thm:isprop-iscontr}, each type $\iscontr (\hfib f y)$ is a mere proposition.
  Thus, by \cref{thm:isprop-forall}, so is~\eqref{eq:iscontrf}.
\end{proof}

\begin{thm}\label{thm:equiv-contr-hae}
  For any $f:A\to B$ we have $\eqv{\iscontr(f)}{\ishae(f)}$.
\end{thm}
\begin{proof}
  We have already established a logical equivalence ${\iscontr(f)} \Leftrightarrow {\ishae(f)}$, and both are mere propositions (\cref{thm:contr-hprop,thm:hae-hprop}).
  Thus, \cref{lem:equiv-iff-hprop} applies.
\end{proof}

Usually, we prove that a function is an equivalence by exhibiting a quasi-inverse, but sometimes this definition is more convenient.
For instance, it implies that when proving a function to be an equivalence, we are free to assume that its codomain is inhabited.

\begin{cor}\label{thm:equiv-inhabcod}
  If $f:A\to B$ is such that $B\to \isequiv(f)$, then $f$ is an equivalence.
\end{cor}
\begin{proof}
  To show $f$ is an equivalence, it suffices to show that $\hfib f y$ is contractible for any $y:B$.
  But if $e:B\to \isequiv(f)$, then given any such $y$ we have $e(y):\isequiv(f)$, so that $f$ is an equivalence and hence $\hfib f y$ is contractible, as desired.
\end{proof}

\index{function!contractible|)}%
\index{contractible!function|)}%
\index{equivalence!as contractible function|)}%

\section{On the definition of equivalences}
\label{sec:concluding-remarks}

\indexdef{equivalence}
We have shown that all three definitions of equivalence satisfy the three desirable properties and are pairwise equivalent:
\[ \iscontr(f) \eqvsym \ishae(f) \eqvsym \biinv(f). \]
(There are yet more possible definitions of equivalence, but we will stop with these three.
See \cref{ex:brck-qinv} and the exercises in this chapter for some more.)
Thus, we may choose any one of them as ``the'' definition of $\isequiv (f)$.
For definiteness, we choose to define
\[ \isequiv(f) \defeq \ishae(f).\]
\index{mathematics!formalized}%
This choice is advantageous for formalization, since $\ishae(f)$ contains the most directly useful data.
On the other hand, for other purposes, $\biinv(f)$ is often easier to deal with, since it contains no 2-dimensional paths and its two symmetrical halves can be treated independently.
However, for purposes of this book, the specific choice will make little difference.

In the rest of this chapter, we study some other properties and characterizations of equivalences.
\index{equivalence!properties of}%


\section{Surjections and embeddings}
\label{sec:mono-surj}

\index{set}
When $A$ and $B$ are sets and $f:A\to B$ is an equivalence, we also call it as \define{isomorphism}
\indexdef{isomorphism!of sets}%
or a \define{bijection}.
\indexdef{bijection}%
\indexsee{function!bijective}{bijection}%
(We avoid these words for types that are not sets, since in homotopy theory and higher category theory they often denote a stricter notion of ``sameness'' than homotopy equivalence.)
In set theory, a function is a bijection just when it is both injective and surjective.
The same is true in type theory, if we formulate these conditions appropriately.
For clarity, when dealing with types that are not sets, we will speak of \emph{embeddings} instead of injections.

\begin{defn}\label{defn:surj-emb}
  Let $f:A\to B$.
  \begin{enumerate}
  \item We say $f$ is \define{surjective}
    \indexsee{surjective!function}{function, surjective}%
    \indexdef{function!surjective}%
    (or a \define{surjection})
    \indexsee{surjection}{function, surjective}%
    if for every $b:B$ we have $\brck{\hfib f b}$.
  \item We say $f$ is an \define{embedding}
    \indexdef{function!embedding}%
    \indexsee{embedding}{function, embedding}%
    if for every $x,y:A$ the function $\apfunc f : (\id[A]xy) \to (\id[B]{f(x)}{f(y)})$ is an equivalence.
  \end{enumerate}
\end{defn}

In other words, $f$ is surjective if every fiber of $f$ is merely inhabited, or equivalently if for all $b:B$ there merely exists an $a:A$ such that $f(a)=b$.
In traditional logical notation, $f$ is surjective if $\fall{b:B}\exis{a:A} (f(a)=b)$.
This must be distinguished from the stronger assertion that $\prd{b:B}\sm{a:A} (f(a)=b)$; if this holds we say that $f$ is a \define{split surjection}.
\indexsee{split!surjection}{function, split surjective}%
\indexsee{surjection!split}{function, split surjective}%
\indexsee{surjective!function!split}{function, split surjective}%
\indexdef{function!split surjective}%
(Since this latter type is equivalent to $\sm{g:B\to A}\prd{b:B} (f(g(b))=b)$, being a split surjection is the same as being a \emph{retraction} as defined in \cref{sec:contractibility}.)
\index{retraction}%
\index{function!retraction}%

The axiom of choice from \cref{sec:axiom-choice} says exactly that every surjection \emph{between sets} is split.
However, in the presence of the univalence axiom, it is simply false that \emph{all} surjections are split.
In \cref{thm:no-higher-ac} we constructed a type family $Y:X\to \type$ such that $\prd{x:X} \brck{Y(x)}$ but $\neg \prd{x:X} Y(x)$;
for any such family, the first projection $(\sm{x:X} Y(x)) \to X$ is a surjection that is not split.

If $A$ and $B$ are sets, then by \cref{lem:equiv-iff-hprop}, $f$ is an embedding just when
\begin{equation}
  \prd{x,y:A} (\id[B]{f(x)}{f(y)}) \to (\id[A]xy).\label{eq:injective}
\end{equation}
In this case we say that $f$ is \define{injective},
\indexsee{injective function}{function, injective}%
\indexdef{function!injective}%
or an \define{injection}.
\indexsee{injection}{function, injective}%
We avoid these word for types that are not sets, because they might be interpreted as~\eqref{eq:injective}, which is an ill-behaved notion for non-sets.
It is also true that any function between sets is surjective if and only if it is an \emph{epimorphism} in a suitable sense, but this also fails for more general types, and surjectivity is generally the more important notion.

\begin{thm}\label{thm:mono-surj-equiv}
  A function $f:A\to B$ is an equivalence if and only if it is both surjective and an embedding.
\end{thm}
\begin{proof}
  If $f$ is an equivalence, then each $\hfib f b$ is contractible, hence so is $\brck{\hfib f b}$, so $f$ is surjective.
  And we showed in \cref{thm:paths-respects-equiv} that any equivalence is an embedding.

  Conversely, suppose $f$ is a surjective embedding.
  Let $b:B$; we show that $\sm{x:A}(f(x)=b)$ is contractible.
  Since $f$ is surjective, there merely exists an $a:A$ such that $f(a)=b$.
  Thus, the fiber of $f$ over $b$ is inhabited; it remains to show it is a mere proposition.
  For this, suppose given $x,y:A$ with $p:f(x)=b$ and $q:f(y)=b$.
  Then since $\apfunc f$ is an equivalence, there exists $r:x=y$ with $\apfunc f (r) = p \ct \opp q$.
  However, using the characterization of paths in $\Sigma$-types, the latter equality rearranges to $\trans{r}{p} = q$.
  Thus, together with $r$ it exhibits $(x,p) = (y,q)$ in the fiber of $f$ over $b$.
\end{proof}

\begin{cor}
  For any $f:A\to B$ we have
  \[ \isequiv(f) \eqvsym (\mathsf{isEmbedding}(f) \times \mathsf{isSurjective}(f)).\]
\end{cor}
\begin{proof}
  Being a surjection and an embedding are both mere propositions; now apply \cref{lem:equiv-iff-hprop}.
\end{proof}

Of course, this cannot be used as a definition of ``equivalence'', since the definition of embeddings refers to equivalences.
However, this characterization can still be useful; see \cref{sec:whitehead}.
We will generalize it in \cref{cha:hlevels}.


% \section{Fiberwise equivalences}
\section{Closure properties of equivalences}
\label{sec:equiv-closures}
\label{sec:fiberwise-equivalences}
\index{equivalence!properties of}%


% We end this chapter by observing some important closure properties of equivalences.
We have already seen in \cref{thm:equiv-eqrel} that equivalences are closed under composition.
Furthermore, we have:

\begin{thm}[The 2-out-of-3 property]\label{thm:two-out-of-three}
  \index{2-out-of-3 property}%
  Suppose $f:A\to B$ and $g:B\to C$.
  If any two of $f$, $g$, and $g\circ f$ are equivalences, so is the third.
\end{thm}
\begin{proof}
  If $g\circ f$ and $g$ are equivalences, then $\opp{(g\circ f)} \circ g$ is a quasi-inverse to $f$.
  On the one hand, we have $\opp{(g\circ f)} \circ g \circ f \htpy \idfunc[A]$, while on the other we have
  \begin{align*}
    f \circ \opp{(g\circ f)} \circ g
    &\htpy \opp g \circ g \circ f \circ \opp{(g\circ f)} \circ g\\
    &\htpy \opp g \circ g\\
    &\htpy \idfunc[B].
  \end{align*}
  Similarly, if $g\circ f$ and $f$ are equivalences, then $f\circ \opp{(g\circ f)}$ is a quasi-inverse to $g$.
\end{proof}

This is a standard closure condition on equivalences from homotopy theory.
Also well-known is that they are closed under retracts, in the following sense.

\index{retract!of a function|(defstyle}%

\begin{defn}\label{defn:retract}
A function $g:A\to B$ is said to be a \define{retract}
of a function $f:X\to Y$ if there is a diagram
\begin{equation*}
  \xymatrix{
    {A} \ar[r]^{s} \ar[d]_{g}
    &
    {X} \ar[r]^{r} \ar[d]_{f}
    &
    {A} \ar[d]^{g}
    \\
    {B} \ar[r]_{s'}
    &
    {Y} \ar[r]_{r'}
    &
    {B}
  }
\end{equation*}
for which there are
\begin{enumerate}
\item a homotopy $R:r\circ s \htpy \idfunc[A]$.
\item a homotopy $R':r'\circ s' \htpy\idfunc[B]$.
\item a homotopy $L:f\circ s\htpy s'\circ g$.
\item a homotopy $K:g\circ r\htpy r'\circ f$.
\item for every $a:A$, a path $H(a)$ witnessing the commutativity of the square
\begin{equation*}
  \xymatrix@C=3pc{
    {g(r(s(a)))} \ar@{=}[r]^-{K(s(a))} \ar@{=}[d]_{\ap g{R(a)}}
    &
    {r'(f(s(a)))} \ar@{=}[d]^{\ap{r'}{L(a)}}
    \\
    {g(a)} \ar@{=}[r]_-{\opp{R'(g(a))}}
    &
    {r'(s'(g(a)))}
  }
\end{equation*}
\end{enumerate}
\end{defn}

Recall that in \cref{sec:contractibility} we defined what it means for a type to be a retract of another.
This is a special case of the above definition where $B$ and $Y$ are $\unit$.
Conversely, just as with contractibility, retractions of maps induce retractions of their fibers.

\begin{lem}\label{lem:func_retract_to_fiber_retract}
If a function $g:A\to B$ is a retract of a function $f:X\to Y$, then $\hfib{g}b$ is a retract of $\hfib{f}{s'(b)}$
for every $b:B$, where $s':B\to Y$ is as in \cref{defn:retract}.
\end{lem}

\begin{proof}
Suppose that $g:A\to B$ is a retract of $f:X\to Y$. Then for any $b:B$ we have the functions
\begin{align*}
\varphi_b &:\hfiber{g}b\to\hfib{f}{s'(b)}, &
\varphi_b(a,p) & \defeq \pairr{s(a),L(a)\ct s'(p)},\\
\psi_b &:\hfib{f}{s'(b)}\to\hfib{g}b, &
\psi_b(x,q) &\defeq \pairr{r(x),K(x)\ct r'(q)\ct R'(b)}.
\end{align*}
Then we have $\psi_b(\varphi_b({a,p}))\equiv\pairr{r(s(a)),K(s(a))\ct r'(L(a)\ct s'(p))\ct R'(b)}$.
We claim $\psi_b$ is a retraction with section $\varphi_b$ for all $b:B$, which is to say that for all $(a,p):\hfib g b$ we have $\psi_b(\varphi_b({a,p}))= \pairr{a,p}$.
In other words, we want to show
\begin{equation*}
\prd{b:B}{a:A}{p:g(a)=b} \psi_b(\varphi_b({a,p}))= \pairr{a,p}.
\end{equation*}
By reordering the first two $\Pi$s and applying a version of \cref{thm:omit-contr}, this is equivalent to
\begin{equation*}
\prd{a:A}\psi_{g(a)}(\varphi_{g(a)}({a,\refl{g(a)}}))=\pairr{a,\refl{g(a)}}.
\end{equation*}
For any $a$, by \cref{thm:path-sigma}, this equality of pairs is equivalent to a pair of equalities. The first components are equal by $R(a):r(s(a))= a$, so we need only show
\begin{equation*}
\trans{R(a)}{K(s(a))\ct r'(L(a))\ct R'(g(a))} = \refl{g(a)}.
\end{equation*}
But this transportation computes as $\opp{g(R(a))}\ct K(s(a))\ct r'(L(a))\ct R'(g(a))$, so the required path is given by $H(a)$.
\end{proof}

\begin{thm}\label{thm:retract-equiv}
  If $g$ is a retract of an equivalence $f$, then $g$ is also an equivalence.
\end{thm}
\begin{proof}
  By \cref{lem:func_retract_to_fiber_retract}, every fiber of $g$ is a retract of a fiber of $f$.
  Thus, by \cref{thm:retract-contr}, if the latter are all contractible, so are the former.
\end{proof}

\index{retract!of a function|)}%

\index{fibration}%
\index{total!space}%
Finally, we show that fiberwise equivalences can be characterized in terms of equivalences of total spaces.
To explain the terminology, recall from \cref{sec:fibrations} that a type family $P:A\to\type$ can be viewed as a fibration over $A$ with total space $\sm{x:A} P(x)$, the fibration being the projection $\proj1:\sm{x:A} P(x) \to A$.
From this point of view, given two type families $P,Q:A\to\type$, we may refer to a function $f:\prd{x:A} (P(x)\to Q(x))$ as a \define{fiberwise map} or a \define{fiberwise transformation}.
\indexsee{transformation!fiberwise}{fiberwise transformation}%
\indexsee{function!fiberwise}{fiberwise transformation}%
\index{fiberwise!transformation|(defstyle}%
\indexsee{fiberwise!map}{fiberwise transformation}%
\indexsee{map!fiberwise}{fiberwise transformation}
Such a map induces a function on total spaces:

\begin{defn}\label{defn:total-map}
  Given type families $P,Q:A\to\type$ and a map $f:\prd{x:A} P(x)\to Q(x)$, we define
  \begin{equation*}
    \total f  \defeq \lam{w}\pairr{\proj{1}w,f(\proj{1}w,\proj{2}w)} : \sm{x:A}P(x)\to\sm{x:A}Q(x).
  \end{equation*}
\end{defn}

\begin{thm}\label{fibwise-fiber-total-fiber-equiv}
Suppose that $f$ is a fiberwise transformation between families $P$ and
$Q$ over a type $A$ and let $x:A$ and $v:Q(x)$. Then we have an equivalence
\begin{equation*}
\eqv{\hfib{\total{f}}{\pairr{x,v}}}{\hfib{f(x)}{v}}.
\end{equation*}
\end{thm}
\begin{proof}
  We calculate:
\begin{align}
  \hfib{\total{f}}{\pairr{x,v}}
  & \jdeq \sm{w:\sm{x:A}P(x)}\pairr{\proj{1}w,f(\proj{1}w,\proj{2}w)}=\pairr{x,v}
  \notag \\
  & \eqv{}{} \sm{a:A}{u:P(a)}\pairr{a,f(a,u)}=\pairr{x,v}
  \tag{by~\cref{ex:sigma-assoc}} \\
  & \eqv{}{} \sm{a:A}{u:P(a)}{p:a=x}\trans{p}{f(a,u)}=v
  \tag{by \cref{thm:path-sigma}} \\
  & \eqv{}{} \sm{a:A}{p:a=x}{u:P(a)}\trans{p}{f(a,u)}=v
  \notag \\
  & \eqv{}{} \sm{u:P(x)}f(x,u)=v
  \tag{$*$}\label{eq:uses-sum-over-paths} \\
  & \jdeq \hfib{f(x)}{v}. \notag
\end{align}
The equivalence~\eqref{eq:uses-sum-over-paths} follows from \cref{thm:omit-contr,thm:contr-paths,ex:sigma-assoc}.
\end{proof}

We say that a fiberwise transformation $f:\prd{x:A} P(x)\to Q(x)$ is a \define{fiberwise equivalence}%
\indexdef{fiberwise!equivalence}%
\indexdef{equivalence!fiberwise}
if each $f(x):P(x) \to Q(x)$ is an equivalence.

\begin{thm}\label{thm:total-fiber-equiv}
Suppose that $f$ is a fiberwise transformation between families
$P$ and $Q$ over a type $A$.
Then $f$ is a fiberwise equivalence if and only if $\total{f}$ is an equivalence.
\end{thm}

\begin{proof}
Let $f$, $P$, $Q$ and $A$ be as in the statement of the theorem.
By \cref{fibwise-fiber-total-fiber-equiv} it follows for all
$x:A$ and $v:Q(x)$ that
$\hfib{\total{f}}{\pairr{x,v}}$ is contractible if and only if
$\hfib{f(x)}{v}$ is contractible.
Thus, $\hfib{\total{f}}{w}$ is contractible for all $w:\sm{x:A}Q(x)$ if and only if $\hfib{f(x)}{v}$ is contractible for all $x:A$ and $v:Q(x)$.
\end{proof}

\index{fiberwise!transformation|)}%


\section{The object classifier}
\label{sec:object-classification}

In type theory we have a basic notion of \emph{family of types}, namely a function $B:A\to\type$.
We have seen that such families behave somewhat like \emph{fibrations} in homotopy theory, with the fibration being the projection $\proj1:\sm{a:A} B(a) \to A$.
A basic fact in homotopy theory is that every map is equivalent to a fibration.
With univalence at our disposal, we can prove the same thing in type theory.

\begin{lem}\label{thm:fiber-of-a-fibration}
  For any type family $B:A\to\type$, the fiber of $\proj1:\sm{x:A} B(x) \to A$ over $a:A$ is equivalent to $B(a)$:
  \[ \eqv{\hfib{\proj1}{a}}{B(a)} \]
\end{lem}
\begin{proof}
  We have
  \begin{align*}
    \hfib{\proj1}{a} &\defeq \sm{u:\sm{x:A} B(x)} \proj1(u)=a\\
    &\eqvsym \sm{x:A}{b:B(x)} (x=a)\\
    &\eqvsym \sm{x:A}{p:x=a} B(x)\\
    &\eqvsym B(a)
  \end{align*}
  using the left universal property of identity types.
\end{proof}

\begin{lem}\label{thm:total-space-of-the-fibers}
  For any function $f:A\to B$, we have $\eqv{A}{\sm{b:B}\hfib{f}{b}}$.
\end{lem}
\begin{proof}
  We have
  \begin{align*}
    \sm{b:B}\hfib{f}{b} &\defeq \sm{b:B}{a:A} (f(a)=b)\\
    &\eqvsym \sm{a:A}{b:B} (f(a)=b)\\
    &\eqvsym A
  \end{align*}
  using the fact that $\sm{b:B} (f(a)=b)$ is contractible.
\end{proof}

\begin{thm}\label{thm:nobject-classifier-appetizer}
For any type $B$ there is an equivalence
\begin{equation*}
\chi:\Parens{\sm{A:\type} (A\to B)}\eqvsym (B\to\type).
\end{equation*}
\end{thm}
\begin{proof}
We have to construct quasi-inverses
\begin{align*}
\chi & : \Parens{\sm{A:\type} (A\to B)}\to B\to\type\\
\psi & : (B\to\type)\to\Parens{\sm{A:\type} (A\to B)}.
\end{align*}
We define $\chi$ by $\chi((A,f),b)\defeq\hfiber{f}b$, and $\psi$ by $\psi(P)\defeq\Pairr{(\sm{b:B} P(b)),\proj1}$.
Now we have to verify that $\chi\circ\psi\htpy\idfunc{}$ and that $\psi\circ\chi \htpy\idfunc{}$.
\begin{enumerate}
\item Let $P:B\to\type$.
  By \cref{thm:fiber-of-a-fibration},
$\hfiber{\proj1}{b}\eqvsym P(b)$ for any $b:B$, so it follows immediately
that $P\htpy\chi(\psi(P))$.
\item Let $f:A\to B$ be a function. We have to find a path
\begin{equation*}
\Pairr{\tsm{b:B} \hfiber{f}b,\,\proj1}=\pairr{A,f}.
\end{equation*}
First note that by \cref{thm:total-space-of-the-fibers}, we have
$e:\sm{b:B} \hfiber{f}b\eqvsym A$ with $e(b,a,p)\defeq a$ and $e^{-1}(a)
\defeq(f(a),a,\refl{f(a)})$.
By \cref{thm:path-sigma}, it remains to show $\trans{(\ua(e))}{\proj1} = f$.
But by the computation rule for univalence and~\eqref{eq:transport-arrow}, we have $\trans{(\ua(e))}{\proj1} = \proj1\circ e^{-1}$, and the definition of $e^{-1}$ immediately yields $\proj1 \circ e^{-1} \jdeq f$.\qedhere
\end{enumerate}
\end{proof}

\noindent
\indexdef{object!classifier}%
\indexdef{classifier!object}%
\index{.infinity1-topos@$(\infty,1)$-topos}%
In particular, this implies that we have an \emph{object classifier} in the sense of higher topos theory.
Recall from \cref{def:pointedtype} that $\pointed\type$ denotes the type $\sm{A:\type} A$ of pointed types.

\begin{thm}\label{thm:object-classifier}
Let $f:A\to B$ be a function. Then the diagram
\begin{equation*}
  \vcenter{\xymatrix{
      A\ar[r]^-{\vartheta_f} \ar[d]_{f} &
      \pointed{\type}\ar[d]^{\proj1}\\
      B\ar[r]_{\chi_f} &
      \type
      }}
\end{equation*}
is a pullback\index{pullback} square (see \cref{ex:pullback}).
Here the function $\vartheta_f$ is defined by
\begin{equation*}
 \lam{a} \pairr{\hfiber{f}{f(a)},\pairr{a,\refl{f(a)}}}.
\end{equation*}
\end{thm}
\begin{proof}
Note that we have the equivalences
\begin{align*}
A & \eqvsym \sm{b:B} \hfiber{f}b\\
& \eqvsym \sm{b:B}{X:\type}{p:\hfiber{f}b= X} X\\
& \eqvsym \sm{b:B}{X:\type}{x:X} \hfiber{f}b= X\\
& \eqvsym \sm{b:B}{Y:\pointed{\type}} \hfiber{f}b = \proj1 Y\\
& \jdeq B\times_{\type}\pointed{\type}
\end{align*}
which gives us a composite equivalence $e:A\eqvsym B\times_\type\pointed{\type}$.
We may display the action of this composite equivalence step by step by
\begin{align*}
a & \mapsto \pairr{f(a),\; \pairr{a,\refl{f(a)}}}\\
& \mapsto \pairr{f(a), \; \hfiber{f}{f(a)}, \; \refl{\hfiber{f}{f(a)}}, \; \pairr{a,\refl{f(a)}}}\\
& \mapsto \pairr{f(a), \; \hfiber{f}{f(a)}, \; \pairr{a,\refl{f(a)}}, \; \refl{\hfiber{f}{f(a)}}}.
\end{align*}
Therefore, we get homotopies $f\htpy\proj1\circ e$ and $\vartheta_f\htpy \proj2\circ e$.
\end{proof}



\section{Univalence implies function extensionality}
\label{sec:univalence-implies-funext}

\index{function extensionality!proof from univalence}%
In the last section of this chapter we include a proof that the univalence axiom implies function
extensionality. Thus, in this section we work \emph{without} the function extensionality axiom.
The proof consists of two steps. First we show
in \cref{uatowfe} that the univalence
axiom implies a weak form of function extensionality, defined in \cref{weakfunext} below. The
principle of weak function extensionality in turn implies the usual function extensionality,
and it does so without the univalence axiom (\cref{wfetofe}).

\index{univalence axiom}%
Let $\type$ be a universe; we will explicitly indicate where we assume that it is univalent.

\begin{defn}\label{weakfunext}
The \define{weak function extensionality principle}
\indexdef{function extensionality!weak}%
asserts that there is a function
\begin{equation*}
\Parens{\prd{x:A}\iscontr(P(x))} \to\iscontr\Parens{\prd{x:A}P(x)}
\end{equation*}
for any family $P:A\to\type$ of types over any type $A$.
\end{defn}

The following lemma is easy to prove using function extensionality; the point here is that it also follows from univalence without assuming function extensionality separately.

\begin{lem} \label{UA-eqv-hom-eqv}
Assuming $\type$ is univalent, for any $A,B,X:\type$ and any $e:\eqv{A}{B}$, there is an equivalence
\begin{equation*}
\eqv{(X\to A)}{(X\to B)}
\end{equation*}
of which the underlying map is given by post-composition with the underlying function of $e$.
\end{lem}

\begin{proof}
  % Immediate by induction on $\eqv{}{}$ (see \cref{thm:equiv-induction}).
  As in the proof of \cref{lem:qinv-autohtpy}, we may assume that $e = \idtoeqv(p)$ for some $p:A=B$.
  Then by path induction, we may assume $p$ is $\refl{A}$, so that $e = \idfunc[A]$.
  But in this case, post-composition with $e$ is the identity, hence an equivalence.
\end{proof}

\begin{cor}\label{contrfamtotalpostcompequiv}
Let $P:A\to\type$ be a family of contractible types, i.e.\ \narrowequation{\prd{x:A}\iscontr(P(x)).}
Then the projection $\proj{1}:(\sm{x:A}P(x))\to A$ is an equivalence. Assuming $\type$ is univalent, it follows immediately that post-composition with $\proj{1}$ gives an equivalence
\begin{equation*}
\alpha : \eqv{\Parens{A\to\sm{x:A}P(x)}}{(A\to A)}.
\end{equation*}
\end{cor}

\begin{proof}
  By \cref{thm:fiber-of-a-fibration}, for $\proj{1}:\sm{x:A}P(X)\to A$ and $x:A$ we have an equivalence
  \begin{equation*}
    \eqv{\hfiber{\proj{1}}{x}}{P(x)}.
  \end{equation*}
  Therefore $\proj{1}$ is an equivalence whenever each $P(x)$ is contractible. The assertion is now a consequence of  \cref{UA-eqv-hom-eqv}.
\end{proof}

In particular, the homotopy fiber of the above equivalence at $\idfunc[A]$ is contractible. Therefore, we can show that univalence implies weak function extensionality by showing that the dependent function type $\prd{x:A}P(x)$ is a retract of $\hfiber{\alpha}{\idfunc[A]}$.

\begin{thm}\label{uatowfe}
In a univalent universe $\type$, suppose that $P:A\to\type$ is a family of contractible types
and let $\alpha$ be the function of \cref{contrfamtotalpostcompequiv}.
Then $\prd{x:A}P(x)$ is a retract of $\hfiber{\alpha}{\idfunc[A]}$. As a consequence, $\prd{x:A}P(x)$ is contractible. In other words, the univalence axiom implies the weak function extensionality principle.
\end{thm}

\begin{proof}
Define the functions
\begin{align*}
  \varphi &: (\tprd{x:A}P(x))\to\hfiber{\alpha}{\idfunc[A]},\\
  \varphi(f) &\defeq (\lam{x} (x,f(x)),\refl{\idfunc[A]}),
\intertext{and}
  \psi &: \hfiber{\alpha}{\idfunc[A]}\to \tprd{x:A}P(x), \\
  \psi(g,p) &\defeq \lam{x} \trans {\happly (p,x)}{\proj{2} (g(x))}.
\end{align*}
Then $\psi(\varphi(f))=\lam{x} f(x)$, which is $f$, by the uniqueness principle for dependent function types.
\end{proof}

We now show that weak function extensionality implies the usual function extensionality.
Recall from~\eqref{eq:happly} the function $\happly (f,g) : (f = g)\to(f\htpy g)$ which
converts equality of functions to homotopy. In the proof that follows, the univalence
axiom is not used.

\begin{thm}\label{wfetofe}
  \index{function extensionality}%
Weak function extensionality implies the function extensionality \cref{axiom:funext}.
\end{thm}

\begin{proof}
We want to show that
\begin{equation*}
\prd{A:\type}{P:A\to\type}{f,g:\prd{x:A}P(x)}\isequiv(\happly (f,g)).
\end{equation*}
Since a fiberwise map induces an equivalence on total spaces if and only if it is fiberwise an equivalence by \cref{thm:total-fiber-equiv}, it suffices to show that the function of type
\begin{equation*}
\Parens{\sm{g:\prd{x:A}P(x)}(f= g)} \to \sm{g:\prd{x:A}P(x)}(f\htpy g)
\end{equation*}
induced by $\lam{g:\prd{x:A}P(x)} \happly (f,g)$ is an equivalence.
Since the type on the left is contractible by \cref{thm:contr-paths}, it suffices to show that the type on the right:
\begin{equation}\label{eq:uatofesp}
\sm{g:\prd{x:A}P(x)}\prd{x:A}f(x)= g(x)
\end{equation}
is contractible.
Now \cref{thm:ttac} says that this is equivalent to
\begin{equation}\label{eq:uatofeps}
\prd{x:A}\sm{u:P(x)}f(x)= u.
\end{equation}
The proof of \cref{thm:ttac} uses function extensionality, but only for one of the composites.
Thus, without assuming function extensionality, we can conclude that~\eqref{eq:uatofesp} is a retract\index{retract!of a type} of~\eqref{eq:uatofeps}.
And~\eqref{eq:uatofeps} is a product of contractible types, which is contractible by the weak function extensionality principle; hence~\eqref{eq:uatofesp} is also contractible.
\end{proof}

\sectionNotes

The fact that the space of continuous maps equipped with quasi-inverses has the wrong homotopy type to be the ``space of homotopy equivalences'' is well-known in algebraic topology.
In that context, the ``space of homotopy equivalences'' $(\eqv AB)$ is usually defined simply as the subspace of the function space $(A\to B)$ consisting of the functions that are homotopy equivalences.
In type theory, this would correspond most closely to $\sm{f:A\to B} \brck{\qinv(f)}$; see \cref{ex:brck-qinv}.

The first definition of equivalence given in homotopy type theory was the one that we have called $\iscontr(f)$, which was due to Voevodsky.
The possibility of the other definitions was subsequently observed by various people.
The basic theorems about adjoint equivalences\index{adjoint!equivalence} such as \cref{lem:coh-equiv,thm:equiv-iso-adj} are adaptations of standard facts in higher category theory and homotopy theory.
Using bi-invertibility as a definition of equivalences was suggested by Andr\'e Joyal.

The properties of equivalences discussed in \cref{sec:mono-surj,sec:equiv-closures} are well-known in homotopy theory.
Most of them were first proven in type theory by Voevodsky.

The fact that every function is equivalent to a fibration is a standard fact in homotopy theory.
The notion of object classifier
\index{object!classifier}%
\index{classifier!object}%
in $(\infty,1)$-category
\index{.infinity1-category@$(\infty,1)$-category}%
theory (the categorical analogue of \cref{thm:nobject-classifier-appetizer}) is due to Rezk (see~\cite{Rezk05,lurie:higher-topoi}).

Finally, the fact that univalence implies function extensionality (\cref{sec:univalence-implies-funext}) is due to Voevodsky.
Our proof is a simplification of his.
\cref{ex:funext-from-nondep} is also due to Voevodsky.

\sectionExercises

\begin{ex}\label{ex:two-sided-adjoint-equivalences}
  Consider the type of ``two-sided adjoint equivalence\index{adjoint!equivalence} data'' for $f:A\to B$,
  \begin{narrowmultline*}
    \sm{g:B\to A}{\eta: g \circ f \htpy \idfunc[A]}{\epsilon:f \circ g \htpy \idfunc[B]}
    \narrowbreak
    \Parens{\prd{x:A} \map{f}{\eta x} = \epsilon(fx)} \times
    \Parens{\prd{y:B} \map{g}{\epsilon y} = \eta(gy) }.
  \end{narrowmultline*}
  By \cref{lem:coh-equiv}, we know that if $f$ is an equivalence, then this type is inhabited.
  Give a characterization of this type analogous to \cref{lem:qinv-autohtpy}.

  Can you give an example showing that this type is not generally a mere proposition?
  (This will be easier after \cref{cha:hits}.)
\end{ex}

\begin{ex}\label{ex:symmetric-equiv}
  Show that for any $A,B:\UU$, the following type is equivalent to $\eqv A B$.
  \begin{equation*}
    \sm{R:A\to B\to \type}
    \Parens{\prd{a:A} \iscontr\Parens{\sm{b:B} R(a,b)}} \times
    \Parens{\prd{b:B} \iscontr\Parens{\sm{a:A} R(a,b)}}.
  \end{equation*}
  Can you extract from this a definition of a type satisfying the three desiderata of $\isequiv(f)$?
\end{ex}

\begin{ex} \label{ex:qinv-autohtpy-no-univalence}
  Reformulate the proof of \cref{lem:qinv-autohtpy} without using univalence.
\end{ex}

\begin{ex}[The unstable octahedral axiom]\label{ex:unstable-octahedron}
  \index{axiom!unstable octahedral}%
  \index{octahedral axiom, unstable}%
  Suppose $f:A\to B$ and $g:B\to C$ and $b:B$.
  \begin{enumerate}
  \item Show that there is a natural map $\hfib{g\circ f}{g(b)} \to \hfib{g}{g(b)}$ whose fiber over $(b,\refl{g(b)})$ is equivalent to $\hfib f b$.
  \item Show that $\eqv{\hfib{g\circ f}{c}}{\sm{w:\hfib{g}{c}} \hfib f {\proj1 w}}$.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:2-out-of-6}
  \index{2-out-of-6 property}%
  Prove that equivalences satisfy the \emph{2-out-of-6 property}: given $f:A\to B$ and $g:B\to C$ and $h:C\to D$, if $g\circ f$ and $h\circ g$ are equivalences, so are $f$, $g$, $h$, and $h\circ g\circ f$.
  Use this to give a higher-level proof of \cref{thm:paths-respects-equiv}.
\end{ex}

\begin{ex}\label{ex:qinv-univalence}
  For $A,B:\UU$, define
  \[ \mathsf{idtoqinv}_{A,B} :(A=B) \to \sm{f:A\to B}\qinv(f) \]
  by path induction in the obvious way.
  Let \textbf{\textsf{qinv}-univalence} denote the modified form of the univalence axiom which asserts that for all $A,B:\UU$ the function $\mathsf{idtoqinv}_{A,B}$ has a quasi-inverse.
  \begin{enumerate}
  \item Show that \qinv-univalence can be used instead of univalence in the proof of function extensionality in \cref{sec:univalence-implies-funext}.
  \item Show that \qinv-univalence can be used instead of univalence in the proof of \cref{thm:qinv-notprop}.
  \item Show that \qinv-univalence is inconsistent (i.e.\ allows construction of an inhabitant of $\emptyt$).
    Thus, the use of a ``good'' version of $\isequiv$ is essential in the statement of univalence.
  \end{enumerate}
\end{ex}

\begin{ex}\label{ex:embedding-cancellable}
  Show that a function $f:A\to B$ is an embedding if and only if the following two conditions hold:
  \begin{enumerate}
  \item $f$ is \emph{left cancellable}, i.e.\ for any $x,y:A$, if $f(x)=f(y)$ then $x=y$.\label{item:ex:ec1}
  \item For any $x:A$, the map $\apfunc f: \Omega(A,x) \to \Omega(B,f(x))$ is an equivalence.\label{item:ex:ec2}
  \end{enumerate}
  (In particular, if $A$ is a set, then $f$ is an embedding if and only if it is left-cancellable and $\Omega(B,f(x))$ is contractible for all $x:A$.)
  Give examples to show that neither of~\ref{item:ex:ec1} or~\ref{item:ex:ec2} implies the other.
\end{ex}

\begin{ex}\label{ex:cancellable-from-bool}
  Show that the type of left-cancellable functions $\bool\to B$ (see \cref{ex:embedding-cancellable}) is equivalent to $\sm{x,y:B}(x\neq y)$.
  Give a similar explicit characterization of the type of embeddings $\bool\to B$.
\end{ex}

\begin{ex}\label{ex:funext-from-nondep}
  The \textbf{na\"{i}ve non-dependent function extensionality axiom} says that for $A,B:\type$ and $f,g:A\to B$ there is a function $(\prd{x:A} f(x)=g(x)) \to (f=g)$.
  \indexdef{function extensionality!non-dependent}%
  Modify the argument of \cref{sec:univalence-implies-funext} to show that this axiom implies the full function extensionality axiom (\cref{axiom:funext}).
\end{ex}

% Local Variables:
% TeX-master: "hott-online"
% End: