EPIMORPHISMS AND ACYCLIC TYPES IN UNIVALENT FOUNDATIONS
Abstract 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 synthetic homotopy theory as developed in univalent foundations. We present examples and applications in group theory, such as the acyclicity of the Higman group, through the identification of groups with 0-connected, pointed 1-types. Many of our results are formalized as part of the agda-unimath library.
Authors
- Tom de Jong (ORCID: https://orcid.org/0000-0003-1585-3172)
- Ulrik Buchholtz (ORCID: https://orcid.org/0000-0002-5944-6838)
- Egbert Rijke (ORCID: https://orcid.org/0000-0002-5272-6175)
Institutions
- University of Nottingham (GB)
- University of Ljubljana (SI)
- Institute of Mathematics, Physics, and Mechanics (SI)
Publication Details
- Journal
- Journal of Symbolic Logic
- Published
- 2025-02-06
- DOI
- https://doi.org/10.1017/jsl.2024.76
- Primary Topic
- Homotopy and Cohomology in Algebraic Topology
- Type
- article
- Field-Weighted Citation Impact
- 0.00
Funders
- Royal Society
- U.S. Air Force
- Multidisciplinary University Research Initiative
- Air Force Office of Scientific Research