A modal proof of the Nerve Theorem

Abstract

Joint work with Mitchel Riley.
The nerve theorem is a classical result in homotopy theory, usually attributed to Borsuk, which computes the homotopy type of a (paracompact) topological space from a “good” open cover of it. An open cover is “good” when finite intersections of opens in the cover are contractible whenever they contain a point; the nerve of a good open cover is the simplicial complex with a point for each open in the cover, and an -simplex for each inhabited intersection of opens in the cover. The nerve theorem states that the homotopy type of is the same as the nerve of any good open cover of it.
In this talk, we’ll prove the nerve theorem in the setting of modal homotopy type theory. The key concepts in the nerve theorem — the homotopy type of a space, the homotopy type presented by a simplicial set, and even the Čech nerve itself — may all be understood as “modalities” which act on simplicial, spatial homotopy types (that is, simplicial stacks on a suitably topological site). Once we understand the idea of modalities, we’ll see that the nerve theorem is a completely modal statement concerning the commutation of two sorts of “cohesion” possible for types (in Lawvere’s sense): the combinatorial cohesion of simplices, and the continuous cohesion of topology. As a result, we’ll actually be proving a nerve theorem for all spatial stacks in a direct, conceptual way.