A Modal Proof of the Nerve Theorem

Explore a modal homotopy type theory approach to proving the classical nerve theorem in this Oxford Seminar presentation. Discover how the nerve theorem, traditionally attributed to Borsuk, computes the homotopy type of paracompact topological spaces using "good" open covers where finite intersections are contractible. Learn about the nerve construction as a simplicial complex and understand how key concepts like homotopy types of spaces, simplicial sets, and the Čech nerve can be interpreted as modalities acting on simplicial spatial homotopy types. Examine the theorem as a modal statement about the commutation of combinatorial and continuous cohesion in Lawvere's sense, leading to a direct conceptual proof that extends to all spatial stacks on topological sites. This joint work with Mitchell Riley demonstrates how modal homotopy type theory provides new insights into classical results in algebraic topology and homotopy theory.