Uploaded August 2025 | Updated September 2026, 2 weeks ago

---

Oxford Seminar, 24th of July 2025

Joint work with Mitchell 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.