Homotopy Type Theory equivalence of precategories (changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

Definition

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$.

Properties

Lemma 9.4.2

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.

Lemma 9.4.5

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

1. $F$ is an equivalence of precategories
2. $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$.

Now for any $g: hom_B(b,b')$, define $G(g): hom_A(G b, G b')$ to be the unique morphism such that $F(G(g))=(\epsilon_{b'})^{-1} \circ g \circ \epsilon_b$ which exists since $F$ is fully faithful. Finally for $a:A$ define $\eta_a : hom_A(a,G F a)$ to be the uniqe morphism such that $F \eta_a = \epsilon^{-1}_{F a}$. It is easy to verify that $G$ is a functor and that $(G,\eta \epsilon)$ exhibit $F$ as an equivalence of precategories.

We clearly recover the same funcion $G_0 : B_0 \to A_0$. For the action of $F$ on hom-sets, we must show that for $g:hom_B (b,b')$, $G(g)$ is the necessarily unique morphism such taht $F(G(g))=(\epsilon_{b'})^{-1} \circ g \circ \epsilon_b$.

But this holds by naturality of $\epsilon$. Then we show $(2) \to (1) \to (2)$ gives the same data hence $(1)\simeq (2)$. $\square$