  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.
