Tom de Jong and Ulrik Buchholz: On acyclic types

Speakers: Tom de Jong and Ulrik Buchholz (University of Nottingham)

Abstract: It is well known that the epimorphisms in the category of sets are exactly the surjections. But what are the epimorphisms of types? Thinking of types as spaces, and following literature in algebraic topology, we characterize epimorphisms of types in homotopy type theory (HoTT) as so-called acyclic maps. An acyclic map is a map whose fibers are acyclic types, and a type is acyclic if its suspension is contractible. We also consider a weaker notion: a type is $k$-acyclic (for $k ≥ -2$) if its suspension is $k$-connected. We show, for example, that the classifying type of a group $G$ is 2-acyclic if and only if the group $G$ is perfect, i.e., its abelianisation is trivial. The Higman group, a well-known example in combinatorial group theory, allows us to construct a nontrivial acyclic type.

In the second half of the talk, we investigate Quillen's plus-construction in HoTT. We identify a meta-theoretic assumption under which this makes sense (i.e., is unique if it exists), dubbed the plus principle. This also provides a characterization of when extensions along epimorphisms exist. Time permitting, we sketch how the plus construction can be effected, assuming Whitehead's principle.

This is joint work with Egbert Rijke.