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

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.

The type of effective epic functions between $A$ and $B$ is defined as

Examples

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

See also

• monic function
• smooth space