Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Epimorphisms and Acyclic Types in Univalent Foundations

Ulrik Buchholtz, Tom de Jong, Egbert Rijke

TL;DR

The paper identifies epimorphisms in univalent foundations with fiberwise acyclic maps, developing a comprehensive internal theory of acyclic maps and $k$-types within synthetic homotopy theory. It proves that every epimorphism is characterized by acyclic fibers and, equivalently, by a contractible fiberwise suspension via the codiagonal, linking to balanced maps and topos-theoretic modalities. A substantial portion is devoted to relativized notions for $k$-types, including $1$- and $2$-acyclic types and their group-theoretic consequences, notably the characterization of perfect groups via $2$-acyclic classifying types. The work also introduces the plus principle to obtain constructive Blakers–Massey-type results for acyclic maps and provides concrete, constructive examples such as Hatcher's 2-dimensional complex and Higman's group, illustrating the theory's reach. Overall, the results advance synthetic homotopy theory by formalizing epis as acyclic maps, elucidating their closure properties, and connecting type-theoretic epimorphisms to algebraic and homological constructs with potential for broader modality-based developments.

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.

Epimorphisms and Acyclic Types in Univalent Foundations

TL;DR

The paper identifies epimorphisms in univalent foundations with fiberwise acyclic maps, developing a comprehensive internal theory of acyclic maps and -types within synthetic homotopy theory. It proves that every epimorphism is characterized by acyclic fibers and, equivalently, by a contractible fiberwise suspension via the codiagonal, linking to balanced maps and topos-theoretic modalities. A substantial portion is devoted to relativized notions for -types, including - and -acyclic types and their group-theoretic consequences, notably the characterization of perfect groups via -acyclic classifying types. The work also introduces the plus principle to obtain constructive Blakers–Massey-type results for acyclic maps and provides concrete, constructive examples such as Hatcher's 2-dimensional complex and Higman's group, illustrating the theory's reach. Overall, the results advance synthetic homotopy theory by formalizing epis as acyclic maps, elucidating their closure properties, and connecting type-theoretic epimorphisms to algebraic and homological constructs with potential for broader modality-based developments.

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.
Paper Structure (21 sections, 65 theorems, 36 equations)

This paper contains 21 sections, 65 theorems, 36 equations.

Table of Contents

  1. Introduction
  2. Outline
  3. Foundations and preliminaries
  4. Formalization
  5. Epimorphisms and acyclic maps
  6. Acyclic maps
  7. Closure properties
  8. Balanced maps
  9. Acyclic maps and epimorphisms of k-types
  10. Closure properties
  11. Characterizing 1-acyclic types and applications in group theory
  12. Characterizing 2-acyclic types
  13. Iterated suspensions and stabilization
  14. The plus principle
  15. The Blakers--Massey theorem for acyclic maps
  16. ...and 6 more sections

Key Result

Lemma 2.3

A map $f : A \to B$ is epic if and only if the commutative square \begin{tikzcd} A \ar[r,"f"] \ar[d,"f"'] & B \ar[d,"\id"] \\ B \ar[r,"\id"'] & B \end{tikzcd}is a pushout.

Theorems & Definitions (146)

  • Definition 2.1: https://unimath.github.io/agda-unimath/foundation.epimorphisms.html#definitions Epimorphism
  • Remark 2.2
  • Lemma 2.3: https://unimath.github.io/agda-unimath/foundation.epimorphisms.html#the-codiagonal-of-an-epimorphism-is-an-equivalence
  • proof
  • Definition 2.4: https://unimath.github.io/agda-unimath/foundation.dependent-epimorphisms.html#definitions Dependent epimorphism
  • Definition 2.5: https://unimath.github.io/agda-unimath/synthetic-homotopy-theory.suspensions-of-types.html#definitions Suspension $\Sigma A$
  • Definition 2.6: https://unimath.github.io/agda-unimath/synthetic-homotopy-theory.acyclic-types.html#definition Acyclicity
  • Definition 2.7: https://unimath.github.io/agda-unimath/synthetic-homotopy-theory.codiagonals-of-maps.html#definitions Codiagonal $\nabla_f$
  • Lemma 2.8: https://unimath.github.io/agda-unimath/synthetic-homotopy-theory.codiagonals-of-maps.html#the-codiagonal-is-the-fiberwise-suspension
  • proof
  • ...and 136 more