equivalence of precategories (Rev #4)

A functor $F : A \to B$ is an **equivalence of precategories** if it is a left adjoint for which $\eta$ and $\epsilon$ are isomorphisms?. We write $A \equiv B$ for the type of equivalences of precategories from $A$ to $B$.

If for $F : A \to B$ there exists $G : B \to A$ and isomorphisms? $G F \cong 1_A$ and $F G \cong 1_B$, then $F$ is an equivalence of precategories.

**Proof.**

The proof from the HoTT book analogues the proof of Theorem 4.2.3 for equivalence of types. This has not been written up at time of writing.

For any precategories $A$ and $B$ and functor $F : A \to B$, the following types are equivalent?.

- $F$ is an equivalence of precategories
- $F$ is fully faithful and split essentially surjective

**Proof.** Suppose $F$ is an equivalence of precategories with $G,\eta,\epsilon$ specified. Then we have the function

$\begin{aligned}
hom_B(F a, F b) &\to hom_A(a,b), \\
g &\mapsto \eta_b^{-1}\circ G(g) \circ \eta_a.
\end{aligned}$

For $f:hom_A(a,b)$, we have

$\eta_b^{-1} \circ G(F(f)) \circ \eta_a = \eta_b^{-1} \circ \eta_b \circ f = f$

while for $g: hom_B(F a, F b)$ we have

$\begin{aligned}
F(\eta_b^{-1} \circ G(g) \circ \eta_a) &= F(\eta_b^{-1}) \circ F(G(g)) \circ F(\eta_a) \\
&= \epsilon_{F b} \circ F(G(g)) \circ F(\eta_a) \\
&= g \circ \epsilon_{F a} \circ F(\eta_a) \\
&= g
\end{aligned}$

using naturality of $\epsilon$, and the triangle identities twice. Thus, $F_{a,b}$ is an equivalence, so $F$ is fully faithful. Finally, for any $b:B$, we have $G b : A$ and $\epsilon_b : F G b \cong b$.

On the other hand, suppose $F$ is fully faithful and split essentially surjective. Define $G_0:B_0\to A_0$ by sending $b:B$ to the $a:A$ given by the spcified essential splitting, and write $\epsilon_b$ for the likewise specified isomorphism? $F G b \cong b$.

Category theory functor fully faithful functor split essentially surjective

category: category theory

Revision on September 18, 2018 at 12:26:57 by Ali Caglayan. See the history of this page for a list of all contributions to it.