#
Homotopy Type Theory

split essentially surjective

## Idea

## Definition

We say that a functor $F : A \to B$ is **split essentially surjective** if for all $b:B$ there exists an $a:A$ such that $F a \cong b$.

## See also

Category theory equivalence of precategories

## References

HoTT book