Homotopy Type Theory weak equivalence of precategories > history (Rev #3, changes)

Idea

Definition

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

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

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

Properties

See also

Category theory equivalence of precategories functor fully faithful functor

References

HoTT book