===== Equivalence of categories =====
==== Collection ====
| @#55CCEE: context     | @#55CCEE: ${\bf C},{\bf D}$ ... categories |
| @#FFBB00: definiendum | @#FFBB00: $F$ in ${\bf D}\simeq{\bf C}$ |
| @#AAFFAA: inclusion   | @#AAFFAA: $F$ in ${\bf D}\longrightarrow{\bf C}$ |
| @#FFFDDD: exists      | @#FFFDDD: $G$ in ${\bf C}\longrightarrow{\bf D}$ |
| @#FFFDDD: exists      | @#FFFDDD: $\alpha$ in $FG\cong Id_{\bf C}$ |
| @#FFFDDD: exists      | @#FFFDDD: $\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.

See also [[my equivalence of categories]].

=== Reference ===
Wikipedia: [[http://en.wikipedia.org/wiki/Equivalence_of_categories|Equivalence of categories]]

nLab: [[http://ncatlab.org/nlab/show/equivalence+of+categories|Equivalence of categories]], [[http://ncatlab.org/nlab/show/principle+of+equivalence|Principle of equivalence]]

==== Parents ====
=== Context ===
[[Categories]]
=== Requirements ===
[[Natural isomorphism]], [[Identity functor]]