Tom day Jong

Tom day Jong

A workshop in honour of the submission of Tom's thesis

Friday 21 October 2022

(Picture from Tom's website)


All times are BST (British Summer Time, UTC+1)

11:40-12:20 Tour Computer Science Building
12:20-13:30 Lunch Noble Room, Staff House
13:30-14:20 Seminar 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.