nLab effective epimorphism in homotopy type theory

Idea

In homotopy type theory, given types $A$ and $B$, a function $f:A \to B$ is an effective epimorphism if $f$ is the colimit of its Čech nerve. See effective epimorphism in an (infinity,1)-category for the corresponding definition in the categorical semantics.

However, the Čech nerve of a function is a semi-simplicial type in homotopy type theory, and so it is not yet known how to formally define the Čech nerve and effective epimorphisms in homotopy type theory. There have been, however, various extensions to homotopy type theory, such as two-level type theory, bi-cubical type theory, simplicial type theory, and displayed type theory, in which it is possible to define semi-simplicial types, and thus it should be possible to define the Čech nerve, its colimit, and effective epimorphisms in those theories.

It is conjectured that the surjections $f:A \to B$ between two sets $A$ and $B$ are effective epimorphisms.

Related concepts

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