On the geometry of intuitionistic S4 proofs

The Curry-Howard correspondence between formulas and types, proofs and programs, proof simplification and program execution, also holds for intuitionistic modal logic S4. It turns out that the S4 modalities translate as a monoidal comonad on the space of proofs, giving rise to a canonical augmented simplicial structure. We study the geometry of these augmented simplicial sets, showing that each type gives rise to an augmented simplicial set which is a disjoint sum of nerves of finite lattices of points, plus isolated (-1)-dimensional subcomplexes. As an application, we give semantics of modal proofs (a.k.a., programs) in categories of augmented simplicial sets and of topological spaces, and prove a completeness result in the style of Friedman: if any two proofs have the same denotations in each augmented simplicial model, then they are convertible. This result rests both on the fine geometric structure of the constructed spaces of proofs and on properties of subscone categories-the categorical generalization of the notion of logical relations used in lambda-calculus.