\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{equivalence of categories}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{category_theory}{}\paragraph*{{Category theory}}\label{category_theory}

[[!include category theory - contents]]

\hypertarget{equality_and_equivalence}{}\paragraph*{{Equality and Equivalence}}\label{equality_and_equivalence}

[[!include equality and equivalence - contents]]

\hypertarget{equivalence_of_categories}{}\section*{{Equivalence of categories}}\label{equivalence_of_categories}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak
\noindent\hyperlink{Variants}{Variants}\dotfill \pageref*{Variants} \linebreak
\noindent\hyperlink{Isomorphism}{Isomorphism}\dotfill \pageref*{Isomorphism} \linebreak
\noindent\hyperlink{StrongEquivalence}{Strong equivalence}\dotfill \pageref*{StrongEquivalence} \linebreak
\noindent\hyperlink{WeakEquivalence}{Weak equivalence}\dotfill \pageref*{WeakEquivalence} \linebreak
\noindent\hyperlink{Anaequivalence}{Anaequivalence}\dotfill \pageref*{Anaequivalence} \linebreak
\noindent\hyperlink{remarks}{Remarks}\dotfill \pageref*{remarks} \linebreak
\noindent\hyperlink{adjoint_equivalence}{Adjoint equivalence}\dotfill \pageref*{adjoint_equivalence} \linebreak
\noindent\hyperlink{an_example_of_a_nonadjoint_equivalence}{An example of a non-adjoint equivalence}\dotfill \pageref*{an_example_of_a_nonadjoint_equivalence} \linebreak
\noindent\hyperlink{in_higher_categories}{In higher categories}\dotfill \pageref*{in_higher_categories} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

The concept of \emph{equivalence of categories} is the correct [[category theory|category theoretic]] notion of ``sameness'' of [[categories]].

Concretely, an equivalence between two categories is a pair of [[functors]] between them which are [[inverse]] to each other \emph{up to} [[natural isomorphism]] of functors ([[inverse functors]]).

This is like an [[isomorphism]], but weakened such as to accomodate for the fact that the correct ambient context for categories is not iself a 1-category, but is the [[2-category]] [[Cat]] of all categories. Hence abstractly an equivalence of categories is just the special case of an [[equivalence in a 2-category]] specialized to [[Cat]].

If some foundational fine print is taken care of, then a functor exhibits an equivalence of categories precisely if it is both [[essentially surjective functor|essentially surjective]] and [[fully faithful functor|fully faithful]]. This is true in [[classical mathematics]] if the [[axiom of choice]] is assumed. It remains true non-classically, say for [[internal categories]], if the concept of functor is suitably adapted (``[[anafunctors]]'').

Form the point of view of [[logic]] one may say that two [[categories]] are \emph{equivalent} if they have the same [[properties]] --- although this only applies (by definition) to properties that obey the \emph{[[principle of equivalence]]}.

Just as equivalence of categories is the generalization of [[isomorphism]] of [[sets]] from sets to categories, so the concept generalizes further to [[higher category theory|higher categories]] (see e.g. \emph{[[equivalence of 2-categories]]}, \emph{[[equivalence of (∞,1)-categories]]}) and ultimately to equivalence of $\infty$-[[infinity-category|categories]].

\hypertarget{definitions}{}\subsection*{{Definitions}}\label{definitions}

\begin{defn}
\label{EquivalenceViaInverseFunctor}\hypertarget{EquivalenceViaInverseFunctor}{}
An \textbf{equivalence} between two [[categories]] $\mathcal{C}$ and $\mathcal{D}$ is an [[equivalence in a 2-category|equivalence in the 2-category]] [[Cat]] of all [[categories]], hence a pair of [[inverse functors]], hence it is

\begin{enumerate}%
\item a pair of [[functors]]

\begin{displaymath}
\mathcal{C} 
    \underoverset
      {\underset{\phantom{AA}F \phantom{AA}}{\longrightarrow}}
      {\overset{\phantom{AA}G\phantom{AA}}{\longleftarrow}}
      {}
  \mathcal{D},
\end{displaymath}

\item [[natural isomorphisms]]

\begin{displaymath}
F \circ G \cong Id_{\mathcal{D}}
\end{displaymath}
and

\begin{displaymath}
G \circ F \cong Id_{\mathcal{C}}
  \,.
\end{displaymath}


\end{enumerate}
This is called an \textbf{[[adjoint equivalence]]} if the natural isomorphisms above satisfy the [[triangle identities]], thus exhibiting $F$ and $G$ as a pair of [[adjoint functors]].

Two categories are called \textbf{equivalent} if there exists an equivalence between them.

\end{defn}
\begin{prop}
\label{ViaEssentiallySurjectiveAndFullyFaithful}\hypertarget{ViaEssentiallySurjectiveAndFullyFaithful}{}
Assume the ambient context is one of the following (see below at \emph{\hyperlink{Variants}{Variants}} for more):

\begin{itemize}%
\item [[classical mathematics]] with the [[axiom of choice]];


\item [[constructive mathematics|constructive]] or [[internal category|internal]] category theory with ``functor'' meaning \emph{[[anafunctor]]};


\item [[homotopy type theory]] with formalization as discussed at \emph{[[internal categories in homotopy type theory]]}.



\end{itemize}
Let $F \colon \mathcal{C} \to \mathcal{D}$ be a [[functor]]. Then the following are equivalent:

\begin{enumerate}%
\item $F$ is part of an equivalence of categories in the sense of def. \ref{EquivalenceViaInverseFunctor}


\item $F$ is

\begin{enumerate}%
\item an [[essentially surjective functor]] and


\item a [[fully faithful functor]].



\end{enumerate}


\end{enumerate}
\end{prop}
\hypertarget{Variants}{}\subsection*{{Variants}}\label{Variants}

We discuss some possible variants of the definition of equivalence of categories, each of which comes naturally from a different view of [[Cat]].

The first, \emph{isomorphism}, comes from viewing $Cat$ as a mere [[1-category]]; it is too strong and is really only of interest for [[strict categories]]. The next, \emph{strong equivalence}, comes from viewing $Cat$ as a [[strict 2-category]]; it is the most common definition given and is correct if and only if the [[axiom of choice]] holds. The next definition, \emph{weak equivalence}, comes from viewing $Cat$ as a [[model category]]; it is correct with or without choice and is about as simple to define as strong equivalence. The last, \emph{anaequivalence}, comes from viewing $Cat$ as a [[bicategory]] that is not (without the axiom of choice) equivalent (as a bicategory!) to the strict $2$-category that defines strong equivalence; it is also always correct.

It is also possible to define `category' in such a way that only a correct definition can be stated, but here we use the usual algebraic definitions of category, [[functor]], and [[natural isomorphism]].

\hypertarget{Isomorphism}{}\subsubsection*{{Isomorphism}}\label{Isomorphism}

Two [[strict categories]] $C$ and $D$ are \textbf{isomorphic} if there exist [[strict functors]] $F\colon C \to D$ and $G\colon D \to C$ such that $F G$ and $G F$ are each [[equality|equal]] to the appropriate [[identity functor]]. In this case, we say that $F$ is an \textbf{isomorphism} from $C$ to $D$ (so $G$ is an isomorphism from $D$ to $C$) and call the pair $(F,G)$ an \textbf{isomorphism} between $C$ and $D$. The functor $G$ is called the \textbf{strict inverse} of $F$ (so $F$ is the strict inverse of $G$).

If you think of $Cat$ as the category of (strict) categories and functors, then this is the usual notion of [[isomorphism]] in a category. This is the most obvious notion of equivalence of categories and the first to be considered, but it is simply too strong for the purposes to which [[category theory]] is put. For example, here are some basic and important equivalences of categories that are not isomorphisms:

\begin{itemize}%
\item Let $C$ be the category of [[pointed sets]], and let $D$ be the category of sets and [[partial functions]]. The functor $F:C\to D$ takes a pointed set to its subset of non-basepoint elements, and a pointed function to the induced partial function on these (which is defined on those elements not sent to the basepoint). See the section ``The category of sets and partial functions'' in [[partial function]] for this equivalence.


\item Let $C$ be the category of finite-dimensional [[vector spaces]] over a [[field]] $k$, and let $D$ be the category whose objects are [[natural numbers]] and whose morphisms $n\to m$ are $m\times n$ matrices of elements of $k$ (which is equivalently the full subcategory of $C$ spanned by the specific vector spaces $k^n$). Note in particular that here $D$ is a [[small category]], while $C$ is not (though it is [[essentially small category|essentially small]], being equivalent to $D$).



\end{itemize}
\hypertarget{StrongEquivalence}{}\subsubsection*{{Strong equivalence}}\label{StrongEquivalence}

Two [[strict categories]] $C$ and $D$ are \textbf{strongly equivalent} if there exist strict functors $F\colon C \to D$ and $G\colon D \to C$ such that $F G$ and $G F$ are each naturally isomorphic (isomorphic in the relevant [[functor category]]) to the appropriate identity functor. In this case, we say that $F$ is a \textbf{strong equivalence} from $C$ to $D$ (so $G$ is a strong equivalence from $D$ to $C$). The functor $G$ is called a \textbf{weak inverse} of $F$ (so $F$ is a weak inverse of $G$).

Note that an isomorphism is precisely a strong equivalence in which the natural isomorphisms are [[identity natural transformation]]s.

If you think of $Cat$ as the [[strict 2-category]] of (strict) categories, functors, and [[natural transformation]]s, then this is the usual notion of [[equivalence]] in a $2$-[[2-category|category]]. This is the first `correct' definition of equivalence to be considered and the one most often seen today; it is only correct using the axiom of choice.

If possible, use or modify the counterexample to isomorphism to show how choice follows if strong equivalence is assumed correct.

\hypertarget{WeakEquivalence}{}\subsubsection*{{Weak equivalence}}\label{WeakEquivalence}

Two categories $C$ and $D$ are \textbf{weakly equivalent} if there exist a category $X$ and functors $F\colon X \to D$ and $G\colon X \to C$ that are [[essentially surjective functor|essentially surjective]] and [[full and faithful functor|fully faithful]]. In this case, we say that $F$ is a \textbf{weak equivalence} from $X$ to $D$ (so $G$ is a weak equivalence from $X$ to $C$) and call the [[span]] $(X,F,G)$ a \textbf{weak equivalence} between $C$ and $D$. (It is not entirely trivial to check that such spans can be composed, but they can be.)

A strict functor with a weak inverse is necessarily essentially surjective and fully faithful; the converse is equivalent to the axiom of choice. Thus any strong equivalence becomes a weak equivalence in which $X$ is taken to be either $C$ or $D$ (or even built symmetrically out of $C$ and $D$ if you're so inclined); a weak equivalence becomes a strong equivalence using the axiom of choice to find weak inverses and composing across $X$.

If you think of $Cat$ as the model category of categories and functors with the [[canonical model structure]], then this is the usual notion of [[weak equivalence]] in a model category.

\hypertarget{Anaequivalence}{}\subsubsection*{{Anaequivalence}}\label{Anaequivalence}

Two categories $C$ and $D$ are \textbf{anaequivalent} if there exist [[anafunctors]] $F\colon C \to D$ and $G\colon D \to C$ such that $F G$ and $G F$ are each ananaturally isomorphic (isomorphic in the relevant [[anafunctor category]]) to the appropriate [[identity anafunctor]]. In this case, we say that $F$ is an \textbf{anaequivalence} from $C$ to $D$ (so $G$ is an anaequivalence from $D$ to $C$). The functor $G$ is called an \textbf{anainverse} of $F$ (so $F$ is an anainverse of $G$). See also \emph{[[weak equivalence of internal categories]]}.

Any strict functor is an anafunctor, so any strong equivalence is an anaequivalence. Using the axiom of choice, any anafunctor is [[ananatural isomorphism|ananaturally isomorphic]] to a strict functor, so any anaequivalence defines a strong equivalence. Using the definition of an anafunctor as an appropriate span of strict functors, a weak equivalence defines two anafunctors which form an anaequivalence; conversely, either anafunctor in an anaequivalence is (as a span) a weak equivalence.

If you think of $Cat$ as the [[bicategory]] of categories, anafunctors, and [[ananatural transformation]]s, then this is the usual notion of [[equivalence]] in a $2$-category. It's fairly straightforward to turn any discussion of functors and strong equivalences in a context where the axiom of choice is assumed into a discussion of anafunctors and anaequivalences in a more general context.

We can also regard the $2$-category $Cat$ above as obtained from the $2$-category $Str Cat$ of strict categories, strict functors, and natural transformations by formally inverting the weak equivalences as in [[homotopy theory]].

\hypertarget{remarks}{}\subsubsection*{{Remarks}}\label{remarks}

Note that \emph{weak} inverses go with \emph{strong} equivalences. The terminology isn't entirely inconsistent (weak inverses contrast with \emph{strict} ones, while weak equivalences contrast with \emph{strong} ones) but developed at different times. The prefix `ana' developed last and is perfectly consistent.

If you accept the axiom of choice, then you don't have to worry about the different kinds of equivalence (as long as you don't use isomorphism). This is not just a question of [[foundations]], however, since the axiom of choice usually fails in [[internalization|internal contexts]].

It's also possible to use foundations (such as [[homotopy type theory]], some other forms of [[type theory]], or [[FOLDS]]) in which isomorphism and strong equivalence are impossible to state. In such a case, one usually drops the prefixes `weak' and `ana'. In the $n$-Lab, we prefer to remain agnostic about foundations but usually drop these prefixes as well, leaving it up to the reader to insert them if necessary.

\hypertarget{adjoint_equivalence}{}\subsection*{{Adjoint equivalence}}\label{adjoint_equivalence}

Any equivalence can be improved to an \textbf{[[adjoint equivalence]]}: a strong equivalence or anaequivalence whose natural isomorphisms satisfy the [[adjoint functor|triangle identities]]. In that case, $G$ is called [[generalized the|the]] \textbf{adjoint inverse} of $F$ (so $F$ is the adjoint inverse of $G$). When working in the $2$-category $Cat$, a good rule of thumb is that it is okay to consider either

\begin{itemize}%
\item a functor with the \emph{property} of being a \emph{general} equivalence or
\item a functor with the \emph{structure} of being an \emph{adjoint} equivalence (that is, a functor $G$ and a pair of natural isomorphisms $F G \cong 1$ and $1 \cong G F$ satisfying the triangle identities),

\end{itemize}
whereas considering

\begin{itemize}%
\item a functor with the \emph{structure} of being a \emph{general} equivalence (that is, merely a functor $G$ and a pair of natural isomorphisms $F G \cong 1$ and $1 \cong G F$)

\end{itemize}
is fraught with peril. For instance, an adjoint inverse is unique up to unique isomorphism (much as a strict inverse is unique up to equality), while a weak inverse or anainverse is not. Including adjoint equivalences is also the only way to make a higher-categorical structure completely \emph{[[algebraic definition of higher category|algebraic]]}.

\hypertarget{an_example_of_a_nonadjoint_equivalence}{}\subsubsection*{{An example of a non-adjoint equivalence}}\label{an_example_of_a_nonadjoint_equivalence}

Identify a group $H$ with its [[delooping]]. One can check the following:

\begin{itemize}%
\item Any equivalence $F : H \leftrightarrows H : G$ of a group with itself comprises two automorphisms $F, G$, such that $F G$ and $G F$ are inner. The unit and counit are the group elements $g_{\rho}$ such that $GF(k) = g_{\rho} k g_{\rho}^{-1}$ and $g_{\sigma}$ such that $FG(k) = g_{\sigma}^{-1} k g_{\sigma}$ for any $k \in H$.


\item Any equivalence of $H$ with itself where $F$ and $G$ are themselves also inner is an adjoint equivalence.


\item If $H$ has trivial center, then any equivalence of $H$ with itself is an adjoint equivalence.


\item To obtain a non-adjoint equivalence, we therefore need a group $H$ with nontrivial center and nontrivial outer automorphisms, such that we can pick two whose products are inner.


\item So take $H = K$ the Klein 4-group. This is a product of abelian groups, so abelian, so is its own center. In fact, it's $\mathbb{Z}/2 \mathbb{Z} \times \mathbb{Z} / 2 \mathbb{Z}$, so let $F = G$ the automorphism which interchanges coordinates. $FG = GF = \operatorname{id}_{K}$, which is given by conjugation by any element.


\item If this were adjoint, the triangle equality for $F$ will stipulate that $F(g_{\rho}) = g_{\sigma}^{-1}$. We can pick $g_{\rho}$ and $g_{\sigma}$ to break this. For example, let $g_{\rho}$ be $(1,1)$ and let $g_{\sigma}$ be $(0,1)$.



\end{itemize}
This is a special case of the fact that, given a non-adjoint equivalence, you can always replace its unit with another unit (which determines the counit) to improve the equivalence to an [[adjoint equivalence]].

\hypertarget{in_higher_categories}{}\subsection*{{In higher categories}}\label{in_higher_categories}

All of the above types of equivalence make sense for $n$-[[n-category|categories]] and $\infty$-categories defined using an [[algebraic definition of higher category]]; again, it is the weak notion that is usually wanted. When using a [[geometric definition of higher category]], often isomorphism cannot even be written down, so equivalence comes more naturally.

In particular, one expects (although a proof depends on the exact definition and hasn't always been done) that in any $(n+1)$-category of $n$-categories, every [[equivalence]] (in the sense of an $(n+1)$-category) will be essentially $k$-[[k-surjective functor|surjective]] for all $0\le k\le n+1$; this is the $n$-version of ``full, faithful, and essentially surjective.'' The converse should be true assuming that

\begin{itemize}%
\item we have an axiom of choice and use weak (pseudo) $n$-[[n-functor|functors]], or
\item we use $n$-[[n-anafunctor|anafunctors]] (which are automatically weak).

\end{itemize}
If we use too strict a notion of $n$-functor, then we will not get the correct notion of equivalence; if we use weak $n$-functors but not anafunctors, then we will get the correct notion of equivalence only if the axiom of choice holds, although again this can be corrected by moving to a span. Note that even strict $n$-categories need weak $n$-functors to get the correct notion of equivalence between them!

For example, assuming choice, a [[strict 2-functor]] between strict $2$-categories is an equivalence in $Bicat$ if and only if it is essentially (up to equivalence) surjective on objects, locally essentially surjective, and [[locally fully faithful 2-functor|locally fully faithful]]. However, its weak inverse may not be a \emph{strict} $2$-functor, and even if it is, the equivalence transformations need not be strictly $2$-natural. Thus, it need not be an equivalence in the [[strict 3-category]] $Str 2 Cat$ of $2$-categories, strict $2$-functors, and strict $2$-natural transformations, or even in the [[semi-strict 3-category]] $Gray$ of strict $2$-categories, strict $2$-functors, and pseudonatural transformations.

As with $Cat$, we can recover $Bicat$ as a [[full subcategory|full]] sub[[tricategory]] of $Gray$ by formally inverting all such weak equivalences. Note that even with the axiom of choice, $Bicat$ is \emph{not} equivalent (as a tricategory) to $Gray$, even though by the coherence theorem for tricategories it is equivalent to \emph{some} $Gray$-category; see \href{http://arxiv.org/abs/math/0612299}{here}.

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item [[equality]], [[isomorphism]], [[equivalence]]


\item [[weak equivalence]], [[homotopy equivalence]], [[weak homotopy equivalence]]


\item [[homotopy equivalence of toposes]]


\item [[equivalence in an (∞,1)-category]]


\item \textbf{equivalence of categories}, [[weak equivalence of internal categories]]


\item [[adjoint functor]]


\item [[equivalence of 2-categories]], [[2-adjunction]]


\item [[equivalence of (∞,1)-categories]], [[adjoint (∞,1)-functor]]



\end{itemize}
[[!redirects equivalence of categories]] [[!redirects equivalences of categories]] [[!redirects equivalent category]] [[!redirects equivalent categories]]

[[!redirects isomorphism of categories]] [[!redirects isomorphisms of categories]] [[!redirects isomorphic category]] [[!redirects isomorphic categories]]

[[!redirects adjoint equivalence of categories]] [[!redirects adjoint equivalences of categories]]

[[!redirects equivalence of n-categories]] [[!redirects equivalences of n-categories]] [[!redirects equivalence of infinity-categories]] [[!redirects equivalences of infinity-categories]] [[!redirects equivalence of higher categories]] [[!redirects equivalences of higher categories]]

[[!redirects equivalence of groupoids]] [[!redirects equivalences of groupoids]] [[!redirects equivalent groupoid]] [[!redirects equivalent groupoids]]

[[!redirects isomorphism of groupoids]] [[!redirects isomorphisms of groupoids]] [[!redirects isomorphic groupoid]] [[!redirects isomorphic groupoids]]

[[!redirects adjoint equivalence of groupoids]] [[!redirects adjoint equivalences of groupoids]]

[[!redirects equivalence of n-groupoids]] [[!redirects equivalences of n-groupoids]] [[!redirects equivalence of infinity-groupoids]] [[!redirects equivalences of infinity-groupoids]] [[!redirects equivalence of higher groupoids]] [[!redirects equivalences of higher groupoids]]



\end{document}