Synthetic Spectra via a Monadic and Comonadic Modality

Mitchell Riley, Eric Finster, Daniel R. Licata

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…