Homotopy Type Theory
equivalence of precategories (changes)

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



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


Lemma 9.4.2

If for F:ABF : A \to B there exists G:BAG : B \to A and isomorphisms? GF1 AG F \cong 1_A and FG1 BF G \cong 1_B, then FF is an equivalence of precategories.


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 AA and BB and functor F:ABF : A \to B, the following types are equivalent?.

  1. FF is an equivalence of precategories
  2. FF is fully faithful and split essentially surjective

Proof. Suppose FF is an equivalence of precategories with G,η,ϵG,\eta,\epsilon specified. Then we have the function

hom B(Fa,Fb) hom A(a,b), g η b 1G(g)η a. \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)f:hom_A(a,b), we have

η b 1G(F(f))η a=η b 1η bf=f\eta_b^{-1} \circ G(F(f)) \circ \eta_a = \eta_b^{-1} \circ \eta_b \circ f = f

while for g:hom B(Fa,Fb)g: hom_B(F a, F b) we have

F(η b 1G(g)η a) =F(η b 1)F(G(g))F(η a) =ϵ FbF(G(g))F(η a) =gϵ FaF(η a) =g \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,bF_{a,b} is an equivalence, so FF is fully faithful. Finally, for any b:Bb:B, we have Gb:AG b : A and ϵ b:FGbb\epsilon_b : F G b \cong b.

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

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

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

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

See also

Category theory functor fully faithful functor split essentially surjective


HoTT Book

category: category theory

Last revised on September 19, 2018 at 13:56:57. See the history of this page for a list of all contributions to it.