nLab effective epimorphism in homotopy type theory

Definition

In homotopy type theory, given types $A$ and $B$, a function $f:A \to B$ is an effective epimorphism 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 epimorphisms between $A$ and $B$ is defined as

$$EffectiveEpis(A, B) \coloneqq \sum_{f:A \to B} isEffectiveEpic(f)$$

Examples

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

See also

• n-monomorphism
• effective epimorphism in an (infinity,1)-category