Andrew Swan: Cohomology in realizability models of HoTT

Abstract: Cohomology is well known in homotopy theory as one of the main ways of assigning algebraic invariants to spaces, and more generally to objects in higher toposes. It also has a connection with logic first studied by Blass: non trivial cohomology groups detect failures of the axiom of choice. In particular, cohomology groups of the natural numbers can be used to measure failures of countable choice. I'll give two examples of this coming from realizability. The first is the original CCHM model, by using particular characteristics of the model including the role of decidability of degeneracies and the particular construction of HITs. The second is a more natural example of cohomology witnessing the failure of countable choice in Lifschitz realizability.