## Equivalence of categories

### Collection

 context ${\bf C},{\bf D}$ … categories definiendum $F$ in ${\bf D}\simeq{\bf C}$ inclusion $F$ in ${\bf D}\longrightarrow{\bf C}$ exists $G$ in ${\bf C}\longrightarrow{\bf D}$ exists $\alpha$ in $FG\cong Id_{\bf C}$ exists $\beta$ in $Id_{\bf D}\cong GF$

### Discussion

#### Elaboration

Here $Id_{\bf C}$ denotes the identity functor on ${\bf C}$.

#### Motivation

We want to formalize when two categories are “exchangeable in terms of results which can be workout in them”. We would call a functors $F$ “invertible” if there is a another functor $G$ so that $G\circ F=Id_{\bf D}$ and $F\circ G=Id_{\bf C}$. However, since one is generally interested in statements involving objects up to isomorphism only, we define a functor to give an “equivalence” by the above definition.

Comparison with homotopy theory: The postulate then looks essentially the same as the one for homotopy equivalent spaces. The natural transformations $\alpha,\beta$ play the role of homotopy equivalences. Working up to isomorphism amounts to working with just any one representative of a homotopy type.