[[!redirects effective epimorphism]] ## 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 [[set]]s $A$ and $B$ are effective epic functions. ## See also ## * [[epic function]] * [[monic function]]