Homotopy type theory allows for a synthetic formulation of homotopy
theory, where arguments can be checked by computer and automatically
apply in many semantic settings. Modern homotopy theory makes
essential use of spectra, a model for stable homotopy
types, where the suspension and loop space operations become an
equivalence.  One can define a version of spectra analytically in type
theory, but with this definition can be quite difficult to work with.
In this paper, we develop an alternative 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.
There is an $\infty$-topos of parametrised spectra, whose
objects are an index space with a family of spectra over it, so
standard homotopy type theory can be interpreted in this setting.  To
isolate the spaces (as objects with trivial spectra) and the spectra
(as objects with trivial base) within this more general setting, we
extend type theory with a novel modality that is simultaneously a
monad and a comonad.  Intuitively, this modality keeps the base of an
object the same but replaces the spectrum over each point with a
trivial one.  Because this modality induces a non-trivial endomap on
every type, it requires a more intricate judgemental structure than
previous modal homotopy type theories.  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.  Next, we augment the type theory with a pair
of axioms, one which implies that the spectra are stable, and the
other which relates the synthetic spectra to the analytic ones, and,
working inside the type theory, show that our synthetic spectra have
many of the properties expected of spectra.

§ INTRODUCTION

Homotopy type theory provides a setting in which one can do
synthetic homotopy theory: rather than working with concrete
topological spaces or simplicial sets, one works with types and the
universal constructions provided by the type formers of the
theory. Working this way requires clever new arguments for standard
results, but the payoff is that the same proof applies in any model of
the theory, not just in the homotopy theory of spaces.  It is
conjectured that all of axiomatic homotopy type theory (“axiomatic
HoTT”) as in <cit.> can be interpreted in any $\infty$-topos
— the interpretation of the basic Martin-Löf type
theory <cit.>, Voevodsky's univalence
axiom <cit.>
and a class of higher inductive types <cit.>
have been worked out, though closure of
the universes under higher inductive types is in progress.  The basics of
synthetic homotopy theory are presented in <cit.>,
and a significant number of results have been developed and formalized

One of the main advantages of axiomatic HoTT is that all
constructions performed in it are necessarily homotopy invariant.
However, this is a double-edged sword, as it rules out some of the first
definitions from algebraic topology one might hope to make. For example,
a key invariant of topological spaces is their homology and cohomology
groups, which are often easier to calculate than their homotopy
groups. Externally, the ordinary homology and cohomology of a space $X$
are defined via maps into $X$ from simplices of various dimensions. But
these simplices are all contractible, so working internally they are
indistinguishable from the point.  Instead, homology and cohomology can
be defined in type theory <cit.> via
the spectra that represent them.

Classically, the study of spectra was motivated by the Freudenthal
suspension theorem (see <cit.> for a proof in type
theory), which implies that, for nice spaces $X$ and $Y$, the sequence
of homotopy classes of maps
\[ [X, Y] \to [\Sigma X, \Sigma Y] \to
[\Sigma^2 X, \Sigma^2 Y] \to \dots \]
stabilises. Stable homotopy theory studies the phenomena
that survive after arbitrarily many suspensions, and it is an important
tool for obtaining results about unstable homotopy theory/spaces as well
— e.g. the homotopy groups of spheres in a certain range coincide with
certain stable homotopy groups. One can form a category out of the above
observation, where the objects are nice pointed spaces and the hom-sets
are given by the colimit over the above diagram, but the resulting
category does not have very nice properties. This motivates passing to
a category of spectra that includes the previous as a full
subcategory, but is much better behaved categorically.

Using $\infty$-categorical technology (by which we mean
$(\infty,1)$-categorical), the $\infty$-category of spectra can be
defined by starting with the $\infty$-category of pointed spaces
$\mathcal{S}_*$, and inverting the loop space functor $\Omega$ in a
universal way:

\begin{align*}
\Spec = \varprojlim \left(  \cdots \xrightarrow{\Omega} \mathcal{S}_* \xrightarrow{\Omega} \mathcal{S}_* \xrightarrow{\Omega} \mathcal{S}_* \right)
\end{align*}

In the $\infty$-category of spectra, the suspension $\Sigma$ and loop
space $\Omega$ functors are equivalences, in contrast to ordinary
spaces where $\Sigma$ and $\Omega$ are far from being
equivalences. This makes $\Spec$ a good place to do stable homotopy
theory: everything is stable under suspension. Spectra behave
much like objects from algebra, such as modules over a ring, or chain
complexes. One has a zero object and biproducts, and every morphism of
spectra has a well-behaved kernel and cokernel. Like chain complexes,
$\Sigma$ and $\Omega$ shift objects up and down in dimension.

Unwinding the above definition, a spectrum can be presented concretely
as a sequence of pointed spaces $X_0,X_1,X_2,\ldots$, together with a
pointed equivalence between each space and the loop space of the next,
$X_0 \equiv_\star \Omega X_1$, $X_1 \equiv_\star \Omega X_2$, ….
This definition of spectra is readily internalised in type
theory, replacing `pointed spaces' with `pointed types', and has been
formalised <cit.>. However, most basic constructions on
spectra are still work in progress, as working with such spectra can
be difficult.  Moreover, re-building the theory of spectra from
scratch within type theory is not so much in the spirit of working
synthetically; we should be leveraging the type theory to provide some
of the structure built-in.

One approach to synthetic spectra would be to look for a type theory
that interprets in the $\infty$-category of spectra, but this category
is not an $\infty$-topos, so the type theory would not include all of
axiomatic HoTT (e.g. it is not even cartesian closed; like modules
over a ring, it is closed for a different notion of monoidal product).
However, spectra are a full subcategory of space-parametrised
families of spectra, which Joyal and Biedermann have shown form an
$\infty$-topos <cit.>. The $\infty$-category
$P\Spec$ of parametrised spectra can be pleasantly described as
follows <cit.>: Given a space $X$, one can think of it as an
$\infty$-groupoid and consider the functor $\infty$-category
$\mathrm{Fun}(X, \Spec)$. The objects of this are our parametrised
spectra over $X$. This assignment from spaces to functor categories
assembles into a functor $\mathcal{S}^\op \to \mathrm{Cat}_\infty$,
with $\mathrm{Cat}_\infty$ the $\infty$-category of
$\infty$-categories. An $\infty$-categorical version of the
Grothendieck construction yields the $\infty$-category $P\Spec$ of
parametrised spectra.  Thus, we can begin by interpreting all of
axiomatic HoTT into this $\infty$-topos $P\Spec$ of parametrised
spectra.  This has important practical advantages over designing a new
type theory for just the spectra, not the families: we can reuse all
of the synthetic homotopy theory that has been developed, and we can
reuse existing proof assistants to work in this setting.

When working in axiomatic HoTT with the model in parametrised spectra
in mind, it will be necessary to have some syntactic way to say when a
type denotes a single spectrum, rather than a family of them — for
example, the fact that suspension and loop space are an equivalence
holds only for spectra, not families thereof.  Moreover, it will be
necessary say when a type (in $P\Spec$) denotes an ordinary space; for
example, some constructions that we will perform apply only to
families of spectra over a space, not families of spectra over a
spectrum, so in certain places we will want to restrict dependency to
types that denote spaces.  It turns out that we can access both the
full subcategory of spaces and the full subcategory of spectra by way
of a modality <cit.>. A basic
operation on $P\Spec$ is the functor that, given a parametrised
spectrum, extracts its underlying space. In the other direction, we
can assign to each space $X$ the parametrised spectrum $(X, 0)$, where
$0 : X \to \Spec$ denotes the constant functor at the zero spectrum,
which has the one-point space at each level (not the empty space,
since the spaces in an $\Omega$-spectrum are all pointed). This is
both left and right adjoint to the forgetful functor from $P\Spec$
to spaces $\mathcal{S}$ that extracts the index space:

\[
\begin{tikzcd}
P\Spec \ar[r] \ar[r, phantom, "\top",yshift=1.5ex, xshift=-0.8ex] \ar[r, phantom, "\top",yshift=-1.5ex, xshift=-0.8ex]&
\mathcal{S} \ar[l, bend left = 40, "0", pos=0.51] \ar[l, bend right = 40, "0" swap]
\end{tikzcd}
\]

and this diagram satisfies the additional coherence of a bireflective
subcategory <cit.>.  This means that the roundtrip on
$P\Spec$, which we write as $\natural$, has a number of special
properties: is a left-exact idempotent monad and comonad, it is
adjoint to itself, and the counit followed by the unit
$\natural E \to E \to \natural E$ is the identity.  Then, we can
isolate the spaces within the parametrised spectra as the
$\natural$-modal types <cit.>, roughly the
types $A$ such that $A \equiv \natural A$ — i.e. an object is a
space iff it is equivalent to the object consisting of the same base
space with the 0-spectrum over every point, because that means the
object has no interesting spectra to begin with.  Dually, we can
isolate the spectra as the $\natural$-connected types, the types such
that $\natural A$ is contractible — i.e. an object is a single
spectrum iff it is a family of spectra over the point.

Monadic modalities are well-studied in axiomatic
HoTT <cit.>, but to describe non-trivial comonadic
modalities, one must modify the judgemental structure of the context.
The adjunction between $\mathcal{S}$ and $P\Spec$ is a degenerate
example of axiomatic cohesion <cit.>. An
$\infty$-topos $\mathcal{T}$ is cohesive (over $\mathcal{S}$) if there
is a string of adjoint functors relating $\mathcal{T}$ to $\mathcal{S}$,
satisfying certain conditions. These adjunctions induce a string of
adjoint functors $\shape \dashv \flat \dashv \sharp$ on $\mathcal{T}$ so
that $\shape$ and $\sharp$ are monads and $\flat$ is a comonad. In our
setting, we have $\shape \defeq \flat \defeq \sharp$, hence the name
$\natural$ for our roundtrip operation.  A `cohesive type theory'
capturing the structure of cohesion was introduced by
Shulman <cit.>, where the three functors also
appear as unary type formers. The part of the theory we are especially
interested in is the $\flat/\sharp$ fragment, which on its own is called
`spatial type theory'. In spatial type theory, the context is divided
into two zones following <cit.>: a `modal' zone,
where the types of all variables are morally prefixed with a $\flat$,
followed by a context with ordinary variables. The rules for the $\flat$
and $\sharp$ modalities move variables between the zones to enforce the
correct relationships between the modalities and the judgemental version
of $\flat$ represented by the modal context zone.  In principle one
could use spatial type theory for $P\Spec$ by adding axioms asserting
that the modalities are all equivalent.  While we have no objection in
principle to adding axioms to type theories for synthetic homotopy
theory (we extend axiomatic HoTT, which already adds univalence and
higher inductive types as axioms), the ergonomics of such axioms can be
poor — in this case, transport across these equivalences would be
pervasive in every construction.

In this paper, we instead describe an extension of the judgements and
rules of type theory, which give the $\natural$ modality the correct
properties without the need for any axioms (Section <ref>).
Relative to existing modal dependent type theories, the primary
difficulty of the $\natural$ modality is that the bireflection induces a
non-trivial roundtrip on every type[In full detail, the
round-trip only applies to types that depend on a space, not a
spectrum.]: the unit map $A \to \natural A$ followed by the counit map
$\natural A \to A$. The syntax has a pair of novel features to handle
this. Firstly, each variable may be used in two ways: as normal, or
“marked”, which is written $\zx$ and means using it via the roundtrip
described above. Secondly, in contrast to spatial type theory, there is
no separation of the context into two zones, one modal and one
non-modal. The presence of both the unit and counit mean that modal and
ordinary variables can be mixed together without restriction.

Next, to demonstrate that the resulting type theory is quite ergonomic
to use, even without a proof assistant, we develop some synthetic
homotopy theory informally in the style of <cit.>.  First, in
Section <ref>, we show that our rules for the $\natural$
modality indeed give it the desired properties—we can prove
internally that it is a monad and comonad, idempotent, self-adjoint,
left-exact, interacts nicely with pointed types, and that the
$\natural$-modal (the “spaces”) are closed under various type constructors.
Next, in Section <ref>, we study the $\natural$-connected types
(the “spectra”), showing that they are pointed and that ordinary
functions between them are automatically pointed, avoiding the need to
carry around proofs of pointedness.  By assuming a base type $\sphere$
(intended to be modelled in $P\Spec$ by the sphere spectrum), we give a
synthetic definition of the adjunction $\Sigma^\infty \dashv
\Omega^\infty$ that relates spaces and spectra, which allows transfer of
information between the unstable and stable worlds.

With the type-theoretic rules for $\natural$, our “synthetic spectra”
do not have all of the properties of spectra.  This is in some sense an
advantage — we can also interpret all of the above constructions in a
simpler model in parametrised pointed spaces, which we give some
intuition for in Section <ref>.  But, to bring the
synthetic spectra closer to spectra, we identify two axioms.  The first,
studied in Section <ref>, makes the internal category of
synthetic spectra stable, in particular making $\Sigma \dashv \Omega$
an adjoint equivalence for these types. It turns out to be sufficient to
assert that coproducts and products of synthetic spectra coincide.
Together with the ambient setting of an $\infty$-topos and a left-exact
$\natural$ modality, this causes commutative squares of
spectra to be pushouts if and only if they are pullbacks, which,
together with finite limits/colimits and a zero object, is an equivalent
characterisation of the stability of an $\infty$-category.  The proof
that this axiom implies stability uses a recent advance in synthetic
homotopy theory, the Generalized Blakers-Massey Theorem <cit.>.

The second axiom connects our synthetic spectra to `analytic' spectra,
defined concretely as sequences of pointed types with connecting maps.
Using the above stability axiom, we show that the
$\Sigma^\infty \dashv \Omega^\infty$ adjunction between pointed types
and synthetic spectra can be factored through analytic spectra,
defining in particular an adjunction between synthetic and analytic
spectra. For this part, we assume the correctness of an analytic
spectrification operation, which has been defined but not yet proved
correct in type theory. Our second axiom is that this adjunction
between synthetic and analytic spectra is an equivalence.  As an
application, we show that this axiom is is strong enough to fix the
homotopy groups (appropriately defined) of the synthetic sphere
spectrum to be the stable homotopy groups of the ordinary higher
inductive spheres, using some recent work on sequential
colimits <cit.>.

Finally, in Section <ref>, we give a sound and complete
categorical semantics for our type theory, in categories with families
enhanced with extra structure to interpret the modality. In
particular, we require a weak CwF endomorphism such that the underlying
functor on contexts is a bireflection, i.e. has a counit-unit
section-retraction pair.

Related work.

Our rules for the natural modality follow the work on constructive modal
logics such constructive S4, intuitionistic linear logic, and adjoint
logic — especially presentations with two contexts or different
judgements for modal assumptions — and their generalisations with
types <cit.>.
The most directly related calculi are spatial type
theory <cit.> and the calculi for right adjoint
functors/comonads <cit.>.  While
these previous works inform our design in Section <ref>, none
consider a bireflective modality as we do here, and there were still
some interesting design questions specific to our setting.  For example,
because $\natural$ is both a monad and a comonad, the previous work
suggests two possible designs:
<cit.> have special context
structure corresponding to a comonad, and the counit is a “silent”
operation (not marked in the proof term), while <cit.>
has special context structure for a monad, and the unit is a silent
operation.  In our setting, we have both a monad and a comonad, but the
“roundtrip” of the unit followed by the counit is not the
identity, so we cannot make both the unit and counit silent.  After some
experimentation, we chose to make the unit silent and the counit
explicit via “marked” variables.

Some additional related work
develops frameworks for modal type theories in
general <cit.>, but our setting is not quite an
instance of these frameworks. The first <cit.> lacks
dependent types, but can describe the simply-typed fragment of our type
The mode theories of the second <cit.>, do not
allow making the left adjoint types (“locks”) into CwF morphisms,
which corresponds in our setting to defining the natural operation on
contexts as a context of individually marked variables.  Additionally,
our contribution in Section <ref> is an “optimised” syntax
where structural rules are combined with other rules, and as much is
admissible as possible, and the step from these frameworks to an
optimised syntax is currently one that must be undertaken for each type
theory separately in any case.

There is also work by Isaev on `indexed type
theories' <cit.>, which correspond to
indexed ($\infty$-)categories. The theory of parametrised spectra can
be described in terms of an indexed $\infty$-category over spaces,
where the $\infty$-category over each fixed space $X$ is
$\mathrm{Fun}(X, \Spec)$. But there are significant benefits in
considering the total category as we do: the existing constructions of
type theory automatically apply to types that correspond to spectra,
whereas in indexed type theory one needs to add an indexed version of
each type constructor together with axioms relating the base and
indexed versions of each. Our ordinary universe $\univ$ is already a
universe of parametrised spectra; in an indexed type theory one has a
universe for the types in the base, but seems difficult to extend this
to indexed types, as only the total category has a universe.

Acknowledgements: The work in this paper benefited heavily
from discussions with Michael Shulman and Mathieu Anel, in particular
to Mike for suggesting Axiom N. Thank you also to Ed Morehouse and
Alex Kavvos for many helpful conversations.

§ THE $\NATURAL$ MODALITY

In this paper, we begin with homotopy type theory as in <cit.>
with $\Pi$, $\Sigma$, identity, and (higher) inductive types, and
univalent universes.  We then add a new modality, a unary type
constructor $\natural$.  Unlike the monadic modalities studied
in <cit.>, which can be described by axioms, our
$\natural$ modality also has some comonadic aspects, which require
changes to the judgements of the type theory.  We first describe a
judgemental version of the modality that applies to contexts and has the
desired unit and counit maps, and then give a type constructor that
internalises this judgemental operation as a type.

§.§ New Judgemental Rules

Marked context extension and variables:

\[
\begin{array}{ccc}
\inferrule*[left=ctx-ext-zero]{\Gamma \ctx \and \zc{\Gamma} \yields A : \univ}{\Gamma, \zx :: A  \ctx} &
\inferrule*[left=var-zero]{~}{\Gamma, \zx :: A, \Gamma' \yields \zx : A}  &
\inferrule*[left=var-roundtrip]{~}{\Gamma, x : A, \Gamma' \yields \zx : \zA}
\end{array}
\]

Natural on contexts:

\[
\raisebox{-10px}{$
\inferrule*[fraction={-{\,-\,}-}]{\Gamma \ctx}{\zc{\Gamma} \ctx}$}
\qquad
\begin{array}{rl}
\zc{\cdot} &:\defeq \cdot \\
\zc{\Gamma, x : A} &:\defeq \zc{\Gamma}, \zx :: \zA \\
\zc{\Gamma, \zx :: A} &:\defeq \zc{\Gamma}, \zx :: A
\end{array}
\qquad
\inferrule*[fraction={-{\,-\,}-}]{ }
{\zc{\zc{\Gamma}} \defeq \zc{\Gamma}}
\]

Precomposition with the counit:

\[
\inferrule*[left=pre-counit,fraction={-{\,-\,}-}]
{\Gamma \yields a:A}{\zc{\Gamma} \yields \za : \zA}
\qquad
\inferrule*[fraction={-{\,-\,}-}]
{\zc{\Gamma} \vdash a : A}
{\zc{\Gamma} \vdash \za \defeq a : A}
\qquad
\inferrule*[fraction={-{\,-\,}-}]{\Gamma \vdash a : A}
{\zc{\Gamma} \vdash \underline{\underline a} \defeq \underline a : \zA}
\]

\[
\raisebox{-10px}{$
\inferrule*[fraction={-{\,-\,}-}]{\Gamma \yields \Delta \tele}{\zc{\Gamma} \yields \Delta^{0\Gamma} \tele}$}
\qquad
\begin{array}{rl}
(\cdot)^{0\Gamma} &:\defeq \cdot \\
(\Delta, x : A)^{0\Gamma} &:\defeq \Delta^{0\Gamma}, x : A^{0\Gamma} \\
(\Delta, \zx :: A)^{0\Gamma} &:\defeq \Delta^{0\Gamma}, \zx :: A
\end{array}
\qquad
\inferrule*[left=pre-counit-gen,fraction={-{\,-\,}-}]
{\Gamma,\Delta \yields a:A}{\zc{\Gamma}, \Delta^{0\Gamma} \yields a^{0\Gamma} : A^{0\Gamma}}
\]

Precomposition with the unit/roundtrip:

\[
\inferrule*[left=pre-unit,fraction={-{\,-\,}-}]
{\Psi,\zc{\Gamma},\Delta \yields a : A}
{\Psi,\Gamma,\Delta \yields a : A}
\qquad
\inferrule*[left=pre-roundtrip,fraction={-{\,-\,}-}]
{\Gamma \yields a : A}
{\Gamma \yields\za : \zA}
\qquad
\inferrule*[left=pre-roundtrip-gen,fraction={-{\,-\,}-}]
{\Gamma,\Delta \yields a :A}
{\Gamma, \Delta^{0\Gamma} \yields a^{0\Gamma} : A^{0\Gamma}}
\]

New Context Structure.  Dashed lines indicate admissible

At a high level, the reason we require some new judgemental structure
for presenting the $\natural$ modality is that it has both a unit $A \to
\natural A$ and a counit $\natural A \to A$ and the roundtrip $A
\to \natural A \to A$ gives a non-trivial map for general types $A$. So
to $\beta$-reduce an introduction followed by an elimination, we need a
judgemental version of this roundtrip map $A \to A$ to reduce to.  This
must satisfy a naturality equation, which says that for any $f : A \to
B$, the composites $A \to B \to \natural B \to B$ and $A \to \natural A
\to A \to B$ are equal: post-composing with the roundtrip is the same as
precomposing with it.  To achieve this, we add post-composition with the
roundtrip as a new way of using variables: for a variable $x : A$, we
write $\zx$ for the roundtrip on $A$ applied to $x$, and say that the
variable is marked or zeroed or dull.  For a
general term $a$, we define an admissible operation $\za$ that
“underlines all of the free variables of $a$”, and denotes
precomposing with the roundtrip on the context.  This gives normal forms
for the above naturality equations.  There is an interaction with
dependency, because applying the roundtrip to a term must also apply it
to the term's type, so if $a : A$ then $\za : \zA$.  For certain rules,
we will need a judgement classifying terms whose free variables are
only used marked, which we call dull terms. We accomplish
this by allowing variable declarations in the context to be marked as
well, written $\zx :: A$, which semantically is the same as $x :
\natural A$.  A variable declared marked in the context can only be used
marked, so a term in a context of only marked declarations must be
dull.  Any context $\Gamma$ can be turned into a context of only marked
declarations via a defined $\zc{\Gamma}$ operation, which semantically
is applying the $\natural$ modality to the context.  Finally, we have
admissible structural rules corresponding to precomposing a judgement
with the unit $\Gamma \to \zc{\Gamma}$ and counit $\zc{\Gamma} \to
\Gamma$.  We now discuss the rules in Figure <ref> in
more detail.

Marked Context Extension and Variables.
To make the type theory easier to use, we will make $\zc{\Gamma}$ an
admissible (defined by induction on syntax) operation, rather
than a derivable (new piece of formal syntax) one. The new piece
of formal syntax is a new context extension $\Gamma,\zx :: A$
(ctx-ext-zero), which semantically is the same as
$\Gamma.\natural A$.  We think of this special context extension as
“marking” a variable by writing $::$ in place of $:$, and by writing
an underscore under the variable name.  Formally, either one of the
underscore or the $::$ would be enough, but we find the syntax
clearer if variables are written the same in the context and at their
use sites, which will be marked; and we carry over the $::$ from spatial
type theory <cit.>.

The restriction imposed by a marked context extension is that a
variable that is declared marked in the context $\Gamma,\zx :: A$ can
only be used marked as $\zx$ in a term, as indicated in the
var-zero rule. Semantically, this is using the counit $\natural
A \to A$, because $\zx :: A$ in the context is semantically $\natural
A$, but $A$ as a type on the right is semantically just $A$.  In
concrete syntax, it is best to think of $\zx$ as a term constructor
$\textsf{underline}(x)$, not that the underline is part of the variable

A new ingredient for the $\natural$ modality is that there are two ways
to use an ordinary unmarked variable declared in the context as
$\Gamma,x : A,\Gamma'$. In addition to the standard rule
$\Gamma,x:A,\Gamma' \vdash x : A$, we can also apply the
var-roundtrip rule, and use the variable $x$ by writing $\zx$.
We say that such a use is marked or zeroed, because
semantically, it corresponds to the projection from $\Gamma$ post-composed with the roundtrip $A \to \natural A \to A$.
In our intended models, this keeps the base of $x$ the same but
replaces the fibres of $x$ with the default sections of $A$.  We
intentionally use the same raw syntax for these two distinct typing
rules var-zero and var-roundtrip, one of which uses a
variable that is marked in the context (via the counit), and the other
uses a variable that is unmarked in the context (via the roundtrip).
This allows precomposition with the unit $\Gamma \to \zc{\Gamma}$ to be
a “silent” operation that leaves the raw syntax unchanged.
We explain the operation $\zA$ marking a type below.

Natural on Contexts
Proceeding to the admissible rules in the figure, marking a context
$\zc{\Gamma}$ is defined inductively by marking all of the
variables in a context.  Semantically, these equations say (roughly —
there are some subtleties with dependency that we discuss below) that
$\natural 1 = 1$, $\natural (\Gamma.A) = \natural \Gamma.\natural A$
(which are the equations of a strict CwF morphism <cit.>) and that $\natural(\Gamma.\natural A) =
\natural \Gamma.\natural A$ (which is reasonable because of idempotence
$\natural \natural A = \natural A$).  The equation states that
$\zc{\Gamma}$ is idempotent—syntactically, $\zc{\Gamma}$ has only
marked variable declarations, which $\zc{\zc{ \Gamma}}$ leaves
unchanged (and the $\zA$ operation discussed next is also idempotent).

Putting together ctx-ext-zero and var-zero and the
definition of $\zc{\Gamma}$, the types of later marked variables can
depend on earlier unmarked ones (but can only use them marked). For
example, in a context $x : A, \zy::B$, the type $B$ is in context
$\zc{x:A} \defeq \zx::\zA$, so may refer to $\zx$ (but not $x$).  This
means we cannot put all of the marked variables in a separate context
zone preceding the unmarked variables <cit.>.

Precomposition with the Counit.
We will often be interested in types and terms where every use of a free
variable is marked/zeroed. We call such types and terms dull. A
dull term in context $\Gamma$ is equivalently a term in the context
$\zc{\Gamma}$—because all the variables in $\zc{\Gamma}$ are marked,
any term $\zc{\Gamma} \yields a : A$ necessarily uses these variables
marked.  We can turn any $\Gamma \vdash a : A$ into a dull term
$\zc{\Gamma} \vdash \za : \zA$ by marking all the free variable uses in
$\za$ with an underscore (pre-counit).  (Note that we overload
the notation and write the $\za$ operation on general terms using the
same syntax as for marked/roundtripped variables.) Semantically, $\za$
is precomposing $a$ with the counit $\zc{\Gamma} \to \Gamma$.  Because
the type $A$ also depends on $\Gamma$, substitution by the counit will
also mark its variables, which we write as $\zA$. We think of types
as elements of a universe, so $\Gamma \vdash A : \univ$ implies
$\zc{\Gamma} \vdash \zA : \univ$ is another instance of this rule.
This means that when a term is marked/zeroed i.e. only varies over
the underlying space of the context, its corresponding type is also
only permitted to vary over the underlying space of the context.

We omit a formal definition of $\za$ on raw syntax, which is given by
recursion over the term syntax (like substitution), turning $x$ into
$\zx$, leaving marked variable uses unchanged, and proceeding
recursively otherwise (e.g. $\underline{f(a)} =
\underline{f}(\underline{a})$). In particular, zeroing commutes with the
type former for $\Idsym$-types: $(\zc{x = y}) \defeq (\zx = \zy)$, which
is part of what makes our modality left-exact.

One subtlety is that, because $\za$ is semantically
substitution/precomposition with the counit $\zc{\Gamma} \to \Gamma$,
it marks the free variables of a term, but leaves the bound
variables the same. For example,
$\underline{\lambda x.f x} \defeq \lambda x.\underline f x$.  This
leads to the full form of the operation in pre-counit-gen,
which marks the variables in $\Gamma$ in the context and changes all
occurrences of the $\Gamma$-variables in the term into marked ones,
but does not change the occurrences of $\Delta$-variables in the term.
Formally, $\Delta$ is a telescope (context in context), but we omit
the rules for $\Gamma \vdash \Delta \,\, \mathsf{telescope}$, with
formation rules analogous to those for contexts, and the operation of
concatenating a context and a telescope $\Gamma,\Delta$.  For example,
with $f$ in $\Gamma$ and $x$ in $\Delta$, $\underline{f x} = \zf x$.
However, when the variables declared in $\Gamma$ occur in the types in
$\Delta$, those occurrences must be marked, which we notate with
${\Delta}^{0\Gamma}$. The telescope ${\Delta}^{0\Gamma}$ is defined by
sending $x:A$ to $x:A^{0\Gamma}$ (not $\zx::A^{0\Gamma}$,
differing from $\zc{\Gamma}$) and $\zx::A$ to $\zx :: A$ (since all
variables are already zeroed) for each variable in $\Delta$.
Officially, we should be annotating the underscores like $\za_\Gamma$
to indicate which variables in $a$ are to be zeroed, but when we
use this operation informally we always start with $\Gamma$
being all free variables and $\Delta$ empty, so we adopt a
convention that $\za$ means to mark all free variables of $a$.

The equations for precomposition with the counit state that if a term
starts out in $\zc{\Gamma}$, then marking has no effect $\za \defeq a$.
Syntactically, this is because a term in context $\zc{\Gamma}$ cannot
have any unmarked free variable uses, which are the only parts of a term
changed by the marking operation.  Note that this equation needs
$\zc{\zc{\Gamma}} \defeq \zc{\Gamma}$ to type check, and semantically
corresponds to the counit on $\zc{\Gamma}$ being the identity.
Consequently, marking is idempotent: $\zc{\za} \defeq \za$.

Precomposition with the Unit.
There is an analogous operation of precomposition with the unit
$\Gamma \to \zc{\Gamma}$. Following <cit.>, we make
this a “silent” operation, i.e. it does not change the raw syntax
of the term or the type, only the typing derivation, as stated in
pre-unit. We refer to as use of the unit as “unzeroing” a
piece of the context, because variables that are marked/zeroed in the
context $\zc{\Gamma}$ in the premise become unmarked/unzeroed in the
conclusion.  The unit does not unmark the uses of the
variables in a term or type — a use $\zx$ of a marked variable
$\zx :: A$ from $\zc{\Gamma}$ (typed by var-zero, which is the
counit $\natural A \to A$) becomes a use $\zx$ of $x : A$ from
$\Gamma$ (typed by var-roundtrip, which is the roundtrip
$A \to \natural A \to A$, the counit precomposed with the
unit).  Thus, the unit can be silent because we
use the same syntax for the counit on marked variables as for the
roundtrip on unmarked variables.
var-roundtrip in the typing derivation.

To work up to the rule in the figure, the most basic form, where
$\Psi$ and $\Delta$ are empty, says that any
$\zc{\Gamma} \vdash a : A$ is also $\Gamma \vdash a : A$.  For the
same reasons as for the counit, we will need a tail telescope $\Delta$
that is not “unzeroed” by the operation (i.e. the marks in $\Delta$
in the premise are still there in the conclusion), for inductively
pushing this operation under bound variables, which are not unzeroed
(and indeed, might not even be marked in the premise). We will also
sometimes find it useful to unzero a variable in the middle of the
context, without unzeroing its prefix, e.g. going from
$\Gamma,\zx::A \vdash \judge$ to $\Gamma,x : A \vdash \judge$.
Semantically, this is precomposition with the unit $A \to \natural A$
paired with the identity substitution on $\Gamma$.
It is an implicit requirement for the judgement in the conclusion to
be well-formed that $\Psi,\Gamma,\Delta$ is a well-formed context

Precomposition with the Roundtrip.
Composing pre-unit and pre-counit, we have a rule
pre-roundtrip representing precomposition with the non-trivial
roundtrip $\Gamma \to \natural \Gamma \to \Gamma$.  (We have not seen a
use for a counit rule with a prefix $\Psi$ as in the unit rule, so we do
not include one, and consequently restrict the roundtrip to the setting
where both the unit and counit exist, when $\Psi$ is empty for the
unit.)  The section-retraction property of a bireflection states that
composing pre-unit and pre-counit in the other
direction, i.e. going from $\zc{\Gamma} \vdash a : A$ to $\Gamma \vdash
a : A$ to $\zc{\Gamma} \vdash \za : \zA$ should be the identity; because
the unit is silent, this is the same as the counit equation $\za \defeq

Returning to the rule var-roundtrip, the type $\zA$ in the
conclusion is typed by pre-roundtrip, because, as for the
counit, precomposing/substituting by the roundtrip on $\Gamma$
substitutes into the type $A$ as well.  Because variable uses $x : A$
and $\zx : \zA$ (in general) have different types, the marked-ness of a
variable usage cannot be naïvely flipped at will in a term. For
example, if $x : A$ then $\zx = x$ may not be well-formed, as $\zA$ is
not in general the same type as $A$.  The only reason that we do not
need to analogously mark the type $A$ in the conclusion of
$\rulen{var-zero}$ as $\zA$ is that the marked context extension
ctx-zero `pre-zeroes' the type — the type $A$ is in context
$\zc{\Gamma}$, so must already use only marked variables.

Well-formedness of the Conclusions.
Whenever we can form a term $\Gamma \yields a : A$, we of course want
that $\Gamma \ctx$ and $\Gamma \yields A : \univ$. (Depending on
precisely how the type theory is set up, these are sometimes
presuppositions of the term judgement; later when checking that
pre-counit and pre-unit are admissible in
Section <ref>, we follow <cit.> in
having them be consequences of the term judgement.) There are few
spots in the above rules where it is a bit subtle why these invariants
are maintained.  First, in var-zero, we have by
ctx-ext-zero that $\zc{\Gamma} \yields A : \univ$, but for the
use of $A$ on the right, we need $\Gamma,x:A,\Gamma' \yields A : \univ$.
In addition to the usual weakening with $x:A,\Gamma'$, this uses
pre-unit.  In var-roundtrip, we have
$\Gamma \yields A : \univ$, so by another application of
var-roundtrip, we also have $\Gamma \yields \zA : \univ$, so all
that is needed is the usual weakening.  In the definition of
$\zc{\Gamma}$ for unmarked variables, we begin with
$\Gamma \yields A : \univ$, and need $\zc{\Gamma} \yields \zA : \univ$,
which we have by pre-counit (with $\Delta$ empty).  In the
definition for marked variables, we start with
$\zc{\Gamma} \yields A :\univ$, and need
$\zc{\zc{\Gamma}} \yields A : \univ$ to apply ctx-ext-zero,
which holds by idempotence.  In the equation $\za \defeq a$, we need
the same equation on types to see that $\zA \defeq A$, and similarly
for the $\underline \za \defeq \za$ equation.

Substitution for Marked Variables.
There is a new case of standard substitution for substituting into
var-roundtrip, which is defined by

\[
\zx [a / x] :\defeq \za
\]

That is, when we substitute a term $a : A$ for a marked variable usage
$\zx$, the result is the marking of $a$.  This type checks for
$\Gamma,x:A \vdash \zx : \zA$ and $\Gamma \vdash a : A$ because the
pre-roundtrip rule gives $\Gamma \vdash \za : \zA$.
Semantically, $\zx$ is the roundtrip $A \to \natural A \to A$, and the
substitution post-composes this roundtrip with $a$; but $\za$ is $a$
pre-composed with the roundtrip $\Gamma \to \natural \Gamma \to
\Gamma$, and these are equal by naturality of the unit and counit.

A substitution principle for marked variables that is typical from other
comonadic type theories following <cit.> is

\[
\inferrule*[fraction={-{\,-\,}-}]
{\Gamma, \zx :: A, \Gamma' \yields b : B \and \zc{\Gamma} \yields a: A}
{\Gamma, \Gamma'[a/\zx] \yields b[a/\zx] : B[a/\zx]}
\]

Here, the term being substituted must already have all of its variables
marked, as indicated by the premise $\zc{\Gamma} \vdash a : A$ of the rule,
and this substitution principle is implemented by a syntactic
substitution, replacing $\zx$ with $a$ everywhere.  Given the admissible
rules in Figure <ref>, we can in fact define this by
first unzeroing the variable $\zx$ to get $\Gamma, x : A, \Gamma'
\yields b : B$ and then doing an ordinary substitution $b[a/x]$.  Since
all uses of $x$ will be marked $\zx$ in $b$ and $B$, this will replace
$\zx$ with $\za$ everywhere—but since $\zc{\Gamma} \yields a : A$, we have
$\za \defeq a$, so we get the same result as the more specialised
principle would have given.

We prefer this style of presenting substitution, where the substitution
for marked variables is given by unmarking and then ordinary
substitution, because it corresponds more closely to what we will do
when working informally in this type theory.  When performing
substitutions $b[a/x]$ by hand, we can simply look in $b$ for each
instance of $x$ and $\zx$ and replace them with either $a$ or $\za$
accordingly, without having to mentally keep track of the context
through each subterm to see whether $x$ is marked or not (variables that
are not marked become marked in the premises of some rules), as we would
have to do if substitution for a marked variable required pre-marking
the term.  This is another benefit of having var-zero and
var-roundtrip rules be identical raw syntax.  In our experience
trying different systems for this setting, this choice seems critical
for the usability of the system for informal type theory.

Comparison with Spatial Type Theory.
In spatial type theory <cit.>, there is also a
special context extension $x :: A$, which is a judgemental version of
extending the context with $\flat A$. Such variables are
called crisp. A usage of a crisp variable $x$ in a term
corresponds to a use of the counit $\flat A \to A$, like our
var-zero rule.  Because there is only a counit and not also a
unit, the type $A$ of a crisp variable $x :: A$ is only permitted to
depend on other crisp variables. A loose way to think about this is as
follows. Before we have access to any structural rules, dependency
forces us to apply modalities to an entire context at once. Given a
type-in-context $\Gamma \yields A : \univ$ presented as a fibration $p : A
\to \Gamma$, ordinary context extension corresponds to considering the
object $A$ as a context. If we want to make $A$ discrete, we have to
apply $\flat$ to everything, giving $\flat p : \flat A \to \flat
\Gamma$. So $\flat A$ can only depend on a discrete context, and the
judgemental version $x :: A$ has the same restriction.  Therefore, all
crisp variables must occur before regular ones, and the context
naturally divides into two zones.  In our system, however, the presence
of the unit map $A \to \natural A$ means that we can no longer neatly
divide the context in this way. For example, if we have a context $\zx
:: A, \zy :: B$, then we can precompose with the unit substitution just
on $\zx$, giving $x : A, \zy :: B$. This breaks the invariant that crisp
variables all occur before ordinary ones.

§.§ The $\natural$ type

\[
\inferrule*[left=$\natural$-form]{\zc{\Gamma} \yields A : \univ }{\Gamma
\yields \natural{A} : \univ} \\
\qquad
\inferrule*[left=$\natural$-intro]{\zc{\Gamma} \yields a : A}{\Gamma \yields a^\natural : \natural{A}} \and
\quad
\inferrule*[left=$\natural$-elim]{\Gamma \yields b : \natural A}{\Gamma \yields b_\natural : A} \\\\
\]

\[
\inferrule*[left=$\natural$-beta]{\zc{\Gamma} \yields a : A}{\Gamma \yields a^\natural{}_\natural \defeq a : A} \and
\quad
\inferrule*[left=$\natural$-eta]{\Gamma \yields b : \natural A}{\Gamma \yields b \defeq \zb{}_\natural{}^\natural : \natural A}
\]

Rules for $\natural$

Using this judgement structure, it is now simple to describe the
$\natural$ type using the rules in Figure <ref>.

Recall that we refer to a term/type in context $\zc{\Gamma}$, i.e. a
term/type all of whose free variables are marked, as dull.  The
formation rule says that for any dull type $A$ there is a type $\natural
A$.  Formally, this formation rule is analogous to $\sharp$ in spatial
type theory or dependent right adjoints <cit.>, in that it asks
for a type under the left adjoint of $\natural A$, which in this case is
also $\natural$, represented by $\zc{\Gamma}$.  One alternate rule that
one could imagine is like $\flat$ in spatial type theory, $\zc{\Gamma}
\vdash A : \univ$ implies $\zc{\Gamma} \vdash \natural A : \univ$.  However,
this rule breaks admissibility of precomposition with the unit, because
it forces variables in the conclusion's context to be marked.

The introduction rule says that for any dull term of a dull type $a : A$
there is a term $a^\natural : \natural A$, again transposing $\natural$
on the right to $\natural$ on the left (roughly, $\natural \Gamma \to A$
implies $\Gamma \to \natural A$). This is the same as the introduction
rule for $\sharp$ and dependent right adjoints.  Note that the type $A$
must be assumed to be dull for the type $\natural A$ in the conclusion
to be well-formed.

The elimination rule says that for any (not necessarily dull) term $b :
\natural A$, there is a term $b_\natural : A$.  Semantically, this is
the counit $\natural A \to A$ precomposed with $b$.  Note that the type
$A$ must be assumed to be dull for $\natural A$ in the premise to be
well-formed — for a non-dull type $A$, we have a counit $\natural \zA
\to \zA$, but in general we do not have a map $\natural \zA \to A$.

The computation or $\beta$-reduction rule says that
$a^\natural{}_\natural \defeq a$.  Whenever the left-hand side is
well-typed, the right-hand side is too, because of the silent unit rule
pre-unit. Note that $a$ is necessarily dull for the
$\natural$-intro rule to have been applied, and all of its free
variables are still marked zeroed on the right.

The uniqueness or $\eta$-rule says that $b \defeq
\zb{}_\natural{}^\natural$ for any term $b : \natural \zA$. Since $b$ is
not necessarily dull, it must be marked (precomposed with the counit)
before being used in the introduction rule $-^\natural$.  One must be
cautious in applying this rule from right to left, as not every possible
`unzeroing' of a term $\zb$ will be well-typed.

For a non-dull type $\Gamma \vdash A : \univ$, note that $\zA$ (given by
pre-counit) and $\natural \zA$ are very different.  In
parametrised pointed spaces/spectra, $\zA$ is $A$ with its dependency on
the fibres of the context $\Gamma$ replaced by the sections of $\Gamma$.
On the other hand, $\natural \zA$ also replaces the fibres of $A$ with
the trivial pointed space/spectrum.  For example, if $A$ is a closed
type then $\zA \defeq A \not \equiv \natural A$.
From this point of view, our notation $\zc{\Gamma}$ for marking a
context is confusing, because it semantically is $\natural \Gamma$;
however, we use this notation to emphasise that it is implemented by
“underlining all of the variables in $\Gamma$”.

We have not proved canonicity or normalisation for the $\natural$ type,
as our intended applications rely on many axioms, but we conjecture they
are true: the equations for $\zc{\Gamma}$ and $\za$ are proved rather
than asserted, and the $\natural$ type has a $\beta$ rule for weak head
reduction and a type-directed $\eta$ rule.

§.§ Alternative Rules Without Marked Context Extension

\[
\begin{array}{c}
\inferrule*[left=var-roundtrip]{~}{\Gamma, x : A, \Gamma' \yields \zx : \zA}
\qquad
\inferrule*[left=pre-roundtrip,fraction={-{\,-\,}-}]
{\Gamma \yields a : A}
{\Gamma \yields\za : \zA}
\qquad
\inferrule*
{\Gamma \yields a : A}
{\Gamma \yields \zc{\za} \defeq \za  : \zA}
\\\\
\inferrule*[left=$\natural$-form]{\Gamma \yields A : \univ }{\Gamma
\yields \natural{A} : \univ} \qquad
\qquad
\inferrule*[left=$\natural$-zero]{\Gamma \yields A : \univ }{\Gamma
\yields \natural{A} \defeq \natural{\zA} : \univ}
\\ \\
%% G |- A
%% N A [\eta] =? N (A [\epsilon][\eta]) [ \eta ]
%%   N (A [\epsilon][\eta]) [ \eta ]
%%   = N (A) [ N epsilon ] [ N eta ] [ \eta ]
%%   = N A [ eta ]
\inferrule*[left=$\natural$-intro]{\Gamma \yields a : A}{\Gamma \yields
a^\natural : \natural{A}}
\qquad
\inferrule*[left=$\natural$-elim]{\Gamma \yields b : \natural A}{\Gamma
\yields b_\natural : \zA}
\qquad
\inferrule*[left=$\natural$-beta]{\Gamma \yields a : A}{\Gamma \yields a^\natural{}_\natural \defeq \za : \zA}
\qquad
\inferrule*[left=$\natural$-eta]{\Gamma \yields b : \natural A}{\Gamma
\yields b \defeq b{}_\natural{}^\natural : \natural \zA \defeq \natural A}
\\\\
\end{array}
\]

Rules without marked context extension

As an alternative to the above rules, it is also possible to give rules
for $\natural A$ without marked context extension
$\rulen{ctx-ext-zero}$, which we show in
Figure <ref> (pre-roundtrip
needs to be generalized with a $\Delta$ like above, but we omit this
from the figure).

The idea with this variation is to have a judgemental account only of
the roundtrip idempotent, and not the object $\zc{\Gamma}$ that the
roundtrip splits through.  We still include the marked variable
uses (representing the roundtrip applied to a variable) and the
admissible operation of underlining terms $\za$ (representing
precomposition with the roundtrip on the context, so it does not change
the context).  The formation, introduction, and elimination rules are
essentially $\natural : \univ \to \univ$ and $-^\natural : A \to
\natural A$ and $-_\natural : \natural A \to \zA$.  The $\beta$ rule
says that the composite $A \to \natural A \to \zA$ is the roundtrip, and
the $\eta$ rule says that the composite $\natural A \to \zA \to \natural
A$ is the identity.  We explicitly include an equation $\natural A
\defeq \natural \zA$ because semantically these types should be equal
— in Figure <ref>, we only allow the latter to be
written, but that requires marked context extension to enforce.  The
$\eta$ rule requires $\natural A \defeq \natural \zA$ for both sides to
have the same type.

While the rules in Figure <ref>
are shorter to describe, we prefer the rules from
Figures <ref> and <ref> with marked
context extension for several reasons.  First, they do not require an
extra equation $\natural$-zero.  Second, when working informally
below, we will often assume a dull/marked variable $\zx :: A$, which has
the same meaning as assuming a variable $x : \natural A$, but using a
dull variable by writing $\zx$ is a bit terser than writing
$x_\natural$, and substitution does not need to go through a
$\beta$-reduction.  However, the main reason we prefer the marked
variables in the context is because they are necessary for future
work on adding the `smash product of spectra' as a tensor type,
as in linear logic.  The base of every type can be duplicated, so when
splitting the context to type check $c : C \vdash (a,b) : A \otimes B$,
we can e.g. allow a split into $c : C \vdash a : A$ and $\zc{c} :: \zC
\vdash b : B$, where one component receives all of $c$ and the other
receives only the base of $c$.  Presenting this nicely requires marked
variables in the context.

§ BASIC PROPERTIES OF $\NATURAL$

For the next several sections, we work in axiomatic
HoTT <cit.> (with $\Pi$, $\Sigma$, identity, and (higher)
inductive types, and univalent universes) with our new rules for
$\natural$.  First, we develop the basic structure of the $\natural$
type internally, proving that $\natural$ behaves like both the $\flat$
and $\sharp$ modalities of spatial type
theory <cit.>.

The introduction and elimination rules immediately give, for any type $A$, unit and counit maps

\begin{align*}
\eta_A :\defeq (\lambda x.\zx{}^\natural) &: A \to \natural \zA \\
\varepsilon_A :\defeq (\lambda n. n_\natural) &: \natural \zA \to \zA
\end{align*}

The fact that the we only have a counit for dull types is what
defeats the `no-go theorem' for comonadic modalities <cit.>. In general, there is no way to go from
a term of $\natural \zA$ or $\zA$ to a term of the non-zeroed type $A$.

The counit and unit are a section-retraction pair, i.e. the roundtrip $\eta_A \circ \varepsilon_A :
\natural \zA \to \zA \to \natural \zA$ is the identity.  The composite
$\varepsilon_A \circ \eta_A : A \to \natural \zA \to \zA$ is equal to
$\lambda x.\zx$.

For $n : \natural \zA$ we have

\[
\eta(\varepsilon(n)) \defeq \zc{n_\natural}^\natural \defeq \zc{n}_\natural^\natural \defeq n
\]

by the definition of $\zc{ }$ and the $\eta$-law.  For the composite on $x : \zA$, we get

\[
\varepsilon(\eta(x)) \defeq {\zx{}^\natural}_{\natural} \defeq \zx
\]

by the $\beta$-law.

We can define the functorial action of $\natural$ on a map, in any ambient context: given $f : A \to B$ we define $\natural \zf : \natural \zA \to \natural \zB$ by:

\begin{align*}
\natural f (x) :\defeq [\zf(\zx{}_\natural)]^\natural
\end{align*}

yielding a map $(A \to B) \to (\natural \zA \to \natural \zB)$.  When $f$ is $\lambda y.y$ we get

\[
\natural (\lambda y.y) (x) \defeq [\zc{(\lambda y.y)}(\zx{}_\natural)]^\natural \defeq
[(\lambda y.y)(\zx{}_\natural)]^\natural
\defeq
(\zx{}_\natural)^\natural \defeq x
\]

When $f$ is $f_2 \circ f_1$ we first have

\[
\natural (f_2 \circ f_1) (x) \defeq [\zc{(f_2 \circ f_1)}(\zx{}_\natural)]^\natural
\defeq [(\zc{f_2} \circ \zc{f_1})(\zx{}_\natural)]^\natural
\defeq [\zc{f_2}(\zc{f_1}(\zx{}_\natural))]^\natural
\]

But we also have

\[
(\natural (f_2) \circ \natural (f_1)) (x)
\defeq
\natural (f_2) ([\zc{f_1}(\zx{}_\natural)]^\natural)
\defeq
\defeq
\defeq
\]

So $\natural f$ preserves identity and composition definitionally.

Note that, in contrast with $\flat$ of spatial type theory, we do not need the function $f$ to be `crisp', i.e., only use modal variables. Here, we can turn any function $f : A \to B$ into a `crisp' one $\zf : \zA \to \zB$ by zeroing, allowing us to apply $\natural$-intro to $\zf(\zx{}_\natural) : \zB$.

The $\eta$-rule for $\natural \zA$ implies that any term of natural type
is equal to the marked version of it:

For any dull type $\zc{\Gamma} \vdash A : \univ$ and not necessarily
dull term $\Gamma \vdash a : \natural A$ there is a definitional
equality $\Gamma \vdash a \defeq \za : \natural A$

Suppose a term $\Gamma \vdash a : \natural A$.  By the $\eta$-rule, we
have $a \defeq {\za_\natural}^\natural$.  But applying the admissible
roundtrip rule pre-roundtrip, we have $\Gamma \vdash \za :
\natural A$ (using the fact that $\zA \defeq A$ because $A$ is dull).
Applying the $\eta$-rule to that gives $\za \defeq
{\zc{\za}_\natural}^\natural$. But $\underline{\zn} \defeq \zn$).

Semantically, this is because, for any $f : \Gamma \to \natural A$,
the composite with the roundtrip $\Gamma \to \natural \Gamma \to
\Gamma \to \natural A$ is still equal to $f$ — first, use naturality
of the unit/counit to see this is equal to $\Gamma \to \natural A \to
\natural \natural A \to \natural A$ and then the latter two maps are
inverse by idempotence of $\natural$.

The unit and counit are natural, so for any $f : A \to B$ the diagrams

A [r, "f"] [d, "η_A" swap]     B [d, "η_B"]

♮[r, "♮f" swap]     ♮

♮[r, "♮f"] [d, "ε_A" swap]     ♮[d, "ε_B"]

[r, "" swap]

On the left:
\[\zf((\za^\natural){}_\natural)^\natural \defeq \zf(\za)^\natural \defeq \zc{f(a)}^\natural \]

On the right:

\[ (\zf(\zx{}_\natural)^\natural)_\natural \defeq \zf(\zx{}_\natural) \defeq \zf(x{}_\natural) \]

We now consider types that are equivalent to their `underlying space'.

A type $A$ is modal if the unit $\eta_A : A \to \natural \zA$ is an equivalence. We define

\begin{align*}
\Modal &:\defeq \sm{X : \univ} \isEquiv(\lambda x. \zx{}^\natural)
\end{align*}

for the type of modal types.

This definition is studied in detail in <cit.>,<cit.>. In the intended model, the modal
types are the spaces, embedded in $P\Spec$ as a space equipped with the
constant zero family of spectra.  We will sometimes need to restrict
statements to such spaces, so it is important that we can carve out a
subuniverse of spaces using the modality.

If $A$ is modal then $\zA$ is also modal.

Given a witness $w :
\isModal(A)$, we have $\zw : \isModal(\zA)$, showing $\zA \equiv
\natural \zA$.

For any $A$, the type $\natural \zA$ is modal.

The counit $(\lambda z. z_\natural) : \natural \natural \zA \to \natural \zA$ is an inverse to the unit $(\lambda v. \zv{}^\natural) : \natural \zA \to \natural \natural \zA$.
Using Proposition <ref>,
for the roundtrip on $\natural \zA$  we have

\[\zv{}^\natural{}_\natural \defeq \zv \defeq v \]

and for the roundtrip on $\natural \natural \zA$ we have

\[\zc{z_\natural}{}^\natural \defeq \zz{}_\natural{}^\natural \defeq z.\]

Note that the unit and counit are not in general an equivalence between $\natural \zA$ and $\zA$ — the use of the $\eta$-law to prove $\zv \defeq v$ does not apply in $\zA$.  Intuitively, $\natural \zA$ is the base space of $\zA$, while $\zA$ itself only zeroes out the dependence of $A$ on the ambient context.  However, we do have:

A type $A$ is modal iff $(\lambda x. \zx) : A \to \zA$ is an equivalence.

Suppose $\lambda x.\zx : A \to \zA$ is an equivalence, with inverse $g
: \zA \to A$.  We show that $\eta_A$ is a quasi-equivalence, which can
be improved to an equivalence.  The inverse is $g \circ \varepsilon_A :
\natural \zA \to A$.  For $x:A$, we have

\[
g[(\zx^\natural)_\natural] \defeq g(\zx) = x
\]

using the inverse law for $g \circ (\lambda x.\zx)$.

For the other composite, let $(\lambda
x.\zx, g, w) : A \equiv \zA$, so that $w$ is the witness that $(\lambda
x.\zx)$ and $g$ are inverses. Now observe that $\zc {(\lambda
x.\zx, g, w)} : \zA \equiv \zA$ and by definition of
$\zc{\ }$, the maps are $\lambda x.\zx$ and $\zc{g}$, so
we also have $\zc{g} \circ (\lambda x.\zx) = \id_{\zA}$.
Then, for $y : \natural \zA$, the composite is

\[
\zc{g(y_\natural)}^\natural \defeq [\zg(\zy_{\natural})]^\natural
\defeq
((\lambda x.\zx^\natural) \circ \zg \circ (\lambda x:\zA.\zx)) (y_\natural)
(\lambda x.\zx^\natural)(y_\natural)
\defeq
\defeq
\]

Conversely, if $A$ is modal then $\zA$ is also modal by
Proposition <ref>.  By the $\beta$-law, the map
$(\lambda x.\zx) : A \to \zA$ is equal to the composite $\varepsilon_{A}
\circ \eta_A : A \to \natural \zA \to \zA$, which is the composite of
two equivalences.  First, $\eta_A$ is an equivalence because $A$ is
modal.  Second, $\varepsilon_{A}$ is an equivalence, because it is
left-inverse to $\eta_{\zA}$, which is an equivalence because ${\zA}$ is
modal, and a left-inverse of a map that is an equivalence is its

A dull type $\zA$ is modal iff $x = \zx$ for any $x : \zA$.

By function extensionality, $(\lambda x.x) = (\lambda x.\zx)$, and transporting the fact that the identity function is an equivalence along this allows us to use Proposition <ref>.

In the remainder of this section we show that $\natural$ has all the properties of both $\flat$ and $\sharp$ from spatial type theory.

§.§ Monadic Properties

We begin with the monadic properties; those shared with $\sharp$.  The
following characterises maps into $\natural \zA$ (from the
ambient context) via an induction principle, so we call it a “right”
universal property (even though the domain on the left of the $\Pi$ type
is what changes).  Below, we also consider a “left” universal
property, which characterises maps out of $\natural \zA$.

Suppose $P : \natural \zA \to \univ$ is a type family such that each $P(v)$ is modal. Given a dependent function $f : \prod_{x : A} P(\zx{}^\natural)$, there is $g : \prod_{v : \natural \zA} P(v)$ such that $g(\zx{}^\natural) = f(x)$ for all $x : A$.

Because each $P(v)$ is modal, we have inverses $r_v : \natural \zP(\zv) \to P(v)$. So it is enough to produce a function $g' : \prod_{v : \natural \zA} \natural \zP(\zv)$. Zeroing $f$ gives a function $\zf : \prod_{x : \zA} \zP(\zx{}^\natural)$, which we can use to define

\begin{align*}
g'(v) :\defeq \zf(\zv{}_\natural)^\natural
\end{align*}

and $g'(v)$ has type $\natural \zP(\zv{}_\natural{}^\natural) \defeq \natural \zP(\zv)$ as required. To get the goal function $g : \prod_{v : \natural \zA} P(v)$ we then post-compose with $r_v$:

\begin{align*}
g(v) :\defeq r_v(\zf(\zv{}_\natural)^\natural)
\end{align*}

This has the correct computation property:

\begin{align*}
g(\zx{}^\natural) \defeq r_v(\zf(\zx{}^\natural{}_\natural)^\natural) \defeq r_v(\zf(\zx{})^\natural) \defeq r_v(\zc{f(x)}{}^\natural) = f(x)
\end{align*}

as $r_v$ is an inverse of $(\lambda x. \zx^\natural)$.

Suppose $B : \natural \zA \to \univ$ is a type family with each $B(v)$ modal. Then precomposition with $\eta_A : A \to \natural \zA$ is an equivalence

\begin{align*}
\prd{v : \natural \zA} B(v)  \equiv \prd{x : A} B(\zx{}^\natural)
\end{align*}

The inverse is given by right $\natural$-induction (Proposition
<ref>), and the roundtrip on $f : \prd{x :
A} B(\zx{}^\natural)$ is exactly the $g(\zx^\natural) = f(x)$
equation given above.

For the other composite, suppose $h : \prd{v : \natural \zA} B(v)$,
and $y:\natural \zA$, and we need to show that $h(y)$ is equal to the
$g(y)$, for the $g$ determined by right $\natural$-induction on
$h$-precomposed-with-$\eta_A$, $\lambda x.h(\zx^\natural)$.
However, by the $\eta$-law, $y \defeq (\zy_\natural)^\natural$, so

\[
g(y) \defeq g((\zy_\natural)^\natural) = h((\zy_\natural)^\natural) = h(y)
\]

(This proof is morally doing another right $\natural$-induction to
reduce $y$ to something of the form $\zx^\natural$, but we have not
yet proved that $b =_{B(y)} b'$ is modal when $B(y)$ is modal, so we cannot
use Proposition <ref> directly, but instead
$\eta$-expand explicitly.)

$(\lambda A. \natural \zA) : \univ \to \univ$ with unit $\lambda x.\zx^\natural : A \to \natural \zA$ is a monadic modality in the sense of <cit.>.

The precomposition equivalence

\begin{align*}
\prd{v : \natural \zA} \natural \zB(\zv) \to \prd{x : A} \natural \zB(\zx{}^\natural)
\end{align*}

of the previous proposition, where $\natural \zB$ is modal by
Proposition <ref>, is precisely the
definition of a `uniquely eliminating modality' <cit.>, one of the several equivalent definitions of a
monadic modality.

Being a monadic modality has many formal consequences. In particular:

* $A$ is modal iff $(\lambda x. \zx^\natural) : A \to \natural \zA$ admits a retraction.

* If the input types are modal then all the following are modal:

1 A ×B x =_A y _f(x) B ×_A C A ≡B

* If $A$ is any type and $P : A \to \univ$ is such that every $P(x)$ is modal, then $\prd{x : A} P(x)$ is modal. If additionally $A$ is modal, then $\sm{x : A} P(x)$ is modal.

* For any types $A$ and $B$, the canonical map $\natural(\zA \times \zB) \to \natural \zA \times \natural \zB$ is an equivalence.

* If $A$ is a proposition, then so is $\natural \zA$.

Also like $\sharp$, the $\natural$ modality preserves $\Sigma$-types and is left-exact.

For types $A : \univ$ and $B : A \to \univ$, we have

\begin{align*}
\natural \left( \sm{x : \zA} \zB(x) \right) \equiv \sm{u : \natural \zA} \natural \zB(\zu{}_\natural)
\end{align*}

We know that the right-hand side is modal, so to define a map from left-to-right it is sufficient to provide $f : \sm{x : A} B(x) \to \sm{u : \natural \zA} \natural \zB(\zu{}_\natural)$ and then apply $\natural$-induction. For this we have $f(a, b) :\defeq (\za{}^\natural, \zb{}^\natural)$.

The other way, we are provided $u : \natural \zA$ and $v : \natural \zB(\zu{}_\natural)$, with which we can produce
\[(\zu{}_\natural, \zv{}_\natural)^\natural : \natural \left( \sm{x : \zA} \zB(x) \right).\]

To show the roundtrip on the left is the identity, suppose $v :
\natural \left( \sm{x : \zA} \zB(x) \right)$. By $\natural$-induction
($=_\natural$ is modal by Lemma <ref>) we
assume this is of the form $\zc{(a, b)}^\natural$, and then the round
trip is just

\begin{align*}
(\za{}^\natural{}_\natural, \zb{}^\natural{}_\natural)^\natural \defeq (\za, \zb)^\natural \defeq \zc{(a, b)}^\natural
\end{align*}

by the $\beta$-rule for $\natural$.

For the other roundtrip, starting with $(u, v) : \sm{u : \natural \zA} \natural \zB(\zu{}_\natural)$,
the computation rule for $\natural$-induction gives that the roundtrip is equal to

\begin{align*}
f(\zu{}_\natural, \zv{}_\natural) \defeq (\zu{}_\natural{}^\natural, \zv{}_\natural{}^\natural) \defeq (u, v)
\end{align*}

For $x, y : A$, there is an equivalence $(\zx{}^\natural = \zy{}^\natural) \equiv \natural(\zx = \zy)$ such that

[column sep = small]
(^♮= ^♮) [dd]

(x = y) [ur, "_(-)^♮"]  [dr, "(-)^♮" swap]

♮(= )

We can define maps both ways by:

\begin{align*}
c \mapsto \ap_{(\zc{-}){}^\natural}(c_\natural) : \natural(\zx = \zy) \to (\zx{}^\natural = \zy{}^\natural) \\
p \mapsto (\ap_{(-)_\natural}(\zp))^\natural : (\zx{}^\natural = \zy{}^\natural) \to \natural(\zx = \zy)
\end{align*}

For showing the roundtrip on $c : \natural(\zx = \zy)$ is the identity,
first, for any type $A$ with $x,y : A$ and $p : x =_A y$, we have
$\ap_{(\lambda x.\zx)}(\zp) = \zp$ as paths in $\zx =_{\zA} \zy$ (which type checks
because $\zc{\zx} = \zx$).  By path induction, it suffices to

\[
\ap_{(\lambda x.\zx)}(\zc{\refl{x}})
\defeq
\ap_{(\lambda x.\zx)}(\refl{\zx})
\refl{\zc{x}} \defeq \zc{\refl x}
\]

Then we have

\[
\defeq
\defeq
\defeq
\defeq
\]

The other direction is easier: the roundtrip on $p$ is:

\begin{align*}
&\ap_{(\zc{-})^\natural}(\ap_{(-)_\natural}(\zp)^\natural{}_\natural) \\
&\defeq \ap_{(\zc{-})^\natural}(\ap_{(-)_\natural}(\zp)) \\
&= \ap_{(\zc{-})_\natural{}^\natural}(\zp) \\
&\defeq \ap_{\id}(\zp) \\
&= \zp\\
&= p
\end{align*}

The last equality is by Lemma <ref> and that $p : (\zx{}^\natural = \zy{}^\natural)$ is a term of a dull modal type.

The triangle commutes by path-induction:

\begin{align*}
\ap_{(-)_\natural}(\ap_{(\zc{-}){}^\natural}(\refl{\zx}))^\natural
&= \ap_{(\zc{-})^\natural{}_\natural}(\refl{\zx}){}^\natural \\
&= (\refl{\zx}){}^\natural \\
&\defeq \zc{(\refl{x})}^\natural
\end{align*}

Left-exactness has some additional formal consequences outlined by <cit.>.

* $\natural$ preserves pullbacks, <cit.>.

* $\natural$ preserves $n$-types and more generally $n$-truncated maps for all $n$, <cit.>.

§.§ Comonadic Properties

Now we turn to the comonadic properties of $\natural$; the properties
it shares with the $\flat$ modality of spatial type theory. First, as
remarked in Section <ref>, we can derive a substitution
principle of dull terms for dull variables:

The dull substitution principle is

*[Left=dull-subst, fraction=- - -]
Γ, :: A ⊢c : C Γ ⊢a : A
Γ⊢c[a/] :c[a/x] : C[a/]

To see that this type checks, precompose with the unit on $A$ to get
$\Gamma, x : A \vdash c : C$ and the unit on $\Gamma$ to get $\Gamma
\vdash a : A$, and then a normal substitution $c[a/x]$ has type $C[a/x]
\defeq C[a/\zx]$.

Definition <ref> corresponds to the substitution
principle for crisp variables in spatial type theory, where a crisp
variable can be substituted by a term containing only crisp variables.
In our setting, given a term $a$ in a general context, we can mark it
and then substitute it for a dull variable:

*[fraction=- - -]
Γ, :: A ⊢c : C Γ⊢a : A
Γ⊢c[/] c[/x] : C[/]

Because $\zc{\Gamma} \vdash \za : A$ is a dull term, we can use
dull-subst.  This is equal to the ordinary substitution
$c[a/x]$ because all of the uses of $x$ in $c$ and $C$ must be marked,
so $a$ will be marked during substitution; we can prove inductively that

\[
\inferrule*[fraction={-{\,-\,}-}]
{\Gamma, \zx :: A \vdash c : C \and
{\Gamma} \vdash a : A}
{\Gamma \vdash c[\za/\zx] \defeq c[a/x] : C[\za/\zx]}
\]

A $\flat$-style eliminator is derivable for $\natural$:

*[Left=“$\flat$”-elim, fraction=- - -]Γ, x : ♮C : Γv : ♮Γ, :: c : C[^♮/x]Γ(vc) : C[v/x]

*[Left=“$\flat$”-beta, fraction=- - -]Γ, x : ♮C : Γ v : Γ, :: c : C[^♮/x]Γ(v^♮c) c[v/] : C[v^♮/x]

The eliminator can be derived by dull substitution:

\begin{align*}
(\flatstyleind{v}{\zu}{c}) :\defeq c[\zc{v}{}_\natural/\zu]
\end{align*}

which has type $C[\zc{v}{}_\natural{}^\natural/x] \defeq C[v/x]$ as required. The $\beta$-rule follows immediately from the $\beta$-rule for $\natural$, using the fact that
$\zv \defeq v$ for $\zc{\Gamma} \vdash v : A$, as all variable uses in $v$ are already marked.

This induction principle can be rephrased as a characterisation of maps
out of $\natural A$ (which we call a “left” universal property to
distinguish it from the characterisation of maps into $\natural A$
given in Theorem <ref>, though confusingly it is the
natural on the codomain that differs between the two sides).

For any $A, B : \univ$, post-composition (and functoriality of $\natural$) with $(-)_\natural : \natural \zB \to \zB$ induces an equivalence

\begin{align*}
\natural (\natural \zA \to \natural \zB) \equiv \natural (\natural \zA \to \zB)
\end{align*}

or more dependently, for $A : \univ$ and $B : \natural \zA \to \univ$, fibrewise post-composition (and functoriality of $\natural$) with $(-)_\natural : \natural \zB(\zv) \to \zB(\zv)$ yields an equivalence

\begin{align*}
\natural \left(\prd{v:\natural \zA} \natural \zB(\zv)\right) \equiv \natural \left (\prd{v:\natural \zA} \zB(\zv)\right)
\end{align*}

The counit map $\natural \zB(\zv) \to \zB(\zv)$ is always a section of the unit map, so the post-composition map in the statement of the Theorem is also a section.

We just have to check that the roundtrip on $\natural \left (\prd{v:\natural \zA} \zB(\zv)\right)$ is the identity. Suppose we have an $f : \natural \left (\prd{v:\natural \zA} \zB(\zv)\right)$. Unfolding the definition of post-composition and functoriality of $\natural$ with both the unit and the counit is:

\begin{align*}
(\lambda x. (\zf_\natural(\zx))^\natural{}_\natural)^\natural
&\defeq (\lambda x. (\zf_\natural(\zx)))^\natural \\
&\defeq (\lambda x. (\zf_\natural(x)))^\natural \\
&\defeq (\zf_\natural)^\natural \\
&\defeq f
\end{align*}

where $\zx \defeq x : \natural \zA$ by
Proposition <ref>. Note that $(\lambda
x. (\zf_\natural(x)))^\natural$ is well-typed, as $x$ is not free below
the $\natural$-intro, so does not need to be marked.

Because the rules for $\flat$ are derivable, we could instead have repeated the proof for $\flat$ verbatim, using $\mathsf{let}$-bindings, but the above is more direct.

One may wonder why the applications of $\natural$ are required around the two sides. Thinking syntactically, they are necessary to block access to `spectral' information from the context. Without $\natural$ on the right, one could use a $b : \zB$ in the context to form constant functions $\const_b : \natural \zA \to \zB$ which have no corresponding maps $\natural \zA \to \natural \zB$ on the left.

Another way to see that they are necessary is to consider the model in families of pointed types. There, it is clear that the map is not an equivalence without the $\natural$ present: $\upst (\natural \zA \to \natural \zB)$ is equivalent to the point in every fibre, but $\upst (\natural \zA \to \zB)$ may be non-trivial.

For any $A, B : \univ$ there is an equivalence

\begin{align*}
\natural (\zA \to \natural \zB) \equiv \natural (\natural \zA \to \zB)
\end{align*}

Combining the left and right universal properties we get

\begin{align*}
\natural (\zA \to \natural \zB) \equiv \natural (\natural \zA \to \natural \zB) \equiv \natural (\natural \zA \to \zB)
\end{align*}

In the presence of univalence, the type $\Modal \defeq \sm{A : \univ} \isModal(A)$ of modal types is modal.

We can use a simpler proof than the one for $\sharp$. By Corollary <ref>, we just have to show that for any $A : \univ$ and $w : \isModal(A)$, there is an equality $(A, w) = (\zA, \zw)$. And there is: by assumption $A$ is modal so $A \equiv \zA$, again by Corollary <ref>. In the second component, $\isModal(A)$ is a proposition, so we are done.

When working with inductive types in a theory with more structured contexts such as ours, one has make sure that the induction principles are strong enough. In spatial type theory, one needs to assert or prove `crisp induction principles', for when the motive of an elimination rule depends on a crisp variable of type being eliminated.  The crisp induction principle for a type constructor is a judgemental way of saying that the modality preserves the type constructor.  For example, crisp coproduct case analysis is a judgemental way of saying that $\flat(A+B) \equiv \flat A + \flat B$, because the crisp induction principle gives crisp variables of type $A + B$ the same universal property as an ordinary variable of type $\flat A + \flat B$.  In our setting, a dull induction principle for coproducts looks like:

*[left=dull-$+$-elim, fraction=- - -]Γ, :: + C :

Γ, :: p : C[()/] Γ, :: q : C[()/]

Γ s : + Γ(.C, .p, .q, s) : C[s/]

In spatial type theory, crisp induction principles are proven using the adjointness of $\flat$ and $\sharp$, and because $\natural$ is self-adjoint, we could repeat the proof almost verbatim. But we can show they are valid more directly, using the pre-counit and pre-unit rules.

With the above inputs, we can apply pre-unit to obtain

\begin{align*}
\Gamma, z : \zA + \zB &\yields C : \univ \\
\Gamma, x : \zA &\yields p : C[\inl(\zx)/z] \\
\Gamma, y : \zB &\yields q : C[\inr(\zy)/z] \\
\Gamma &\yields s : \zA + \zB
\end{align*}

Now note that $C[\inl(\zx)/z] \defeq C[\inl(x)/z]$ and $C[\inr(\zx)/z]
\defeq C[\inr(x)/z]$, because $z$ is only used marked in $C$, as in
Remark <ref>. These inputs are now of the right shape to
apply the ordinary $+$-elim rule.

Using an analogous construction, we can derive dull induction principles
for $\Idsym$-types, pushouts, etc.

Suppose $\zf : \zC \to \zA$ and $\zg : \zC \to \zB$ are dull functions between dull types. Then
\[\natural(\zA +_{\zC} \zB)  \equiv \natural \zA +_{\natural \zC} \natural \zB,\]
the pushout of $\natural \zf : \natural \zC \to \natural \zA$ and $\natural \zg : \natural \zC \to \natural \zB$.

Morally, this follows because we just proved that $\natural$ is a left adjoint, but we can also write out the maps explicitly as follows.

From left-to-right, we extract a term of $p : \zA +_{\zC} \zB$, and then do case analysis. On $a : \zA$, we have $\inl(\za^\natural) : \zA +_{\natural \zC} \natural \zB$. Similarly, on $b : \zB$ we have $\inr(\zb^\natural) : \zA +_{\natural \zC} \natural \zB$. To complete the cocone we have to to provide for any $c : \zC$, a path $\inl(\zf(\zc{c})^\natural) = \inr(\zg(\zc{c})^\natural)$ in $\natural \zA +_{\natural \zC} \natural \zB$. The glue constructor for the $\natural \zA +_{\natural \zC} \natural \zB$ pushout gives us a path

\begin{align*}
\glue(\zc{c}^\natural) : \inl(\natural \zf(\zc{c}^\natural)) = \inr (\natural \zg(\zc{c}^\natural))
\end{align*}

And this type is equal to $\inl(\zf(\zc{c})^\natural) = \inr (\zg(\zc{c})^\natural)$ by the definition of the functorial action of $\natural$, and the $\beta$-rule.

The right-to-left direction is similar. We begin with case analysis on $\zz$. On $n : \natural \zA$ and $m : \natural \zB$ we have $\inl(\zn_\natural) : \zA +_{\zC} \zB$ and $\inr(\zm_\natural) : \zA +_{\zC} \zB$ respectively. For any $o : \natural \zC$, we need a path $\inl(\natural \zf(\zo)_\natural) = \inr(\natural \zg(\zo)_\natural)$. Expanding the definition of functoriality and applying the $\beta$-rule, this is a path

\begin{align*}
\inl(\zf(\zo_\natural)) = \inr(\zg(\zo_\natural))
\end{align*}

and $\glue(\zo_\natural)$ is such a path in $\zA +_{\zC} \zB$. All together this produces a dull term of $\zA +_{\zC} \zB$, so applying $\natural$-intro we are done.

Checking the roundtrips are the identity is straightforward, using left $\natural$-induction and dull pushout induction, which can be derived as in Remark <ref>.

The sequential colimit (see e.g. <cit.>) of a sequence

\begin{align*}
A(0) \xrightarrow{a(0)} A(1) \xrightarrow{a(1)} A(2) \xrightarrow{a(2)} \dots
\end{align*}

is given by the higher inductive type $\colim A_n$ with point and path constructors

\begin{align*}
\iota &: \prd{n : \NN} A(n) \to \colim_n A_n \\
\kappa &: \prd{n : \NN} \prd{x : A(n)} \iota(n+1, a(n,x)) = \iota(n,x)
\end{align*}

Suppose we have a diagram

\begin{align*}
\zA(0) \xrightarrow{\za(0)} \zA(1) \xrightarrow{\za(1)} \zA(2) \xrightarrow{\za(2)} \dots
\end{align*}

of dull types and dull functions between them. Then
\[ \natural (\colim_n \zA(n)) \equiv \colim_n \natural \zA(n) \]

where the sequential colimit on the right is over the diagram

\begin{align*}
\natural \zA(0) \xrightarrow{\natural \za(0)} \natural A(1) \xrightarrow{\natural \za(1)} \natural \zA(2) \xrightarrow{\natural \za(2)} \dots
\end{align*}

The proof is analogous to that for pushouts.

Finally, we give compound rules for $\Pi x : \natural A.B$, which we
refer to as “dull $\Pi$-types”
(c.f. <cit.>, or the connective $A \to B$ in
linear logic as a fusion of $! A \multimap B$).

Dull $\Pi$-types are definable with

\[
\begin{array}{c}
\inferrule*{\zc{\Gamma} \vdash A : \univ \and
\Gamma,\zx::A \vdash B : \univ}
{\Gamma \vdash \prd{\zx::A} B : \univ}
\qquad
\inferrule*{\Gamma,\zx::A \vdash b : B}
{\Gamma \vdash \lambda \zx::A.b : \prd{\zx::A} B : \univ}
\qquad
\inferrule*{\Gamma \vdash f : \prd{\zx::A} B \and
\zc{\Gamma} \vdash a : A
{\Gamma \vdash f(a) : B[a/\zx]}
\\ \\
(\lambda \zx::A.b)(a) \defeq b[a/\zx]
\qquad\qquad
f : \prd{\zx::A} B \defeq \lambda \zx::A.f(\zx)
\end{array}
\]

Recall from Definition <ref> that dull substitution
$B[a/\zx]$ is syntactically just $B[a/x]$. We define

\[
\begin{array}{l}
\prd{\zx::A} B :\defeq \prd{y:\natural A} B[\zy_\natural/\zx]\\
\lambda \zx::A. b :\defeq \lambda y.b[\zy_\natural/\zx] \\
f(a) :\defeq f (a^\natural)
\end{array}
\]

The $\beta/\eta$ equations follow from the same for $\Pi$ and

§.§ Pointed Types

The modality also interacts nicely with pointed types and functions. Recall the following standard definitions:

A pointed type is a pair $(A, a)$ of a type $A$ and a term $a : A$. A pointed map from $(A, a)$ to $(B, b)$ is a function $f : A \to B$ and a path $p : f(a) = b$. Write $\univ_\star$ for the type of pointed types and

\begin{align*}
A \to_\star B :\defeq \sm{f : A \to B} f(a) = b
\end{align*}

for the type of pointed maps.

Note that a type or map being pointed is structure, not a property. However, it is common to abuse notation and write $A \to_\star B$ rather than $(A, a) \to_\star (B, b)$ when the points of $A$ and $B$ can be inferred from context.

If $B$ is modal then then $A \to_\star B$ is modal.

By Lemma <ref>, modal types are closed under
$\Sigma$, $=$ and $\Pi$ where the codomain is modal.

For any pointed type $(A, a)$, there are canonical points $\za : \zA$ and $\za^\natural : \natural \zA$ for which the unit $\eta_A : A \to \natural \zA$ and counit $\varepsilon_A : \natural \zA \to \zA$ are pointed maps.

Both are immediate from the definitions:

\begin{align*}
(\lambda x. \zx^\natural)(a) &\defeq \za^\natural \\
(\lambda n. n_\natural)(\za^\natural) &\defeq \za^\natural{}_\natural \defeq \za
\end{align*}

The following is a standard characterisation of equivalence between $\Sigma$-types:

Suppose we have type families $P : A \to \univ$ and $Q : B \to \univ$. If we have an equivalence $f : A \equiv B$ and a family of equivalences $g_x : P(x) \equiv Q(f(x))$ then the map

\begin{align*}
(\lambda (x,p). (f(x), g_x(p))) : \sm{x : A} P(x) \to \sm{y : B} Q(y)
\end{align*}

is an equivalence.

We have $\Sigma : (\Sigma A : \univ. A \to \univ) \to \univ$, and the given data is equivalent to $(A,P) =_{(\Sigma A : \univ. A \to \univ)} (B,Q)$ by univalence and the definitions of paths in $\Sigma$ and $\Pi$ types.

Let $(A, a)$ and $(B, b)$ be pointed types with $B$ modal. Precomposition with $A \to_\star \natural \zA$ induces an equivalence

\begin{align*}
(\natural \zA \to_\star B) \equiv (A \to_\star B)
\end{align*}

We have seen (Theorem <ref>) that there is an equivalence

\begin{align*}
w : (\natural \zA \to B)  \equiv (A \to B).
\end{align*}

So we need to show that for every $f : \natural \zA \to B$, there is an equivalence

\begin{align*}
(f(\za^\natural) = b) \equiv (w(f)(a) = b)
\end{align*}

but $w$ is precomposition with the unit, so the type on the right is also $(f(\za^\natural) = b)$.

For dull pointed types $(\zA, \za)$ and $(\zB, \zb)$, post-composition with $(-)_\natural : \natural \zB \to \zB$ induces an equivalence

\begin{align*}
\natural (\natural \zA \to_\star \natural \zB) \equiv \natural (\natural \zA \to_\star \zB)
\end{align*}

Because $\natural$ commutes with $\Sigma$ by
Proposition <ref>, we can again apply
Lemma <ref> so it is enough to show that the map

\begin{align*}
\sm{f : \natural (\natural \zA \to \natural \zB)} \natural (\zf_\natural(\za^\natural) = \zb^\natural) \equiv \sm {g : \natural(\natural \zA \to \zB)} \natural (\zg_\natural (\za^\natural) = \zb)
\end{align*}

induced by post-composition is an equivalence.

First, we know by Theorem <ref> that

\begin{align*}
w : \natural (\natural \zA \to \natural \zB) \equiv \natural (\natural \zA \to \zB)
\end{align*}

Explicitly, this is

\begin{align*}
w(f) \defeq (\lambda x. \zf_\natural(x)_\natural)^\natural
\end{align*}

So we need to produce for every $f : \natural (\natural \zA \to \natural \zB)$ an equivalence

\begin{align*}
\natural (\zf_\natural(\za^\natural) = \zb^\natural) \equiv \natural ((\zw(\zf))_\natural (\za^\natural) = \zb)
\end{align*}

On the right we calculate

\begin{align*}
(\zw(\zf))_\natural (\za^\natural) \defeq [(\lambda x. \zf_\natural(x)_\natural)^\natural]_\natural (\za^\natural) \defeq
(\lambda x. \zf_\natural(x)_\natural)(\za^\natural) \defeq
\zf_\natural(\za^\natural)_\natural
\end{align*}

And then we have

\begin{align*}
\natural (\zf_\natural(\za^\natural) = \zb^\natural)
&\defeq \natural ((\zf_\natural(\za^\natural))_\natural{}^\natural = \zb^\natural) && \text{(by the $\eta$-rule)} \\
&\defeq \natural ((\zw(\zf))_\natural{}(\za^\natural)^\natural  = \zb^\natural) && \text{(by the above calculation)}\\
&\equiv \natural ((\zw(\zf))_\natural (\za^\natural) = \zb) && \text{(by left exactness and idempotence)}
\end{align*}

One then has to check that this equivalence is the one that is induced by composition with the counit, but this follows from the definition of the left-exactness equivalence.

For any dull pointed types $A$ and $B$, there is an equivalence

\begin{align*}
\natural (\zA \to_\star \natural \zB) \equiv \natural (\natural \zA \to_\star \zB)
\end{align*}

By Proposition <ref> (where $\natural
\zB$ is modal by Proposition <ref>), $(\zA
\to_\star \natural \zB) \equiv (\natural \zA \to_\star \natural \zB)$.
Using univalence, $(\lambda X:\univ.\natural \zX)$ preserves equivalences, so we have

\[
\natural (\zA \to_\star \natural \zB) \equiv \natural (\natural \zA \to_\star \natural \zB)
\]

Then by Proposition <ref> we have
$\natural (\natural \zA \to_\star \natural \zB) \equiv \natural (\natural \zA \to_\star \zB)$.

§ REDUCED TYPES

Informally, the modal types $A \equiv \natural \zA$ studied above are
those with no synthetic spectral information—we think of
$\natural A$ as forgetting the spectra and replacing them with the
trivial one, so if $A$ is equivalent to $\natural \zA$, then $A$ had no spectral
information to begin with.  Dually, we can consider types with
only synthetic spectral information, which can be defined by
demanding that its underlying space is contractible.  In our intended
model, such a type corresponds to an individual spectrum indexed by the
point — finding the spectra among the parametrised families of spectra
as those families where the index space is trivial.  However, since the
type theory thus far admits more models than the main intended one, we
will refer to such a type as reduced rather than as “a
spectrum” (though when reading it can be helpful to substitute “a
spectrum” for “reduced” to gain intuition).  This is an instance of a
general definition: for any monadic modality $\bigcirc$, a
$\bigcirc$-connected type $A$ is one where $\bigcirc A$ is
contractible <cit.>, so a reduced type is a $\natural$-connected

A type $E$ is reduced if $\natural \zE$ is contractible.  We have

\begin{align*}
\Redu &:\defeq \sm{E : \univ} \isContr(\natural \zE)
\end{align*}

for the type of reduced types.

In the pointed spaces model of Section <ref>, the
reduced types are “synthetic pointed types”.  A reduced type $A$
has $\dnst A$ contractible, so $\upst A$ is just a single
type, and its section $\ptst A$ is just an element of $\upst A$.
Moreover, any function $f : A \to B$ for $A$ and $B$ reduced is a
“synthetic pointed map”—inside the type theory, we do not need to
carry around the data saying that $f$ preserves the point, but in the
pointed spaces model it will be interpreted as a function that
preserves the sections of $A$ and $B$, i.e. the points.

With reduced types/spectra in mind, we can clarify why the syntactic
property of a type $\zE$ being dull is not the same as it being
modal. Thinking of our intended model, the only spectrum (reduced type)
that is also a space (modal) is the point.  However, we can have a
non-trivial spectrum (reduced type) that is dull, which describes the
relationship of $\zE$ to the context—a dull spectrum is one
that only varies over the underlying space of the context.

In what follows, we will often say “For a dull …”, which
should be parsed formally as a dull $\Pi$ type $\prd{\zX::\ldots}
\ldots$ as in Definition <ref>.  In particular “For a dull
reduced type $\zE$ means $\prd{\zE :: \Redu}{\ldots}$, though we will
omit the projection of the type part and use $\zE$ directly as a type.
This means that proof that $\zE$ is reduced is dull, as well as the type

Any dull reduced type $\zE$ has a canonical point $\star_{\zE} : \zE$
given by the composite $1 \to \natural \zE \to \zE$, where the first map
is part of the data of $\natural \zE$ being contractible, and the second
is $\varepsilon_E$.

Any dull map $\zf : \zE \to \zF$ between dull reduced types is a pointed map in a canonical way.

In the diagram

[column sep=1em]
1 [dl] [dr]

♮[rr, "♮"] [d]        ♮[d]

[rr, "" swap]

the top triangle commutes by contractibility of $\natural \zF$, and the bottom square commutes by naturality of the counit, so we have a path equipping $\zf$ with the structure of a pointed map.

We can't show that this pointing of $\zf : \zE \to \zF$ is unique, but we can show that the underlying space of `$\zf$ is pointed' is contractible, i.e.  `$\zf$ is pointed' is itself reduced. Hence:

If $\zE$ and $\zF$ are dull reduced types then $\natural(\zE \to \zF) \equiv \natural(\zE \to_\star \zF)$.

We verify

\begin{align*}
\natural(\zE \to_\star \zF)
&\defeq \natural\left (\sm{f : \zE \to \zF} f(\star_{\zE}) = \star_{\zF} \right) \\
&\equiv \sm{f : \natural(\zE \to \zF)} \natural(\zf_\natural(\star_{\zE}) = \star_{\zF} ) && \text{(Proposition~\ref{prop:natural-preserves-sigma})} \\
&\equiv \sm{f : \natural(\zE \to \zF)} \zf_\natural(\star_{\zE})^\natural =_{\natural \zF} \star_{\zF}{}^\natural && \text{(Proposition~\ref{prop:natural-is-left-exact})} \\
&\equiv \natural(\zE \to \zF) && \text{($\natural \zF$ is contractible)}
\end{align*}

If $A$ is any type and $\zx : \natural \zA$ is a dull point of its base, the reduced type over $x$ is the type

\[ A_{\zx} :\defeq \sm{y : A} (\zx = \zy{}^\natural) \]

When $\zA$ is dull, ${\zA}_{\zx}$ is canonically pointed by $(\zx{}_\natural, \refl{\zx}) : \sm{y : A} (\zx = \zy{}^\natural)$.

$A_{\zx}$ is reduced.

We calculate:

\begin{align*}
\natural \left( \sm{y : A} (\zx = \zy{}^\natural) \right)
%&\equiv \sm{u : \natural \zA} \natural (\zx = (u_\natural)^0{}^\natural) \\
&\equiv \sm{u : \natural \zA} \natural (\zx = \zu{}_\natural{}^\natural) && \text{(Proposition~\ref{prop:natural-preserves-sigma})}\\
&\equiv \sm{u : \natural \zA} (\zx = \zu{}_\natural{}^\natural) && \text{($=_{\natural A}$ is modal by Proposition~\ref{lem:modality-consequences})}\\
&\defeq \sm{u : \natural \zA} (\zx = u)
\end{align*}

which is contractible.

This lets us internalise the idea that every type is a `space-valued family of spectra':

For any type $A$,

\[ A \equiv \sm{x : \natural \zA} A_{\zx}\]

Expanding $A_{\zx}$ on the right, and using the fact that $x = \zx$:

\begin{align*}
\sm{x : \natural \zA} \sm{y : A} (\zx = \zy{}^\natural) \equiv \sm{x : \natural \zA} \sm{y : A} (x = \zy{}^\natural)
\end{align*}

Interchange the $\Sigma$-types and then you have a contractible pair.

Reduced types are closed under many operations:

Reduced types are closed under $\Sigma$-types, identity types, pullbacks, pushouts, suspensions and loop spaces.

Closure under $\Sigma$, identity types and pullbacks holds for any lex
modality <cit.>. Closure under pushouts
follows from
Proposition <ref>. Suspension types and
loop spaces (defined via identity types) are special cases of pullbacks and pushouts.

Since a reduced type $E$ is a type, we can apply the ordinary higher
inductive suspension type constructor $\Sigma \zE$ to it, and
similarly, for an element $x:E$, form a loop space via the identity
type $\Omega(E,x) :\defeq x=_E x$.  Thinking of the reduced types as
spectra, these operations on types do turn out to correspond
semantically to the correct operations of suspension and loop space
on spectra.  This is because $\Spec$ is a full subcategory of
$P\Spec$, and the limits and colimits defining suspension and loop
space already land in $\Spec$, so they coincide with the limits and
colimits calculated in the subcategory.

A common abuse of notation is, for a pointed type $(X,x)$, to write
$\Omega X$ for the pointed type $(x =_X x, \refl{x})$, leaving $x$ to be
inferred from context.  Any dull reduced type $\zE$ is pointed by
$\star_{\zE}$ from Definition <ref>, and when we
write $\Omega \zE$ for a dull reduced type, $\star_{\zE}$ is the point
that should be inferred.

For dull reduced types $\zE$ and $\zF$, suspension and loop space are dull adjoints, i.e.

\[
\natural(\Sigma \zE \to \zF) \equiv \natural(\zE \to \Omega \zF)
\]

By Proposition <ref>, it is equivalent to show

\[
\natural(\Sigma \zE \to_\star \zF) \equiv \natural(\zE \to_\star \Omega \zF)
\]

so this follows by functoriality of $\natural$ from the fact that
suspension and loop space are adjoint for (general) types and pointed
maps <cit.>.

§.§ Synthetic Stabilisation

We now have defined the modal types, i.e. the spaces (in the intended
model in $P\Spec$), and the reduced types, i.e. the spectra.  One
important feature of spectra that we would like to capture synthetically
is an adjunction relating these:

[row sep = 4em, column sep = 4em]
(spectra)[d, bend left=30, "Ω^∞"]

_⋆ (spaces) [u, bend left=30, "Σ^∞"] [u, phantom, "⊣"]

The $\Sigma^\infty$ operation `freely stabilises' a pointed modal
type. Once we have imposed some axioms, we will find that the homotopy
groups of the reduced type $\Sigma^\infty X$ correspond to the stable
homotopy groups of the modal type $X$.

Recall from the introduction that the $\infty$-category of spectra may
be defined as the limit

\begin{align*}
\Spec = \varprojlim \left(  \cdots \xrightarrow{\Omega} \mathcal{S}_* \xrightarrow{\Omega} \mathcal{S}_* \xrightarrow{\Omega} \mathcal{S}_* \right)
\end{align*}

and that spectra can presented concretely as a sequence of pointed
spaces $X_0,X_1,\ldots$ with $X_0 \equiv \Omega X_1$,
$X_1 \equiv \Omega X_2$, ….  Then $\Omega^\infty$ sends a
spectrum to the space $X_0$.  It is named $\Omega^\infty$ as we have
`applied $\Omega$ infinitely many times' to reach the end of the
limit.  The left adjoint $\Sigma^\infty$ sends a space $X$ to the
spectrification of its suspension pre-spectrum (see
Section <ref> below), i.e. we can make a sequence of pointed
spaces $X, \Sigma X, \Sigma \Sigma X, \ldots$ with maps
$X \to_\star \Omega \Sigma X$,
$\Sigma X \to_\star \Omega \Sigma \Sigma X$ …given by the unit
of the $\Sigma \dashv \Omega$ adjunction. These maps are not
equivalences, which is corrected by replacing each space by a certain
colimit, a process called spectrification.

Here, we instead define an abstract/synthetic variant of this
adjunction, which can be interpreted in this way in $P\Spec$.  We will
do so by assuming the existence of a distinguished reduced type $\sphere
: \Redu$. Note that $\sphere$ is a closed type, so is dull. In our
intended model this will be interpreted as the sphere spectrum
(i.e. $\Sigma^\infty S^0$) living over the point.  In this section, we
will use the notation $\sphere$ and $\Sigma^\infty/\Omega^\infty$
because of the intended interpretation in $P\Spec$, but these will be
abstract operations that exist in any model (up to the choice of

Using $\sphere$, we define $\Omega^\infty$ as follows:

For $\zE : \Redu$, define the modal type

\begin{align*}
\Omega^\infty \zE :\defeq \natural(\sphere \to \zE)
\end{align*}

which is pointed by the constant zero map
$(\lambda \_. \star_{\zE})^\natural$.

To gain intuition for why this is the right definition, we can
consider the pointed spaces model of Section <ref>. The analogue of $\sphere$ there
is $\mathbb{B}$, the two-point space $S^0$ living over the
point. The base of the function type $\mathbb{B} \to \zE$ is
equivalent to the type of all basepoint preserving maps from the
upstairs of $\mathbb{B}$ to the upstairs of $\zE$. The basepoint is
fixed, and there is one free point that can be mapped to any point
of the upstairs $\zE$. So the base space of $\mathbb{B} \to \zE$
indeed corresponds to the upstairs of $\zE$.

For spectra, similar reasoning applies, using the
$\Sigma^\infty \dashv \Omega^\infty$ adjunction more explicitly, and
that the sphere spectrum is the stabilisation of the two-point space:

\begin{align*}
\mathrm{Map}_{\Spec}(\sphere, E) \equiv \mathrm{Map}_{\Spec}(\Sigma^\infty S^0,  E) \equiv \mathrm{Map}_{\mathcal{S}_\star}(S^0, \Omega^\infty E) \equiv \mathrm{Map}_{\mathcal{S}}(1, \Omega^\infty E) \equiv \Omega^\infty E
\end{align*}

So we take `$\mathrm{Map}_{\Spec}(\sphere, E)$' as our definition of $\Omega^\infty E$.

One application of $\Omega^\infty$ is defining the homotopy groups of a spectrum, in the sense that is used in stable homotopy theory:

The $\sphere$-shifted homotopy groups of a reduced type $\zE$ are defined by

\begin{align*}
\pi^s_n \zE :\defeq \pi_n(\Omega^\infty \zE)
\end{align*}

Simply calculating $\pi_n(\zE)$ will not do the correct thing: we will
see later that, after imposing a stability axiom
(Section <ref>), reduced types are
$\infty$-connected <ref>, so $\pi_n(\zE) \equiv
1$ always.

The left adjoint $\Sigma^\infty \dashv \Omega^\infty$ then has a surprisingly simple formula:

For $X$ a pointed modal type, define $\Sigma^\infty X :\defeq X \topsmash \sphere$.

This is left adjoint roughly because maps of reduced types are pointed
maps, and $- \topsmash A \dashv A \to_\star -$ for any $A$.

First, we check that $\Sigma^\infty$ lands in reduced types:

For any modal type $X$, $\Sigma^\infty X$ is reduced.

The pushout diagrams defining $X \vee \sphere$ and $X \topsmash \sphere$

1 [d] [r] [dr, phantom, "⌜", very near end]     X [d]

[r]     X ∨

X ∨[d] [r] [dr, phantom, "⌜", very near end]     X ×[d]

1 [r]     Σ^∞X

Because $\natural$ preserves pushouts by
Proposition <ref> and products
by Proposition <ref>, and $\sphere$ is
reduced, so $\natural \sphere \equiv 1$, we can calculate

1 [d] [r] [dr, phantom, "⌜", very near end]     ♮[d]

1 [r]     ♮(∨) ≡♮

♮[d] [r] [dr, phantom, "⌜", very near end]     ♮[d]

1 [r]     ♮(Σ^∞) ≡1

because the top of the second diagram is the identity, and the pushout
of a map along the identity is the same map.

$\Sigma^\infty$ and $\Omega^\infty$ are (dull) adjoints: there is an equivalence
\[\natural (\Sigma^\infty \zX \to \zE) \equiv (\zX \to_\star \Omega^\infty \zE)\]
where $\zX$ is a pointed modal type and $\zE$ is reduced.

\begin{align*}
\zX \to_\star \Omega^\infty \zE
&\defeq (\zX  \to_\star \natural(\sphere \to_\star \zE)) \\
&\equiv \natural(\zX \to_\star \natural(\sphere \to_\star \zE)) &&(- \to_\star \natural - \text{ is modal })\\
&\defeq \natural(\natural \zX  \to_\star (\sphere \to_\star \zE)) && (\text{Proposition~\ref{prop:pointed-self-adjoint}})\\
&\equiv \natural(\zX  \to_\star (\sphere \to_\star \zE)) && \text{($\zX$ modal)} \\
&\equiv \natural(\zX  \topsmash \sphere \to_\star \zE) \\
&\defeq \natural(\Sigma^\infty \zX  \to_\star \zE) \\
&\equiv \natural(\Sigma^\infty \zX  \to \zE) && (\text{Proposition~\ref{prop:spectra-map-is-pointed}, Proposition~\ref{prop:sigmainf-reduced}})
\end{align*}

Here we use currying for pointed maps $A \to_\star (B \to_\star C)
\equiv (A \topsmash B) \to_\star C$, which has been proved in type theory <cit.>.

In the pointed spaces model, for a pointed modal type $X$,
$X \topsmash \mathbb{B}$ works out to be $\dnst \zX \topsmash 1$ in the
base (which is indeed contractible). Over this point, we are
calculating the cofibre of the map

\[ X + 1 \equiv X \wedge S^0 \to X \times S^0 \equiv X + X \]
is the identity on the first component $X$ and the basepoint
inclusion on the second. So the first copy of $X$ is crushed to a
point, and identified with the basepoint of the second copy of $X$.

In all, the operation takes a pointed modal type $X$ to a reduced
type $\Sigma^\infty X$, moving $X$ from the base to the fibre,
internalising the analytic pointing as synthetic pointing.

In $P\Spec$ we have to work a little harder to justify this
definition. $\Sigma^\infty$ is a functor from pointed spaces to
spectra, but we can precompose with the functor
$(-)_+ : \mathcal{S} \to \mathcal{S}_*$ to get a functor from
unpointed spaces. This is typically written
$\Sigma^\infty_+ : \mathcal{S} \to \Spec$, and is left adjoint to
the functor given by computing the pointed space $\Omega^\infty$ and
forgetting the basepoint.

As a left adjoint, $\Sigma^\infty_+$ preserves colimits, and because
every space is the colimit of its points, we calculate

\[ \Sigma^\infty_+(X) \equiv \Sigma^\infty_+(\colim_X 1) \equiv
\colim_X \Sigma^\infty_+(1) \equiv \colim_X \Sigma^\infty(S^0)
\equiv \colim_X \sphere \]

I.e., the colimit of the constant diagram on $X$ at $\sphere$. For
us, such a constant diagram is given by the parametrised spectrum
$X \times \sphere$, placing a copy of $\sphere$ over every point in
$X$. The desired colimit can be computed as the cofibre of
$X \to X \times \sphere$ which is the basepoint in the second
component, crushing the base $X$ to a point. We can take this as our
type-theoretic definition of $\Sigma^\infty_+$:

\[ \Sigma^\infty_+(X) :\defeq \cofib(X \to X \times \sphere) \]

To get back to $\Sigma^\infty(X)$ for $X$ a pointed type, we have to
crush the `extra copy of $\sphere$' that was added over the new
basepoint: this is now taking the cofibre of the composite
$\sphere \to X \times \sphere \to \Sigma^\infty_+ X$ which is the
basepoint in the first component. Combining the two cofibre
diagrams, in all we have calculated the smash product
$X \topsmash \sphere$.

§.§ Commutativity of the Adjunctions

So far, we have seen that we have the three adjunctions in the following
diagram (the two vertical sides are the same):

[row sep = 4em, column sep = 4em]
_⋆[r, bend left=15, "Σ"] [d, bend left=20, "Σ^∞"] [r, phantom, ""] [d, phantom, "⊢"]      _⋆[l,bend left=15,"Ω"] [d,bend left=20, "Σ^∞"] [d, phantom, "⊢"]

[r, bend left=15, "Σ"] [u, bend left=20, "Ω^∞"] [r, phantom, ""]     [l,bend left=15, "Ω"][u,bend left=20, "Ω^∞"]

We can also show that the diagram commutes.

In pointed spaces it is clear this should be true, as the
$\Sigma^\infty \dashv \Omega^\infty$ adjunction simply moves pointed
spaces into the fibre over a point and back, and the suspension/loop
space of a reduced type is calculating the suspension/loop space of
the unique fibre.

For spectra, consider a spectrum again presented as a sequence of
pointed spaces $(E_0, E_1, \dots)$. The loop space of such an
$\Omega$-spectrum can be calculated by shifting the spaces over by
one, giving $\Omega$-spectrum $(\Omega E_0, E_0, E_1, \dots)$, so
extracting the $0$th space commutes with calculating the loop space.

The suspension of an $\Omega$-spectrum can be calculated by shifting
the spaces the other way, giving $(E_1, E_2, \dots)$.  Leaving aside
spectrification briefly, $\Sigma^\infty X$ is given by the
prespectrum $(X, \Sigma X, \Sigma^2 X, \dots)$, so
$\Sigma^\infty \Sigma X \defeq (\Sigma X, \Sigma^2 X, \dots)$ is
exactly $\Sigma^\infty X$ shifted by one.

$\Omega^\infty$ commutes with the ordinary loop space operation $\Omega$:

\begin{align*}
\Omega^\infty \Omega \zE \equiv_\star \Omega \Omega^\infty \zE
\end{align*}

naturally in $\zE$.

Note that the left-hand side is the loop space on reduced (and therefore
pointed) types, while the right-hand side is the loop space on pointed
modal types, but both are implemented by the usual loop space on types.

This is easy, after the following basic fact about loop spaces.

For any pointed types $A$ and $B$,

\[(A \to_\star \Omega B) \equiv_\star \Omega(A \to_\star B) \]

naturally in $B$.

\begin{align*}
(A \to_\star \Omega B) &\equiv_\star (A \to_\star (S^1 \to_\star B)) \\
&\equiv_\star (S^1 \to_\star (A \to_\star B)) \\
&\equiv_\star \Omega(A \to_\star B)
\end{align*}

The first equivalence is essentially the universal property of the
higher inductive circle $S^1$, while the second follows from exchange
for function types.

\begin{align*}
\Omega^\infty \Omega \zE \defeq \natural(\sphere \to_\star \Omega \zE) \equiv_\star \natural (\Omega(\sphere \to_\star \zE)) \equiv_\star \Omega\natural (\sphere \to_\star \zE) \defeq  \Omega \Omega^\infty \zE
\end{align*}

For any pointed type, $\natural \Omega(A,a) \equiv_\star \Omega(\natural A,\za^\natural)$ follows from
Proposition <ref>.

In the other direction, we have:

$\Sigma^\infty$ commutes with $\Sigma$:

\begin{align*}
\Sigma \Sigma^\infty X \equiv \Sigma^\infty \Sigma X
\end{align*}

naturally in $X$.

First, some properties of the suspension and smash higher inductive
types in ordinary homotopy type theory are that
$\Sigma X \equiv S^1 \topsmash X$ <cit.> and smash is
associative <cit.>.  Thus, we can

\[\Sigma \Sigma^\infty X \defeq \Sigma(X \topsmash \sphere) \equiv S^1 \topsmash (X \topsmash \sphere) \equiv (S^1 \topsmash X) \topsmash \sphere \equiv \Sigma^\infty \Sigma X \]

§ STABILITY

Classically, the category of spectra has a number of special
properties, including a zero object, biproducts (products and
coproducts that are isomorphic), any pushout square is a pullback
square and vice versa, and suspension and loop space are inverse (not
only adjoint).  Thus far, our definition of synthetic spectra as
reduced types (dully) has a zero object: $1$ is initial as well as
terminal because $\natural(1 \to \zE) \equiv \natural(\zE) \equiv 1$.
To establish the other properties, it turns out to suffice to add an
apparently weaker axiom asserting that products and coproducts in
$\Redu$ coincide—we will show that this implies stability in the
sense of pullback and pushout squares coinciding, which in turn
implies that suspension and loop space are an equivalence.

Reduced types are pointed, so the coproduct in the category of reduced
types is actually the wedge $\vee$.  For any pointed types $A$ and $B$
there is a canonical wedge inclusion
$\iota_{A,B} : A \wedge B \to A \times B$.

Axiom S (for Stable)

For any dull reduced types $\zE$ and $\zF$, the wedge inclusion $\iota_{\zE,\zF} : \zE \wedge \zF \to \zE \times \zF$ is an equivalence.

Unfolding the informal use of dull $\Pi$-types,
(Proposition <ref>), this is asserting the existence of
a term

\begin{align*}
\mathsf{ax}_S : \prd{E : \natural \Redu} \prd{F : \natural \Redu} \isEquiv(\iota_{E_\natural, F_\natural})
\end{align*}

Some care has to be taken when devising an internal version of the external fact that the subcategory $\Spec \hookrightarrow P\Spec$ is stable. The obvious thing to try is an an axiom that applies to any reduced type. The issue is that when asserting the existence of a closed term, like the axiom above, the term can be weakened to any ambient context.

Semantically, this means we have to consider whether the axiom holds in all slice categories $P\Spec/\Gamma$. In our situation, it does not. A reduced type in $P\Spec/\Gamma$ consists of a family of spectra $E$ over the base of $\Gamma$, together with spectrum maps between the fibres of $E$ and the corresponding fibres of $\Gamma$. This category is not stable in general, as it lacks a zero object (among other things). If the context $\Gamma$ itself consists of a single spectrum $F$, then the existence of a zero object would imply that any map $E \to F$ splits.

The axiom does hold in $P\Spec/X$ when $X$ is a space, as reduced types in $P\Spec/X$ are exactly the families of spectra over $X$, comprising a stable category. Syntactically this requirement corresponds to having a dull context, hence the restriction to types in $\natural \Redu$ in Axiom S.

We can weaken our $\mathsf{ax}_S$ to an arbitrary context $\Gamma$ and still be safe, as the spectra $E_\natural$ and $F_\natural$ will only depend on the underlying space of $\Gamma$.

This axiom rules out the pointed spaces model, as the wedge and product of reduced types in that model correspond to the ordinary wedge and product of the pointed types in the unique fibre. But it doesn't rule out the trivial model where $\natural$ is the identity functor. There, the only reduced type is the point, and the wedge inclusion $1 \wedge 1 \to 1 \times 1$ is certainly an equivalence.

For two dull reduced types $\zE$ and $\zF$, the smash product $\zE
\topsmash \zF$ and the join $\zE \join \zF$ are both contractible.

Recall that the smash product $\zE \topsmash \zF$ is the cofibre of the wedge inclusion, i.e. the pushout

\[
\begin{tikzcd}
\zE \vee \zF \ar[d] \ar[r] \arrow[dr, phantom, "\ulcorner", very near end] & \zE \times \zF \ar[d] \\
1 \ar[r] & \zE \topsmash \zF
\end{tikzcd}
\]

Axiom S asserts that the top map is an equivalence, so the
bottom-right corner is equivalent to the bottom-left.  For the join,
we have $\zE \join \zF \equiv \Sigma(\zE \topsmash \zF)$
by <cit.>, and the suspension of a
contractible type is contractible.

Here, $\zE \topsmash \zF$ is the smash product of types, which
does not correspond to the `smash product of spectra', an important
operation in stable homotopy theory.

Next, we show that Axiom S indeed makes pullbacks and pushouts in
$\Redu$ coincide, mainly as a consequence of the Little Blakers-Massey
Theorem <cit.>.  As a first step:

For any pointed type $A$, there is a pullback square

ΣΩA [d] [r]     A ∧A [d, "ι"]

A [r, "Δ" swap]     A ×A

where the map on the left is the counit of the $\Sigma \dashv \Omega$ adjunction.

This will follow quickly from the following consequence of descent for pushouts:

Consider a commuting cube of types

S' [dl] [dr] [d]

A' [d]     S [dl] [dr]     B' [dl,crossing over] [d]

A [dr]     X' [d] [from=ul,crossing over]     B [dl]

and suppose the vertical squares are pullback squares. Then the commuting square

A' ⊔_S' B' [r] [d]     X' [d]

A⊔_S B [r]     X

is a pullback square.

Consider the commutative cube

ΩA [dl] [dr] [d]

1 [d]     1[dl] [dr]     1 [dl,crossing over] [d]

A [dr]     A [d] [from=ul,crossing over]     A [dl]

A ×A,

where the vertical map $A \to A \times A$ is the diagonal, and the maps $A \to A \times A$ on the left and right are the identity on one component and constant at the point on the other. All of the vertical squares are pullbacks.

Now note that the pushout of the top span is $\Sigma \Omega A$, and the
pushout of the bottom span is $A \wedge A$, so by the above theorem we
have the desired pullback square (with the top/left bottom/right maps
swapped, but pullbacks are symmetric in the sense that $A \times_C B
\equiv B \times_C A$).

For any dull reduced type, the canonical map $\Sigma \Omega \zE \to \zE$ is an equivalence.

By Lemma <ref>, this map is the pullback
of the wedge inclusion $\iota$ along $\Delta$.  By Axiom S, $\iota$ is
an equivalence, and the pullback of an equivalence along any map is an

Recall <cit.> that a type $A$ is $n$-connected if its
$n$-truncation is contractible, and a map is $n$-connected if its fibre is
an $n$-connected type for all base points.  A type or function is
$\infty$-connected if it is $n$-connected for every $n$.

We will use the following Lemmas about $n$-connected types:

Suppose that a type $A$ is 0-connected and $P : A \to \mathsf{Prop}$ is a family
of propositions ($-1$-types).  Then if $P(a)$ holds for some $a:A$, then
$P(a')$ holds for all $a'$.

Assume an $a$ such that $P(a)$ and another point $a'$.  Since $A$ is
0-connected, its 0-truncation is contractible, and therefore its
0-truncation is a proposition <cit.>, so we
get a path $|a'| =_{\trunc{0}{A}} |a|$. Commuting the truncation
with the loop space gives $\trunc{-1}{a' = a}$ <cit.>.  That is, $a'$ is merely equal to $a$.  But
$P(a')$ is a proposition by assumption, so to prove it, we can
assume $a' = a$, and then transport the assumed proof of $P(a)$.

* If $A$ and $B$ are $0$-connected then so is $A \times B$

* If $A,B$ are $0$-connected and $C$ is $1$-connected, then for
any maps $f : A \to C$ and $g : B \to C$, the pullback $A \times_C
B$ is $0$-connected.

For the first part, truncation preserves products <cit.>, so to show $\trunc{0}{A \times B}$ is
contractible, we can equivalently show that
$\trunc{0}{A} \times \trunc{0}{B}$ is contractible.  But
$\trunc{0}{A}$ and $\trunc{0}{B}$ are contractible by assumption,
and $1 \times 1 \equiv 1$.

For the second, the pullback is given by the type
$\sm{(x,y):A \times B} f(x) =_{C} g(y)$.
By <cit.>, we have

\begin{align*}
& \trunc{0}{\sm{(x,y):A \times B} f(x) =_{C} g(y)} \\
& \equiv \trunc{0}{ \sm{(x,y):A \times B} \trunc{0}{f(x) =_{C} g(y)}   }\\
& \equiv \trunc{0}{ \sm{(x,y):A \times B} |f(x)| =_{\trunc{1}{C}} |g(y)| }\\
& \equiv \trunc{0}{A \times B} \\
& \equiv 1
\end{align*}

The second-to-last step is because $\trunc{1}{C}$ is contractible by assumption, so any identity type in it is as well,
and the last step is by the previous part, since $A$ and $B$ are 0-connected.

Dull reduced types and dull maps between them are $\infty$-connected.

For types, we prove by induction on $n$ that every dull reduced type
$\zE$ is $n$-connected.  Every type is $(-2)$-connected, since the
$(-2)$-truncation is contractible by definition.  For the inductive step,
suppose $\zE$ is reduced, and we want to show that it is
$(n+1)$-connected.  Then $\Omega \zE$ is also reduced by
Proposition <ref> and dull, so by the
inductive hypothesis (which applies to all dull reduced types, so in
particular $\Omega \zE$) it is $n$-connected.  Suspension increases
connectivity by 1 <cit.>, so $\Sigma \Omega \zE$ is
$(n+1)$-connected.  But by Corollary <ref>,
$\zE \equiv \Sigma \Omega \zE$, so $\zE$ is $(n+1)$-connected as well.

Now for maps, fix an $n$.  The fibre of a dull map $\zf : \zE \to \zF$
over the basepoint is the type $\fib_{\zf}(\star_{\zF}) := \sm{x : \zE}
\zf(x) = \star_{\zF}$, which is a dull reduced type and thus is an
$\infty$-connected type by above, and therefore $n$-connected.  We now
show that this implies that all fibres are $n$-connected using
Lemma <ref>.  First, $\zF$ is a dull reduced type, and
thus by the previous part it is in particular 0-connected.  For any type
$A$, the type “$A$ is $n$-connected” is a proposition, because it
unfolds to “the $n$-truncation of $A$ is contractible”, and being
contractible (like all h-levels) is a proposition <cit.>.  Thus, $\fib{\zf}(\star_{\zF})$ being $n$-connected
implies the same for any basepoint $x : \zF$, so $\zf$ is an
$n$-connected map.

We will now make use of the Little Blakers-Massey Theorem and its dual, which is the specialisation of the Generalised Blakers-Massey Theorem <cit.> to the identity modality. The Generalised Theorem has been formalised in The HoTT Library <cit.>. First, some notation:

For $f : A \to B$, let $\Delta f$ denote the canonical map $A \to A \times_B A$.

For $f : A \to B$ and $g : C \to D$, the pushout product $f \pushpr g$ is defined to be the canonical gap map

A ×C [r] [d] [dr, phantom, "⌜", very near end]     A ×D[d] [ddr, bend left]

B ×C [r] [drr, bend right]     P [dr, dotted, "f g"]

B ×D

where $P :\defeq (A \times D) \sqcup_{A \times C} (B \times C)$.

The fibres of $\Delta f$ are given by

\[ \fib_{\Delta f}(a, a', p) \equiv ((a, p) =_{\fib_f(f(a'))} (a', \refl{f(a)})),\]
and in particular,
\[\fib_{\Delta f}(a, a, \refl{a}) \equiv \Omega_{(a, \refl{a})} \fib_f(f(a)). \]

Direct calculation:

\begin{align*}
\fib_{\Delta f}(a, a', p)
&:\defeq \sm{x : A} (x, x, \refl{f(x)}) = (a, a', p) \\
&\equiv \sm{x : A} \sm{l : x = a} \sm{r : x = a'} !\ap_f(l) \cdot \ap_f(r) = p \\
&\equiv \sm{r : a = a'} \ap_f(r) = p \\
&\equiv \sm{r : a = a'} !\ap_f(r) \cdot p = \refl{f(a')}\\
&\equiv \sm{r : a = a'} r_*(p) = \refl{f(a')}\\
&\equiv (a, p) = (a', \refl{f(a')})
\end{align*}

The pushout product is the `external fibrewise join', in the sense that
for $b : B$ and $d : D$,

\[ \fib_{f \pushpr g}(b, d) \equiv \fib_f(b) \join \fib_g(d) \]

This is another application of descent. Consider the cube

_f(b) ×_g(d) [dl] [dr] [d]

_f(b) [d]     A ×C [dl] [dr]     _g(d) [dl,crossing over] [d]

A ×D [dr]     1 [d] [from=ul,crossing over]     B ×C [dl]

B ×D

The back vertical map extracts the $A$ and $C$ from the fibres, the side
vertical maps extract the $A$ or $C$ and pair with $b$ or $d$ in the
other component, and the front vertical map is $(b,d)$.  By singleton
contractibility and paths in products being component-wise, all the
vertical sides are pullback squares. The corresponding square

_f(b) _g(d) [r] [d]     1 [d]

P [r, "f g" swap]     B ×D

is a pullback by Theorem <ref>, so
$\fib_f(b) \join \fib_g(d)$ is equivalent to the fibre of
$f \pushpr g$ at $(b, d)$.

We now quote the Theorem that actually does the work:

Consider the following square.

Z [r, "g"] [d, "f" swap]     Y [d, "h"]

X [r, "k" swap]     W

* If the square is a pushout and $\Delta f \pushpr \Delta g$ is an equivalence, then the square is also a pullback.

* If the square is a pullback and $h \pushpr k$ is an equivalence, then the square is also a pushout.

A dull commutative square in reduced types is a pullback square iff it is a pushout square.

Suppose a dull commutative square in reduced types

[r, ""] [d, "" swap]     [d, ""]

[r, "" swap]

By Definition <ref> and
Proposition <ref>, we have base points
$\star_{\zE}$, $\star_{\zF}$, $\star_{\zG}$, $\star_{\zH}$, and
the maps are all pointed. Thus, the fibres all have dull points—
e.g. $\fib_{\zf}(\star_{\zF}) := \sm{z:\zE} \zf(z) = \star_{\zF}$ has a
point given by $\star_{\zE}$ and the path showing $\zf$ is pointed.

To use Theorem <ref>, we just need to show that $\Delta \zf
\pushpr \Delta \zg$ and $\zh \pushpr \zk$ are equivalences, which we
will do using the “contractible fibres” definition of equivalence.

The fibre of $\Delta \zf \pushpr \Delta \zg$ over the basepoint $p_0
:\defeq ( (\star_{\zE},\star_{\zE},\refl{\zf(\star_{\zE})}),
(\star_{\zE},\star_{\zE},\refl{\zg(\star_{\zE})}))$ is $\Omega
(\fib_{\zf}(\star_{\zF}))\join \Omega(\fib_{\zg}(\star_{\zG}))$ by
Lemma <ref> (where $f(\star_{\zE}) = \star_{\zF}$
and $g(\star_{\zE}) = \star_{\zG}$ because the maps are pointed) and
Proposition <ref>.  Again by
Proposition <ref>, the fibre of $h \pushpr k$
over $q_0 :\defeq (\star_{\zH},\star_{\zH})$ is
$\fib_{\zh}(\star_{\zH}) \join \fib_{\zk}(\star_{\zH})$.  To show
that these are both contractible, by
Proposition <ref>, it suffices to
show that the pieces of the join are dull, reduced types.  By
Proposition <ref>, reduced types are closed
under fibres and loop spaces, and for the basepoints these types are
dull because the basepoints are.  This shows that $\fib_{\Delta \zf
\pushpr \Delta \zg}(p_0)$ and $\fib_{\zh \pushpr \zk}(q_0)$ are

Since the fibres over $p_0$ and $q_0$ are contractible, to show that
general fibres $\fib_{\Delta \zf \pushpr \Delta \zg}(p)$ and $\fib_{\zh
\pushpr \zk}(q)$ over any $p$ and $q$ are contractible, by
Lemma <ref> it suffices to show that $p : (\zE
\times_{\zF} \zE) \times (\zE\times_{\zG} \zE)$ and $q :
\zH \times \zH$ are elements of 0-connected types, since being
contractible is a proposition.  For $q$, by
Corollary <ref>, $\zH$ is $\infty$-connected
and in particular $0$-connected, so $\zH \times \zH$ is
0-connected by Lemma <ref>.  For $p$, again using
closure under products, we need to show that $(\zE\times_{\zF}
\zE)$ and $(\zE\times_{\zG} \zE)$ are 0-connected.  By
Corollary <ref>, $\zE$ is 0-connected and
$\zF,\zG$ are 1-connected, so the pullbacks are 0-connected as well by
Lemma <ref>.  This use of 0-connectedness is
important because the fibre of a map between dull reduced types is only
dull when the point over which we are taking the fibre is, so the
argument in the previous paragraph can be applied directly to $p$ and

We showed that the counit $\Sigma \Omega \zE \to \zE$ is an equivalence in Corollary <ref>, and we can now show that the unit is as well:

For any $\zE : \Redu$, the unit map $\zE \to \Omega \Sigma \zE$ is an equivalence.

The pushout square defining the suspension is

\[
\begin{tikzcd}
\zE \ar[d] \ar[r] \arrow[dr, phantom, "\lrcorner", very near start] \arrow[dr, phantom, "\ulcorner", very near end] & 1 \ar[d, , "\mathsf{s}"] \\
1 \ar[r, "\mathsf{n}", swap] & \Sigma \zE
\end{tikzcd}
\]

By Theorem <ref>, this is also a pullback square.  However, we also have a pullback square

\[
\begin{tikzcd}
\mathsf{n} =_{\Sigma \zE} \mathsf{s} \ar[d] \ar[r] \arrow[dr, phantom, "\lrcorner", very near start] \arrow[dr, phantom, "\ulcorner", very near end] & 1 \ar[d, "\mathsf{s}"] \\
1 \ar[r, "\mathsf{n}", swap] & \Sigma \zE
\end{tikzcd}
\]

so uniqueness of pullbacks gives an equivalence $\zE \equiv (\mathsf{n}=\mathsf{s})$.  If we
consider the suspension to be pointed by $N$, then $\Omega(\Sigma \zE)$
is the type $\mathsf{n}=\mathsf{n}$.  But since $\zE$ is pointed, we have a path $\!
\mathsf{mer}(\star_{\zE}) : \mathsf{s} = \mathsf{n}$, and composition with this path gives an
equivalence $(\mathsf{n} = \mathsf{s}) \equiv (\mathsf{n} = \mathsf{n})$, so $\zE \cong \Omega(\Sigma \zE)$.

The unit of the adjunction $\Sigma \vdash \Omega$ sends $e : \zE$ to the
path $\mathsf{mer}(e) \cdot !\mathsf{mer}(\star_{\zE})$, so the composite equivalence is
indeed the unit.

§ RELATING SYNTHETIC AND ANALYTIC SPECTRA

In the previous section, we showed that Axiom S gives the reduced
types/synthetic spectra many of the properties that we expect spectra to
have.  In this section, we investigate an additional axiom, which
relates the synthetic spectra represented by reduced types to the
concrete/analytic spectra that can be defined in pure homotopy type
theory.  This also results to be proved using the reduced types and
transferred to analytic spectra, and vice versa.

One can define (“$\Omega$-”)spectra internally in type
theory <cit.> as sequences of types
and connecting maps.

A sequential prespectrum $J$ is a sequence of pointed modal types $J : \mathbb{N} \to \Modal_\star$ together with pointed maps $\alpha_n : J_n \to_\star \Omega J_{n+1}$. A sequential spectrum is a prespectrum such that the $\alpha_n$ are pointed equivalences. The types of such objects are denoted $\SeqPreSpec$ and $\SeqSpec$ respectively.

A morphism of sequential (pre)spectra $f : \Mor(I,J)$ is a sequence of pointed maps $f_n : I_n \to_\star J_n$ that commute with the $\alpha_n$.

We need to restrict the types in the sequence to be modal so that semantically they correspond to sequences of spaces. Otherwise we would be describing a spectrum object in $P\Spec_\star$, something more complicated than an ordinary spectrum.

Our goal is to relate our reduced types with these sequential spectra. We do this by describing a series of (dull) adjoints:

[column sep=large]
_⋆[r, bend left, "susp"] [r, phantom, "⊥"]     [r, phantom, "⊥"] [r, bend left, "spec"] [l, bend left, "0th", pos=0.48]     [r, phantom, "⊥"] [r, bend left, "L"] [l, bend left, "ι"]     [l, bend left, "R"]

The left two adjunctions take place almost entirely in pure homotopy
type theory: $\mathrm{susp}$ takes a space $X$ to the suspension
prespectrum $(X, \Sigma X, \Sigma \Sigma X, \ldots)$, and
$\mathrm{spec}$ is spectrification, inverting the connecting maps to
equivalences. Their composite $\mathrm{spec} \circ \mathrm{susp}$ is
thus an analytic analogue of the $\Sigma^\infty$ stabilisation functor
we defined in Section <ref>, taking a modal type to its
suspension analytic spectrum.  The right adjoint $\iota$ is
forgetful/an inclusion, while $0th$ selects the $0th$ term of a
pre-spectrum, and the composite $0th \circ \iota$ is an analytic
analogue of $\Omega^\infty$. All that takes us out of ordinary HoTT is
the requirement that the types involved are modal types. The new
construction in this section is the rightmost adjunction relating
analytic and synthetic spectra, and an axiom stating that it is an
adjoint equivalence, making the two notions of spectra coincide.

For any pointed modal type $X$, we have the suspension sequential prespectrum $\mathrm{susp} X$ where $(\mathrm{susp} X)_n :\defeq \Sigma^n X$, and the structure maps are the unit maps $\alpha_n : \Sigma^n X \to \Omega\Sigma^{n+1} X$.

Note that all the $\Sigma^n X$ are modal, by Proposition <ref>.

$\mathrm{susp}$ is left adjoint to taking the zeroth type of a sequential prespectrum.

Suppose we have a map $X \to_\star J_0$. We need a map $\Sigma X \to_\star J_1$ such that

X [r] [d]     ΩΣX [d]

J_0 [r]     ΩJ_1

commutes, equivalently, one such that

ΣX [r, equals] [d]     ΣX [d]

ΣJ_0 [r]     J_1

commutes. Then $\Sigma X \to_\star J_1$ is forced to be the composite of $\Sigma X \to \Sigma J_0 \to J_1$. This argument iterates to produce a map $\Mor(\mathrm{susp}X, J)$, showing the data of such a morphism is equivalent to that of a map $X \to_\star J_0$.

For a sequential prespectrum $J$, the spectrification of $J$ is given by

\begin{align*}
(\mathrm{spec} J)_n :\defeq \colim_k \Omega^k J_{n+k}
\end{align*}

Each $(\mathrm{spec} J)_n$ is modal by Proposition <ref> and Lemma <ref>. That these types actually assemble into a sequential spectrum has not yet been proven in type theory, so we leave it as an unjustified assertion — note that this assertion is a statement in pure homotopy type theory, and is not dependent on the modal extension we make in this paper, a proof of the assertion would certainly apply when the types concerned happen to be modal.

Assertion 1
This formula defines a sequential spectrum, and the operation is left adjoint to the inclusion of sequential spectra into sequential prespectra.

Now we turn to the $L \dashv R$ adjunction relating these sequential
spectra to our synthetic spectra'. First, we can extract a sequential
prespectrum from any reduced type $\zE$.

For $\zE : \Redu$, define $R\zE : \SeqPreSpec$ by

\begin{align*}
(R\zE)_n :\defeq \Omega^\infty \Sigma^n \zE
\end{align*}

with connecting maps

\begin{align*}
(R\zE)_n \defeq \Omega^\infty \Sigma^n \zE \to_\star \Omega^\infty \Omega \Sigma \Sigma^n \zE \equiv_\star \Omega \Omega^\infty \Sigma \Sigma^{n} \zE \equiv_\star \Omega \Omega^\infty \Sigma^{n+1} \zE \defeq \Omega (R\zE)_{n+1}
\end{align*}

The first map is given by functoriality of $\Omega^\infty$ on the unit $X \to_\star \Omega \Sigma X$ for $X = \Sigma^n \zE$.
The second is derived from Proposition <ref>
and the third is essentially by definition, depending on how iterated suspension is defined.

$R\zE$ is a sequential spectrum.

By Proposition <ref>, reduced types are closed
under suspensions, so an induction shows that $\Sigma^n \zE$ is reduced.
Therefore the unit map $\Sigma^n \zE \to_\star \Omega \Sigma \Sigma^n \zE$
is an equivalence by Corollary <ref>, so the connecting map defined above is a composite of equivalences.

Conversely, suppose we have a sequential prespectrum $J : \SeqPreSpec$. We can produce a reduced type $LJ : \Redu$.

For $J : \SeqPreSpec$ let $LJ : \Redu$ be

\begin{align*}
LJ :\defeq \colim (\Sigma^\infty J_0 \to \Omega \Sigma^\infty J_1 \to \Omega^2 \Sigma^\infty J_2 \to \dots)
\end{align*}

where the maps $\Sigma^\infty J_n \to \Omega \Sigma^\infty J_{n+1}$ are given by

\begin{align*}
\Sigma^\infty J_n \to \Omega \Sigma \Sigma^\infty J_n \equiv \Omega \Sigma^\infty \Sigma J_n \to \Omega \Sigma^\infty \Sigma \Omega J_{n+1} \to \Omega \Sigma^\infty J_{n+1}
\end{align*}

where the maps are the unit of $\Sigma \vdash \Omega$, Proposition <ref>, functoriality on the connecting map $J_n \to \Omega J_{n+1}$ of the prespectrum, and then the counit of $\Sigma \vdash \Omega$.

To see that this type is reduced, by
Proposition <ref>, $\natural L J$ is equivalent
to the colimit of the $\natural \Omega^n \Sigma^\infty J_i$, and
reduced types are closed under loop spaces by Proposition <ref>, and $\Sigma^\infty$ of any type is reduced by Proposition <ref>, so each of the terms of that colimit is contractible, so the colimit is as well.

Let $S : \SeqPreSpec$ denote the sphere (analytic) prespectrum, i.e. the suspension prespectrum of $S^0$. Then $LS \equiv \sphere$, because at each level of the colimit we have

\[\Omega^n \Sigma^\infty S^n \defeq \Omega^n (S^n \topsmash \sphere) \equiv \Omega^n (\Sigma^n \sphere) \equiv \sphere \]

The first equivalence is $\Sigma^n A \equiv S^1 \topsmash (S^1 \topsmash
\ldots (S^1 \topsmash A)) \equiv (S^1 \topsmash S^1 \ldots \topsmash S^1) \topsmash A
\equiv S^n \topsmash A$,
using associativity of smash and $\Sigma A \equiv S^1 \topsmash A$ <cit.>,
The second is given by iterating $\Omega \Sigma \zE \equiv \zE$ for a dull reduced type $\zE$ (Corollary <ref>), noting that the suspension of a dull reduced type is reduced by Proposition <ref>, and $\sphere$ is assumed to be reduced.

The operations $L$ and $R$ are dull adjoints:
\[ \natural(L\zJ \to_\star \zE) \equiv \Mor(\zJ, R\zE) \]

Suppose we have a dull map $\zk : L\zJ \to_\star \zE$. We can forget the fact that $\zk$ is pointed using Proposition <ref>. The data of $\zk$ (using the universal property for maps out of a colimit) is equivalent to a sequence of dull maps $\zk_n : \Omega^n \Sigma^\infty \zJ_n \to \zE$ so that the squares

Ω^n Σ^∞_n [d, "_n" swap] [r]     Ω^n+1 Σ^∞_n+1 [d, "_n+1"]

[r, equal]

We can transpose the $\zk$ across the adjunctions to get maps $\hat{k}_n : J_n \to_\star \Omega^\infty \Sigma^n \zE$. This type on the right is exactly $(R\zE)_n$, so we just have to show that this collection of maps forms a morphism of sequential prespectra. This mostly involves unwinding the definition of the map $\Omega^n \Sigma^\infty \zJ_n \to \Omega^{n+1} \Sigma^\infty \zJ_{n+1}$

Precompose the upper left corner with the equivalence $\Omega^{n+1}\Sigma^\infty\Sigma \zJ_n
\equiv \Omega^n\Omega\Sigma^\infty\Sigma \zJ_n \equiv
\Omega^n\Omega\Sigma\Sigma^\infty \zJ_n \equiv
\Omega^n\Sigma^\infty \zJ_n$:

[column sep=5em]
Ω^n+1 Σ^∞Σ_n [d,"…" swap] [r,"Ω^n+1Σ^∞α̂_n"]     Ω^n+1 Σ^∞_n+1 [d,"_n+1"]

[r, equal]

Since $\Sigma \dashv \Omega$, and for dull reduced types Axiom S implies that $\Sigma$ and $\Omega$ are inverses,
we also have an adjunction $\Omega \dashv \Sigma$ on dull reduced types.
Transposing across this and $ \Sigma^\infty \dashv \Omega^\infty$ vertically, such squares are equivalent to squares

Σ_n [d, "…" swap] [r, "α̂_n"]     _n+1 [d, "_n+1"]

(R)_n+1 [r, equal]     (R)_n+1

Now transposing `diagonally' along $\Sigma \dashv \Omega$, we get

_n [d, "…" swap] [r, "α_n"]     Ω_n+1 [d, "Ω_n+1"]

Ω(R)_n+1 [r, equal]     Ω(R)_n+1

Finally, precompose the lower left corner with the equivalence $\beta_n : (R\zE)_n \equiv \Omega (R\zE)_{n+1}$ to get

_n [d, "…" swap] [r, "α_n"]     Ω_n+1 [d, "Ω_n+1"]

(R)_n [r, "β_n" swap]     Ω(R)_n+1

All we have left is to check is that the vertical map on the left is equal to $\hat{k}_n$. Tracing through what we have done, it is equal to

\begin{align*}
\zJ_n &\to \Omega \Sigma \zJ_n
\to \Omega \Omega^\infty  \Sigma^{n+1} \Omega^{n+1} \Sigma^\infty \Sigma \zJ_n
\to \Omega \Omega^\infty  \Sigma^{n+1} \Omega^{n+1} \Sigma \Sigma^\infty \zJ_n \\
&\to \Omega \Omega^\infty \Sigma^{n+1} \Omega^n \Sigma^\infty \zJ_n
\to \Omega \Omega^\infty \Sigma^{n+1} \zE
\to \Omega^\infty \Omega \Sigma^{n+1} \zE
\to \Omega^\infty \Sigma^n \zE
\end{align*}

In the above sequence, the map
$\Omega \Omega^\infty \Sigma^{n+1} \Omega^n \Sigma^\infty \zJ_n \to
\Omega \Omega^\infty \Sigma^{n+1} \zE$ is given by
$\Omega \Omega^\infty \Sigma^{n+1} \zc{k}_n$, so by naturality, we can
move this use of $\zc{k}_n$ to the end. The above chain is then equal to the composite

\begin{align*}
\zJ_n &\to \Omega \Sigma \zJ_n
\to \Omega \Omega^\infty  \Sigma^{n+1} \Omega^{n+1} \Sigma^\infty \Sigma \zJ_n
\to \Omega \Omega^\infty  \Sigma^{n+1} \Omega^{n+1} \Sigma \Sigma^\infty \zJ_n \\
&\to \Omega \Omega^\infty \Sigma^{n+1} \Omega^n \Sigma^\infty \zJ_n
\to \Omega^\infty \Omega \Sigma^{n+1} \Omega^n \Sigma^\infty \zJ_n
\to \Omega^\infty \Sigma^n \Omega^n \Sigma^\infty \zJ_n
\to \Omega^\infty \Sigma^n \zE
\end{align*}

For this to be the transpose of $\zc{k}_n$, what we need is for the
$\zJ_n \to \Omega^\infty \Sigma^n \Omega^n \Sigma^\infty \zJ_n$,
leaving off the last map, is equal to the unit.  And it is, by liberal
use of the triangle inequalities, as every map in the string is either
unit/counit or an equality of composites in a system of commuting

Having established this adjunction, we introduce the following axiom, which identifies the synthetic and analytic spectra:

Axiom N