Homotopy Type Theory effective epic function > history (Rev #1)

Definition

Given types $A$ and $B$ , a function $f:A \to B$ is a effective epic function if for all terms $b:B$ the fiber of $f$ over $b$ is inhabited.

isEffectiveEpic(f) \coloneqq \prod_{b:B} \Vert fiber(f, b) \Vert

Examples

The surjections $f:A \to B$ between two sets $A$ and $B$ are effective epic functions.

See also

epic function?
monic function

Revision on March 13, 2022 at 01:01:30 by Anonymous?. See the history of this page for a list of all contributions to it.