A functor is an equivalence of precategories if it is a left adjoint for which and are isomorphisms?. We write for the type of equivalences of precategories from to .
If for there exists and isomorphisms? and , then 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.
For any precategories and and functor , the following types are equivalent?.
Proof. Suppose is an equivalence of precategories with specified. Then we have the function
For , we have
while for we have
using naturality of , and the triangle identities twice. Thus, is an equivalence, so is fully faithful. Finally, for any , we have and .
On the other hand, suppose is fully faithful and split essentially surjective. Define by sending to the given by the spcified essential splitting, and write for the likewise specified isomorphism? .
Category theory functor fully faithful functor split essentially surjective
Revision on September 18, 2018 at 16:26:57 by Ali Caglayan. See the history of this page for a list of all contributions to it.