Epimorphisms and Acyclic Types in Univalent Foundations

Ulrik Buchholtz, Tom de Jong, Egbert Rijke

We characterize the epimorphisms in homotopy type theory (HoTT) as the fiberwise acyclic maps and develop a type-theoretic treatment of acyclic maps and types in the context of syn…