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? .
Now for any , define to be the unique morphism such that which exists since is fully faithful. Finally for define to be the uniqe morphism such that . It is easy to verify that is a functor and that exhibit as an equivalence of precategories.
We clearly recover the same funcion . For the action of on hom-sets, we must show that for , is the necessarily unique morphism such taht .
But this holds by naturality of . Then we show gives the same data hence .
Category theory functor fully faithful functor split essentially surjective
Revision on September 19, 2018 at 17:56:57 by Ali Caglayan. See the history of this page for a list of all contributions to it.