[[!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$$ The type of effective epic functions between $A$ and $B$ is defined as $$EffectiveEpic(A, B) \coloneqq \sum_{f:A \to B} isEffectiveEpic(f)$$ ## Examples ## * The surjections $f:A \to B$ between two [[set]]s $A$ and $B$ are effective epic functions. ## See also ## * [[epic function]] * [[monic function]] * [[multivalued function]]