# Homotopy Type Theory weak equivalence of precategories (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

## 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.