Synthetic Spectra via a Monadic and Comonadic Modality

Abstract

We extend Homotopy Type Theory with a novel modality that is simultaneously a monad and a comonad. Because this modality induces a non-trivial endomap on every type, it requires a more intricate judgemental structure than previous modal extensions of Homotopy Type Theory. We use this theory to develop an synthetic approach to spectra, where spectra are represented by certain types, and constructions on them by type structure: maps of spectra by ordinary functions, loop spaces by the identity type, and so on. We augment the type theory with a pair of axioms, one which implies that the spectra are stable, and the other which relates synthetic spectra to the ordinary definition of spectra in type theory as $\Omega$-spectra. Finally, we show that the type theory is sound and complete for an abstract categorical semantics, in terms of a category-with-families with a weak endomorphism whose functor on contexts is a bireflection, i.e. has a counit an a unit that are a section-retraction pair.

75 pages

References in corpus (8)

• Parametrized spectra, multiplicative Thom spectra, and the twisted Umkehr map
• Quotient inductive-inductive types
• On the homotopy groups of spheres in homotopy type theory
• Homotopy Theoretic Models of Type Theory
• On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
• Space-Valued Diagrams, Type-Theoretically (Extended Abstract)
• Synthetic Homology in Homotopy Type Theory
• Indexed type theories

Cited by in corpus (2)

• Semantics of multimodal adjoint type theory
• Unifying cubical and multimodal type theory