Homotopy Type Theory
weak equivalence of precategories (Rev #1)



A functor F:ABF: A \to B is essentially surjective if for all b:Bb:B, there merely exists an a:Aa:A such that FabF a \cong b.

We say that FF is a weak equivalence if it is fully faithful and essentially surjective.

For categories there is no difference between weak equivalences and equivalences.


See also

Category theory equivalence of precategories functor fully faithful functor


HoTT book

Revision on September 19, 2018 at 17:30:57 by Ali Caglayan. See the history of this page for a list of all contributions to it.