natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In homotopy type theory, given types and , a function is an effective epimorphism if 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 between two sets and are effective epimorphisms.
Last revised on December 9, 2024 at 19:59:19. See the history of this page for a list of all contributions to it.