Epimorphisms and acyclic types in univalent foundations

Buchholtz, Ulrik; De Jong, Tom; Rijke, Egbert

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.

Citation

Buchholtz, U., De Jong, T., & Rijke, E. (in press). Epimorphisms and acyclic types in univalent foundations. Journal of Symbolic Logic, 1-36. https://doi.org/10.1017/jsl.2024.76

• Journal Article Type: Article
• Acceptance Date: Oct 29, 2024
• Online Publication Date: Feb 6, 2025
• Deposit Date: Nov 1, 2024
• Publicly Available Date: Aug 7, 2025
• Journal: The Journal of Symbolic Logic
• Print ISSN: 0022-4812
• Electronic ISSN: 1943-5886
• Publisher: Association for Symbolic Logic
• Peer Reviewed: Peer Reviewed
• Pages: 1-36
• ISBN: 0022-4812
• DOI: https://doi.org/10.1017/jsl.2024.76
• Public URL: https://nottingham-repository.worktribe.com/output/41196879
• Publisher URL: https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/epimorphisms-and-acyclic-types-in-univalent-foundations/FA957B9E10172AD18D3271DA28980C45
• Additional Information: Copyright: © The Author(s), 2025. Published by Cambridge University Press on behalf of The Association for Symbolic Logic; License: This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.; Free to read: This content has been made available to all.