Abstract
Cohomology groups have a natural definition for types internal to homotopy type theory (HoTT) and so can also be defined for objects of any model of HoTT. Since the cohomology groups are trivial for projective objects, one way of thinking about cohomology is as a “measure” of how the axiom of choice fails. In particular the cohomology group of the natural numbers being non trivial witnesses the failure of countable choice.
I will provide an explicit description of a suitable “externalisation” of the cohomology group of the natural numbers in cubical assemblies from an internal group in the model to an actual group. We can get an explicit description of the externalisation by examining details of the cubical set model, in particular propositional truncation, in a metatheory where the non classical axiom of Church’s thesis holds. I will briefly sketch how to show some non trivial group theoretic properties of the resulting torsion free abelian group using some arguments based on computability theory: it has infinite rank, contains infinitely many copies of the rational numbers, and contains infinitely many pure elements but cannot be decomposed as a direct sum of the form Z ⊕ A.
Talk Details
Speaker: Andrew Swan (University of Ljubljana, Slovenia)
Event: Types and Topology Workshop in Honour of Martin Escardo’s 60th Birthday
Date: Thursday 18 December 2025
Time: 09:55
Key Topics
- Homotopy type theory
- Cohomology groups
- Axiom of choice
- Countable choice
- Cubical assemblies
- Church’s thesis
- Computability theory