Showing changes from revision #2 to #3:
Added | Removed | Changed
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.
Revision on September 14, 2018 at 15:52:31 by Ali Caglayan. See the history of this page for a list of all contributions to it.