Homotopy Type Theory
equivalence of precategories (Rev #4)

Idea

Definition

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.

Properties

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.

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

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.

See also

Category theory functor fully faithful functor split essentially surjective

References

HoTT Book

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.