Homotopy Type Theory
equivalence of precategories (Rev #3)

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.

References

HoTT book

category: category theory

Revision on September 14, 2018 at 11:52:31 by Ali Caglayan. See the history of this page for a list of all contributions to it.