Homotopy Type Theory essentially surjective > history (Rev #2, changes)

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

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