Homotopy Type Theory
split essentially surjective (Rev #1, changes)

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

Idea

Definition

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

See also

Category theory equivalence of precategories

References

HoTT book

Revision on September 18, 2018 at 11:38:38 by Ali Caglayan. See the history of this page for a list of all contributions to it.