Acyclic types and epimorphisms in homotopy type theory

14:20-17:00

Questions

17:00-18:30

Social

Bratby Bar, Staff House

18:30-21:30

Social

Lunar Springs, Digbeth

21:30-22:30

Social

Halton Turner Brewing Company, Digbeth

22:30-

Social

Zumhof Biergarten, Digbeth

Talk details

Acyclic types and epimorphisms in homotopy type theory

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 characterise epimorphisms of types in homotopy type theory
(HoTT) as so-called acyclic maps. An acyclic map is a map whose fibres
are acyclic types, and a type is acyclic if its suspension is
contractible. We also consider a weaker notion called k-acyclicity (for
k ≥ -2) and 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. I will not assume any familiarity with HoTT and pause to
introduce the relevant notions. This is joint work with Ulrik Buchholtz
and Egbert Rijke.