Epimorphisms and Acyclic Types in Univalent Foundations
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866929708093931520 |
|---|---|
| author | Buchholtz, Ulrik de Jong, Tom Rijke, Egbert |
| author_facet | Buchholtz, Ulrik de Jong, Tom Rijke, Egbert |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_14106 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Epimorphisms and Acyclic Types in Univalent Foundations Buchholtz, Ulrik de Jong, Tom Rijke, Egbert Logic in Computer Science Algebraic Topology Category Theory 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. |
| title | Epimorphisms and Acyclic Types in Univalent Foundations |
| topic | Logic in Computer Science Algebraic Topology Category Theory |
| url | https://arxiv.org/abs/2401.14106 |