classic example is the guarded stream type $\Str_A \cong A \times \Later \Str_A$, with

\[
\Cons_A : A \times \Later \Str_A \cong \Str_A
\]

The presence of the modality enforces the requirement that the head of the stream is available
immediately, but the tail may only be accessed after some productive work has taken place. This
allows us to  construct an infinite stream of ones:

\[
\mathsf{inf\_stream\_of\_ones} \defeq \LobV{s}{\Cons(1, s)}
\]

Unlike the ordinary type of streams, $\Str_A$ does not behave like a coinductive type: we may only
define causal operations, which excludes useful functions (e.g. the $\Tail$ function). In
order to regain coinductive behaviour, <cit.> introduced the always
modality $\Box$, an idempotent comonad for which

\begin{equation*}
\Box \Later A \Equiv \Box A. \TagEq[$\ast$]\label{eq:guarded:force}
\end{equation*}

Combining $\Box$ and $\Later$ in the same system has proven tricky. Previous work has used
delayed substitutions <cit.>, or replaced $\Box$ with clock
quantification <cit.>. Neither solution is
entirely satisfactory: the former poses serious implementation and usability issues, and the latter
does not enjoy the conceptual simplicity of a single modality. We will show that  enables us
to effortlessly combine the two modalities whilst satisfying (<ref>).

To encode guarded recursion inside , we must

* construct a mode theory that induces an applicative functor $\Later$ and an idempotent comonad
$\Box$ satisfying (<ref>),

* construct the intended model of $\MTT$ with this mode theory,  a model where
these modalities are interpreted in the standard way <cit.>, and

* include Löb induction as an axiom, and use it to reason about guarded streams.

§.§ A guarded mode theory

\[
\begin{tikzpicture}[on grid, node distance = 2.5cm]
\node (T) {$t$};
\node (S) [right = of T] {$s$};
\path[->] (T) edge[looseness = 15, out = 210, in = 150] node[left] {$\ell$} (T);
\path[->] (S) edge[bend left] node[below] {$\delta$} (T);
\path[->] (T) edge[bend left] node[above] {$\gamma$} (S);
\node (E) [right = 2.5cm of S]
\delta \circ \gamma &\le 1 & 1 &= \gamma \circ \delta\\
1 &\le \ell & \gamma &= \gamma \circ \ell
\end{aligned}$};
\end{tikzpicture}
\]

The `adjoint bowling pin' $\ModeGuarded$: a mode theory for guarded recursion.

We define $\ModeGuarded$ to be the mode theory generated by the graph and equations of Fig.
<ref>. We require that $\ModeGuarded$ be poset-enriched,
i.e. that there be at most one 2-cell between a pair of modalities $\mu, \nu$, which we denote by
$\mu \le \nu$ when it exists. Consequently, we need not state any coherence equations between

Unlike prior guarded type theories, $\ModeGuarded$ has two modes. We will think of elements
of $s$ as being constant types and terms, while types in $t$ may vary over time.
Observe that we can thence construct a composite modality $b \defeq \delta \circ \gamma$. Moreover,
this modality is idempotent, for $b \circ b = \delta \circ \gamma \circ \delta \circ \gamma = \delta
\circ \gamma = b$. We will prove in <ref> that

$\Modify[b]$ is an idempotent comonad and $\Modify[\ell]$ is an applicative functor.

§.§ Decomposing the standard model

The above mode theory arises from a careful and informative decomposition of the standard model of
guarded recursion, namely the topos of trees $\PSH{\omega}$, along with the later and always endomodalities.

The topos of trees consists of presheaves over the natural numbers, seen as a poset with the usual
order. An element $x_n \in X(n)$ of a presheaf $X : \PSH{\omega}$ represents an element computed
after $n$ steps of computation. The restriction maps $r_n : X(n+1) \to X(n)$ trim an element
computed after $n+1$ steps to its form at the preceding moment in time. The canonical example is
given by $X(n) \defeq \{\text{streams of length $n$}\}$, where $r_n$ deletes the last element of a
stream of length $n+1$. The later and always endomodalities are given by delaying the computation by
one step, and by taking global sections (total elements):

\begin{align*}
(\Later X)(n) &\defeq {
\begin{cases}
\{\ast\} &\text{if $n = 0$} \\
X(n-1)   &\text{if $n > 0$}
\end{cases}
}  &
(\Box X)(n) &\defeq \Hom[\PSH{\omega}]{1}{X}
\end{align*}

To arrive at the mode theory above, one must notice that the comonad $\Box$ results in a
constant presheaf, namely one which consists of the same set at each time. We can thus
decompose it into the adjunction

\begin{equation}
\begin{tikzpicture}[on grid, node distance = 2.5cm, baseline=(current  bounding  box.center)]
\node (T) {$\PSH{\omega}$};
\node (S) [right = of T] {$\SET$};
\node (Z) [right = 1.3cm of T, rotate=+90] {$\Adjoint$};
\path[->] (T) edge[looseness = 10, out = 210, in = 150] node[left] {$\Later$} (T);
\path[->] (T) edge[bend left] node[above] {$\GSec$} (S);
\path[->] (S) edge[bend left] node[below] {$\Disc$} (T);
\end{tikzpicture}
\label{diag:guarded:model}
\end{equation}

$\GSec$ maps $X : \PSH{\omega}$ to the set of its global sections $\Hom[\PSH{\omega}]{1}{X}$, and
$\Delta$ maps a set $S$ to the constant presheaf $(\Delta S)(n) \defeq S$. It is well-known that
$\Delta \Adjoint \Gamma$, and `always' is given by the induced comonad $\Box \defeq \Disc \circ
\GSec$. This explains the provenance of the two modes in Figure
<ref>: $s$ stands for sets, and $t$ for timed
sets, i.e. presheaves over $\omega$.

We want to bootstrap (<ref>) into a model of . We will do so by leveraging
an impressive sequence of facts:

* Both categories in (<ref>) are presheaf categories, and hence models of
: see <ref>.

* Every functor in (<ref>) is a right adjoint.

* The corresponding left adjoints are introduced by precomposition, and hence can easily  be
arranged into a modal context structure for the mode theory $\ModeGuarded$ as per

* Hence, by uniqueness of adjoints the functors in (<ref>) are induced by
right Kan extension. Consequently, they can be bootstrapped into dependent right adjoints, by
Lemma <ref>.

* Therefore, by Theorem <ref>, this data yields a model of  with mode theory $\ModeGuarded$.

Let us elaborate on this chain of reasoning.
First, we identify the category $\SET$ and the category $\PSH{1}$ of presheaves over the terminal
category. Second, we construct the two left adjoints. As $\omega$ has an initial object $0$, we
obtain a left adjoint to the discrete functor $\Disc$, given by

\[
\Pi_0(X) \defeq X(0)
\]

It is easy to see that $\Pi_0 \Adjoint \Disc$: by naturality at the unique morphism $0 \leq n$ we
see that any $\alpha : X \To \Disc S$ is fully determined by the component $\alpha_0 : X(0) \to S$.
Furthermore, recall from the work of <cit.> that the later modality $\Later$ has a
left adjoint $\Earlier : \PSH{\omega} \to \PSH{\omega}$ (pronounced `earlier'), given by

\[
(\Earlier X)(n) \defeq X(n+1)
\]

It remains to show that the three left adjoints—$\Pi_0$, $\Delta$, and $\Earlier$—are given by
precomposition. We define three monotone functions between the posets $1 \defeq \{\ast\}$ and

K_0         :    1            →       ω         !_ω :       ω       →       1              l :           ω       →       ω

∗       ↦       0                  n          ↦       ∗               n          ↦       n+1

Identifying $\SET$ with $\PSH{1}$, we see that

\begin{align*}
\Pi_0  &= \Pre{K_0}{} : \PSH{\omega} \to \SET &
\Delta &= \Pre{{!}_\omega}{} : \SET \to \PSH{\omega} &
\Earlier &= \Pre{l}{} : \PSH{\omega} \to \PSH{\omega}
\end{align*}

Moreover, we trivially have the following pointwise equations and inequalities:

\begin{align*}
\text{id}_\omega &\leq l
K_0 \circ {!}_\omega &\leq \text{id}_\omega
\text{id}_1 &= {!}_\omega \circ K_0
{!}_\omega &= {!}_\omega \circ l
\end{align*}

Seeing posets as categories, pointwise inequalities are simply natural transformations between
monotone maps. By feeding them into the strict 2-functor $\Pre{(-)}{} : \Coop{\CAT} \to \CAT$, we
are able to define a strict 2-functor $\Interp{-} : \Coop{\ModeGuarded} \to \CAT$ which maps

γ       : t →s        ⟼        Δ       : →ω

δ       : s →t        ⟼        Π_0        : ω →

ℓ         : t →t        ⟼               : ω →ω

This fully specifies the modal context structure, which consists of left adjoints. Each of these
left adjoints is given by precomposition. Thus, the unique corresponding right adjoint is given by
right Kan extension (see <ref>). Hence, by Lemma
<ref> and Theorem <ref>,

There is a model of  with mode theory $\ModeGuarded$, interpreting $s$ as $\SET$ and $t$ as
$\PSH{\omega}$. Furthermore, this model interprets $\delta$ by the dependent right adjoint arising
from $\CComp \Adjoint \Disc$, $\gamma$ by $\Disc \Adjoint \GSec$, and $\ell$ by $\Earlier \Adjoint
\Later$.

This mode theory is a poset-enriched category. As a result, the key substitutions are unique: for
any $\mu, \nu$ there is at most one substitution $\IsSb[\LockSb{\Gamma}]{\Key{\nu \le
\mu}{\Gamma}}{\LockSb{\Gamma}<\nu>}$. This property means that we can elide them without
ambiguity. However, this may sometimes make type-checking on pen-and-paper difficult, so we employ
a simplified notation: we will write $A^{\nu \le \mu}$ or $M^{\nu \le \mu}$ for the application of
the unique key substitution $\nu \le \mu$ in context $\LockSb{\Gamma}$. For instance, given a type
$\LockCx{\Gamma}<1> = \IsTy{A}[1]<t>$ we can form the type $\IsTy[\LockCx{\Gamma}<\ell>]{A^{1 \le
\ell}}[1]<t>$, and hence the type $\IsTy{\Modify[\ell]{A^{1 \le \ell}}}[1]<t>$.

§.§ Guarded recursion, internally

Given the model that we constructed above, we feel perfectly justified in defining the following
shorthands within :

\begin{align*}
\Box A &\defeq \Modify[b]{A} &
\Later A &\defeq \Modify[\ell]{A} &
\GSec A &\defeq \Modify[\gamma]{A} &
\Disc A &\defeq \Modify[\delta]{A}
\end{align*}

where $b \defeq \delta \circ \gamma$. The aim of this section is to show that $\MTT{}$ equipped with $\ModeGuarded$ and these shorthands can be used to reason about guarded recursion. In particular, we will show that this is strict improvement on previous solutions, by establishing that

* When restricted to mode $s$, the type theory is simply standard Martin-Löf Type Theory.

* The modalities on mode $t$ give rise to the standard modalities and operations of
Guarded Type Theory <cit.> inside the type theory.

First, we wish to show that if we restrict ourselves to endomodalities $\mu \in \Hom{s}{s}$ from
sets to sets, the type theory is just . Looking at Fig.
<ref> as a finite state machine, we see that all loops on $s$
are of the form $\gamma \circ \ell^n \circ \delta$, and the equations of $\ModeGuarded$ allow us to
prove that they are all equal to the identity $1_s$. It follows that $\Modify{A} \simeq A$. Finally,
as there is no non-trivial 2-cell $1_s \To 1_s$ the variable rule reduces to

\[
\inferrule{
\mu \in \Hom{s}{s}\\
\IsCx{\Gamma}<s>\\
\IsTy{A}<s>\\
(\DeclVar{x}{A}<\mu>) \in \Gamma
\IsTm{x}{A}<s>
\]

which is essentially the usual variable rule of .

Second, we use the combinators of <ref> to prove that $\Box$ is an
idempotent comonad.

\[
\arraycolsep=1.4pt
\begin{array}{lcllcl}
\Dup_A    &:&  \Box A \xrightarrow{\simeq} \Box \Box A \qquad\qquad &\Unbox_A &:& \Box A \to A^{b \le 1} \\
\Dup_A(x) &\defeq& \MComp*{x}{b}{b}   \qquad\qquad &\Unbox_A(x) &\defeq& \Triv*{\Coe{x}{b}{1}}
\end{array}
\]

Recall the $K$ operator $\ZApp{-}{-}{b} : \Box(A \to B) \to \Box A \to \Box B$ for the modality $b$,
which was defined in <ref>. Writing $ \Always(M) \defeq
\MkBox[b]{M}$, the claim that $\Box$ is an internal idempotent comonad amounts to defining terms of
the following types.

\begin{align}
(x : \Box A) &\to \Id{\Box A}{x}{\ZApp{\Always(\Unbox)}{\Dup(x)}{b}}
\label{eq:guarded-recursion:comonad1}\\
(x : \Box A) &\to \Id{\Box A}{x}{\Unbox(\Dup(x))}
\label{eq:guarded-recursion:comonad2}\\
(x : \Box A) &\to \Id{\Box \Box \Box A}{\Dup(\Dup(x))}{\ZApp{\Always(\Dup)}{\Dup(x)}{b}}
\label{eq:guarded-recursion:comonad3}
\end{align}

These can be constructed by unfolding and modal induction on $x : \Box A$.

The $K$ operator $\ZApp{-}{-}{\ell} : \Later(A \to B) \to \Later A \to \Later B$ for the modality
$\ell$ proves that $\Later$ is an applicative functor. We show that $\Later$ is pointed by constructing the term

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\Next_A    &:&      A \to \Later A \\
\Next_A(x) &\defeq& \Coe{\Triv{x}}{1}{\ell}
\end{array}
\]

Next, we show the defining equivalence (<ref>). We calculate that $b \circ \ell
\defeq \delta \circ \gamma \circ \ell = \delta \circ \gamma$, and hence that the equivalence is a
corollary of a combinator given in <ref>:

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\Force_A(x)    &:&   \Box \Later A \xrightarrow{\simeq} \Box A \\
\Force_A(x) &\defeq& \MComp*{x}{b}{\ell}
\end{array}
\]

As a sanity check, we can compute that the following composite is the identity:

\[
\begin{tikzpicture}[on grid, node distance = 5cm]
\node (A) {$\Box A$};
\node (B) [right = of A] {$\Box \Later A$};
\node (C) [right = of B] {$\Box A$};
\path[->] (A) edge node[above] {$\ZApp{\Always(\Next)}{-}{}$} (B);
\path[->] (B) edge node[above] {$\Force$} (C);
\end{tikzpicture}
\]

The calculation is as follows:

\begin{align*}
&&\text{by induction, suppose $x = \MkBox[b]{y}$}\\
&= \MComp{\ZApp{\MkBox[b]{\Coe{\Triv{-}}{1}{\ell}}}{\MkBox[b]{y}}{}}{b}{\ell} &&\\
&= \MComp{\MkBox[b]{\Coe{\Triv{y}}{1}{\ell}}}{b}{\ell}  &&\\
&= \MComp{\MkBox[b]{\MkBox[\ell]{y}}}{b}{\ell} &&\\
&= \MkBox[b]{y} &&\text{as $b \circ \ell = b$}\\
&= x
\end{align*}

The only thing that remains is to add Löb induction. This is a modality-specific
operation that cannot be expressed in the mode theory, so we must add it as an axiom:

(A^1 ≤ℓ →A) →A<t>

MA^1 ≤ℓ →A<t>

(M)M(((M)))(A^1 ≤ℓ →A) →A<t>

Notice that these rules are only added in mode $t$, as they only admit an interpretation in
$\PSH{\omega}$ <cit.>. Unfortunately, these ad-hoc additions mean that the
canonicity theorem of <ref> no longer applies.

§.§ Reasoning about Streams

We now put  to work: we will use it to reason about infinite streams defined by guarded
recursion. We will demonstrate that the rules and axioms given in
<ref> suffice to carry out coinductive constructions. In
particular, we will reproduce an example of <cit.>: we will show that $\ZipWith(f)$ on
a coinductive stream is commutative whenever $f$ itself is.

In order to simplify our working, we will swap the intensional equality type $\Id{A}{M}{N}$ with an
extensional identity type $\Eq{A}{M}{N}$. This has the same introduction rule, but its
elimination is replaced by the usual equality reflection rule

\[
\inferrule{
\IsTm{P}{\Eq{A}{M_0}{M_1}}
\EqTm{M_0}{M_1}{A}
\]

This is straightforwardly interpreted in the model, as both modes are mapped to presheaf toposes.
The switch to extensional equality is not strictly necessary: we could carry out the following
calculations with intensional identity, at the price of significantly more verbose terms. Moreover,
the need for the function extensionality axiom would arise. However, adding Löb induction has
already ensured that type-checking is undecidable, so nothing of value is lost by making the switch
to extensional type theory for these examples.

We begin with a simple reasoning principle. Eliding $(-)^{1 \leq \ell}$ annotations:

$(A : \Uni)(x, y : \Dec{A}) \to \Later\Eq{\Dec{A}}{x}{y} \to \Eq{\Later \Dec{A}}{\Next(x)}{\Next(y)}$

Suppose $x , y : \Dec{A}$ and $p : \Later\Eq{\Dec{A}}{x}{y}$; to show $\Next(x) = \Next(y) :
\Later \Dec{A}$. By congruence and the elimination rule for the modality, it suffices to prove $x
= y : \Dec{A}$ in the locked context $\LockCxV{A : \Uni, x : \Dec{A} , y : \Dec{A},
\DeclVar{p}{\Eq{\Dec{A}}{x}{y}}<\ell>}<\ell>$. But by the variable rule we have $p :
\Eq{\Dec{A}}{x}{y}$ in this context, and hence $x = y : \Dec{A}$.

This can be used to prove internally that guarded fixed points are unique.

$\Lob(M)$ is the unique guarded fixed point of $M : \Later \Dec{A} \to \Dec{A}$,

\[
(A : \Uni)(x : \Dec{A}) \to \Eq{\Dec{A}}{M(\Next(x))}{x} \to \Eq{\Dec{A}}{\Lob(M)}{x}
\]

Suppose $A : \Uni$; to show $(x : \Dec{A}) \to \Eq{\Dec{A}}{M(\Next(x))}{x} \to
\Eq{\Dec{A}}{\Lob(M)}{x}$ by Löb induction. Thus, assume that

\[
f : \Later ((x : \Dec{A}) \to \Eq{\Dec{A}}{M(\Next(x))}{x} \to \Eq{\Dec{A}}{\Lob(M)}{x})
\]

If $x : A$ and $p : \Eq{\Dec{A}}{M(\Next(x))}{x}$, we calculate that

\begin{align*}
\Lob(M)
&= M(\Next(\Lob(M))) && \text{unfolding rule for $\Lob$}\\
&= M(\Next(x)) && \text{by Lemma \ref{lem:guarded:later-eq} on $\ZApp{\ZApp{f}{\Next(x)}{}}{\Next(p)}{} : \Later \Eq{\Dec{A}}{\Lob(M)}{x}$}\\
&= x && \text{by $p$}
\end{align*}

Thus, this type is inhabited by the term $\Lam[A]{\Lob(\Lam[f]{\Lam[x]{\Lam[p]{\Refl{x}}}})}$.

We can also use the Löb operator on the universe to form guarded recursive types. For
example, streams can be defined by[We denote modalities and their counterparts on the
universe by the same notation. For example, we may write $\Delta A$ to mean the type
$\IsTy{\Modify[\delta]{A}}[1]$ whenever $\IsTy[\LockCxV{\Gamma}<\delta>]{A}[1]$, but also to mean
the term $\IsTm{\Enc{\Modify[\delta]{\Dec{A}}}}{\Uni}$ whenever

:            →@ s

(A)              (([X]A ×X[Y]Y<ℓ>[1]))

$\Str$ maps a constant set,  a type $A \Mute{{}\mathop{@} s}$, to the type of streams over $A$,
which is again a constant set. This is done by first defining a timed set

\[
\IsTm[\LockCxV{\DeclVar{A}{\Uni}<1>}<\gamma>]{
\Str'(A) \defeq \Lob(\Lam[X]{\Disc A \times \Open{X}[Y]{\Later Y}<\ell>[1]})
\]

$\Str'(A)$ is defined by Löb induction: assuming $\DeclVar{X}{\Later \Uni^{1 \leq \ell}}<1>$ we
must define an element of the timed universe. This is given as the product of

* the set $A \Mute{{}\mathop{@} s}$, considered as a constant-everywhere timed set $\Delta A
\Mute{{}\mathop{@} t}$;

* a guarded recursive call, which represents the rest of the stream.

Recalling that $\Uni^{1 \leq \ell} = \Uni$, the second component is given by modal elimination.
Nevertheless, it is not immediate that the first component type-checks: we must show that

\[
\IsTm[\LockCxV{\LockCxV{\DeclVar{A}{\Uni}<1>}<\gamma>}<\delta>]{A}{\Uni}<s>
\]

But $\gamma \circ \delta = 1$, so the context is equal to $\LockCxV{\DeclVar{A}{\Uni}<1>}<1>$ and we
can use $A$. Unfolding the guarded fixed point, we have that

\[
\Str'(A) = \Disc{A} \times \Later \Str'(A) : U \Mute{{}\mathop{@} t}
\]

We apply $\Gamma$ to `totalize' this into the constant set $\Str(A) \Mute{{}\mathop{@} s}$ of
guarded streams.

Even though not immediately obvious, there is a serious advantage in expressing this definition in a
way that spans two modes. In previous work <cit.> the stream type $\Str(A)$ was
coinductive only if $A$ was provably a `constant set,'  if $A \Equiv \Box A$. Theorems about
streams had to carry around a proof of this equivalence. In our case, defining $\Str(A)$ at the mode
$s$ of constant sets automatically ensures that. Hence, $\Str(A)$ is equivalent to the familiar
definition, but we no longer need to propagate proofs of constancy.

$\Str(A)$ supports the following operations:

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\Cons &:& (A : \Uni) \to \Dec{A} \to \Dec{\Str(A)} \to \Dec{\Str(A)} \Mute{{}\mathop{@} s}\\
\Cons_A(h, t) &\defeq& \Open{t}[t']{\MkBox[\gamma]{\Pair{\MkBox[\delta]{h}}{\Next(t')}}}<\gamma>[1]\\[0.3cm]
\Head &:& (A : \Uni) \to \Dec{\Str(A)} \to \Dec{A} \Mute{{}\mathop{@} s} \\
\Head_A(s) &\defeq& \Open{s}[s']{\Triv*{\MComp{\MkBox[\gamma]{\Proj[0]{s'}}}{\gamma}{\delta}}}<\gamma>[1]\\[0.3cm]
\Tail &:& (A : \Uni) \to \Dec{\Str(A)} \to \Dec{\Str(A)} \Mute{{}\mathop{@} s} \\
\Tail_A(s) &\defeq& \Open{s}[s']{\MComp{\MkBox[\gamma]{\Proj[1]{s'}}}{\gamma}{\ell}}<\gamma>[1]
\end{array}
\]

Those familiar with prior work on guarded streams may be surprised by the type of $\Tail$. The
expected definition would be

\[
\Tail_A(s) \stackrel{?}{=} \Open{s}[s']{\MkBox[\gamma]{\Proj[1]{s'}}}<\gamma>[1]
\]

This term has type $\Dec{\Str(A)} \to \GSec(\Later \Dec{\Str'(A)})$. However, in our case the
$\GSec$ modality is sufficiently strong to “absorb” this extra $\Later$: the equality $\gamma
\circ \ell = \gamma$ induces an equivalence $\GSec \circ \Later \simeq \GSec$, which we use to
obtain the version given above. This small difference is crucial: it will internally make $\Str(A)$
into a final coalgebra!

These operations satisfy the expected $\beta$ and $\eta$ laws,

* $(h : \Dec{A})(t : \Dec{\Str(A)}) \to \Eq{\Dec{A}}{\Head_A(\Cons_A(h, t))}{h} \Mute{{}\mathop{@} s}$

* $(h : \Dec{A})(t : \Dec{\Str(A)}) \to \Eq{\Dec{\Str(A)}}{\Tail_A(\Cons_A(h, t))}{t} \Mute{{}\mathop{@} s}$

* $(h : \Dec{A})(t : \Dec{\Str(A)}) \to \Eq{\Dec{\Str(A)}}{s}{\Cons_A(\Head_A(s), \Tail_A(s))}\Mute{{}\mathop{@} s}$

We prove (2), the other two being similar. If $h : \Dec{A}$ and $t : \Dec{\Str(A)}$, note that $\Dec{\Str(A)}$ is a type of the form $\Gamma(-)$, and calculate that

\begin{align*}
&\ \Tail_A(\Cons_A(h, t)) && \\
&= \Tail_A(\Cons_A(h, \MkBox[\gamma]{t'}))
&& \text{write $t = \MkBox[\gamma]{t'}$ by modal induction}\\
% &= \Tail_A(\Open{\MkBox[\gamma]{t'}}[x]{\MkBox[\gamma]{\Pair{\MkBox[\delta]{h}}{\Next(x)}}}<\gamma>[1])\\
&= \Tail_A(\MkBox[\gamma]{\Pair{\MkBox[\delta]{h}}{\Next(t')}}) && \\
% &= \Open{\MkBox[\gamma]{\Pair{\MkBox[\delta]{h}}{\Next(t')}}}[s']{\MComp{\MkBox[\gamma]{\Proj[1]{s'}}}{\ell}{\gamma}}<\gamma>[1]\\
&= \MComp{\MkBox[\gamma]{\Proj[1]{\Pair{\MkBox[\delta]{h}}{\Next(t')}}}}{\gamma}{\ell} &&\\
&= \MComp{\MkBox[\gamma]{\Next(t')}}{\gamma}{\ell} && \\
&= \MkBox[\gamma]{t'}
&&\text{as $\gamma \circ \ell = \gamma$}\\
&= t && \qedhere
\end{align*}

$\Str(A)$ is the final coalgebra for $\Lam[X]{\Dec{A} \times X} : \Uni \to \Uni \Mute{{}\mathop{@} s}$.

Given $A : \Uni$ we define a coalgebra $\Uncons : \Str(A) \to (\Dec{A} \times \Str(A)) \Mute{{}\mathop{@} s}$ by

\[
\Uncons(s) \defeq \Pair{\Head_A(s)}{\Tail_A(s)}
\]

To show finality, suppose $c : B \to \Dec{A} \times B \Mute{{}\mathop{@} s}$ is another
coalgebra. We define a function $f : B \to \Str(A) \Mute{{}\mathop{@} s}$ by

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
f' &:& \Disc B \to \Dec{\Str'(A)} \Mute{{}\mathop{@} t}\\
f' &\defeq& \Lob(\Lam[f', x]{\Open{x}[x']{\Pair{h}{t}}<\delta>[1]})\\
&&\text{where }       h = \MkBox[\delta]{\Proj[0]{c(x')}}\\
&&\text{and}\quad\;\, t = {\ZApp{f'}{\Next(\MkBox[\delta]{\Proj[1]{c(x')}})}{\ell}}\\[0.3cm]
f &:& B \to \Dec{\Str(A)} \Mute{{} \mathop{@} s}\\
f(x) &\defeq& \MkBox[\gamma]{f'(\MkBox[\delta]{x})}
\end{array}
\]

This is a morphism of coalgebras: for any $x : B$ we have

\begin{align*}
\Uncons(f(x))
&= \Pair{\Head_A(f(x))}{\Tail_A(f(x))}\\
&= \Pair{\Proj[0]{c(x)}}{\Tail_A(f(x))}\\
&= \Pair{\Proj[0]{c(x)}}{\MComp{\MkBox[\gamma]{\Proj[1]{f'(x)}}}{\gamma}{\ell}}\\
&= \Pair{\Proj[0]{c(x)}}{\MComp{\MkBox[\gamma]{\ZApp{\Next(f')}{\Next(\MkBox[\delta]{\Proj[1]{c(x)}})}{\ell}}}{\gamma}{\ell}}\\
&= \Pair{\Proj[0]{c(x)}}{f(\Proj[1]{c(x)})}
\end{align*}

Finally, we must show that $f$ is the unique coalgebra morphism. Suppose we are given
$g : B \to \Dec{\Str(A)} \Mute{{}\mathop{@} s}$ which also satisfies
$\Uncons(g(x)) = \Pair{\Proj[0]{c(x)}}{g(\Proj[1]{c(x)})}$. We `shift' this definition to timed sets, by defining

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\hat{g}    &:& \Disc{B} \to \Dec{\Str'(A)} \Mute{{}\mathop{@} t} \\
\hat{g}(x) &\defeq& \Coe{\ZApp{\MkBox[\delta]{g} }{x}{\delta}}{\delta \circ \gamma}{1}
\end{array}
\]

It suffices to show that $\hat{g} = f' \Mute{{}\mathop{@} t}$, and we do so by Löb induction and
function extensionality. Assume $p : \Later \Eq{}{\hat{g}}{f'}$, and $x : \Disc B$. To prove
$\hat{g}(x) = f'(x) : \Disc B \times \Later \Str'(A)$ it suffices to show componentwise equality.
By modal induction write $x = \MkBox[\delta]{y}$ for $y : B$.

First, we have that $\Proj[0]{f'(\MkBox[\delta]{y})} = \MkBox[\delta]{\Proj[0]{c(y)}}$ by the definition of $f'$. On the other hand, we have that

\[
\Proj[0]{\hat{g}(\MkBox[\delta]{y})}
= \Proj[0]{\Coe{\MkBox[\delta]{g(y)}}{\delta \circ \gamma}{1}}
= \Proj[0]{g_x} : \Disc B \Mute{{}\mathop{@} t}
\]

where we have used modal induction to write $g(y) = \MkBox[\gamma]{g_x}$. That  $g$ is a coalgebra
morphism implies that $\Head(g(y)) = \Proj[0]{c(y)}$. If we now use modal induction to write
$\Proj[0]{g_x} = \MkBox[\delta]{b}$ for $b : B$ and unfold the definition of $\Head$, we obtain $b
= \Proj[0]{c(y)}$, so $\Proj[0]{g_x} = \MkBox[\delta]{b} = \MkBox[\delta]{\Proj[0]{c(y)}}$, which shows
that the two first components are equal.

For the second component, we compute that

\begin{align*}
&\Proj[1]{f'(\MkBox[\delta]{y})} & \\
&= \ZApp{\Next(f')}{\Next(\MkBox[\delta]{\Proj[1]{c(y)}}))}{\ell} & \\
&= \Next(f'(\MkBox[\delta]{\Proj[1]{c(y)}})) & \\
&= \Next(\hat{g}(\MkBox[\delta]{\Proj[1]{c(y)}}))
& \text{using $p$ through Lemma \ref{lem:guarded:later-eq}}\\
&= \Next(\Coe{\MkBox[\delta]{g(\Proj[1]{c(x)})}}{\delta \circ \gamma}{1}) & \\
&= \Next(\Coe{\MkBox[\delta]{\Tail(g(y))}}{\delta \circ \gamma}{1})
& \text{as $g$ is a coalgebra morphism} \\
&= \Proj[1]{\Coe{\MkBox[\delta]{g(y)}}{\delta \circ \gamma}{1}}
& \text{lemma} \\
&= \Proj[1]{\hat{g}(x)}
\end{align*}

The lemma referred to above is the fact that for any $s : \Str(A)$ it is the case that

\[
\Next(\Coe{\MkBox[\delta]{\Tail(s)}}{\delta \circ \gamma}{1})
= \Proj[1]{\Coe{\MkBox[\delta]{s}}{\delta \circ \gamma}{1}}
\]

which can be shown by a series of modal inductions.

We conclude this section by showing how to use use these mechanisms in order to prove properties of
coinductive programs. Specifically, we will replicate a proof from <cit.> which shows
that the  operator on streams preserves commutativity. Let

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\ZipWith' &:& \Disc (\Dec{A} \to \Dec{B} \to \Dec{C}) \to \Dec{\Str'(A)} \to \Dec{\Str'(B)} \to \Dec{\Str'(C)}\\
\ZipWith'(f) &\defeq&%
\Lob(%
\Lam[r]{
\Lam[x, y]{%
\Pair{
\ZApp{\ZApp{f}{\Proj[0]{x}}{\delta}}{\Proj[0]{y}}{\delta}
\ZApp{\ZApp{r}{\Proj[1]{x}}{\ell}}{\Proj[1]{y}}{\ell}
\ZipWith &:& (\Dec{A} \to \Dec{B} \to \Dec{C}) \to \Dec{\Str(A)} \to \Dec{\Str(B)} \to \Dec{\Str(C)}\\
\ZipWith(f) &\defeq& \Lam[x, y]{\ZApp{\ZApp{\MkBox[\gamma]{\ZipWith'(\MkBox[\delta]{f})}}{x}{\gamma}}{y}{\gamma}}
\end{array}
\]

Take note of a useful pattern for programming with guarded recursion, which is visible both here
and in the proof of Theorem <ref>. We first define an auxiliary
function in mode $t$, which uses Löb induction. The main function itself is then just a thin
wrapper which `corrects' that with the appropriate modalities and modal combinators.

If $f$ is commutative then $\ZipWith(f)$ is commutative. That is, given $A, B : \Uni$ and
$f : \Dec{A} \to \Dec{A} \to \Dec{B}$ there is a term of the following type:

\begin{align*}
((x, y &: \Dec{A}) \to \Eq{\Dec{B}}{f(x, y)}{f(y, x)}) \to{}\\
&(s, t : \Dec{\Str(A)}) \to \Eq{\Dec{\Str(B)}}{\ZipWith(f, s, t)}{\ZipWith(f, t, s)}
\end{align*}

Suppose $e : (x, y : \Dec{A}) \to \Eq{\Dec{B}}{f(x, y)}{f(y, x)}$ and $s, t : \Dec{\Str(A)}$. We
wish to show that $\ZipWith(f, s, t) = \ZipWith(f, t, s)$. By the definition of $\ZipWith$, it is sufficient to prove that for any $u, v : \Dec{\Str'(A)}$ we have

\[
\ZipWith'(\MkBox[\delta]{f}, u, v)
= \ZipWith'(\MkBox[\delta]{f}, v, u)
\]

In turn, it suffices to show that

\[
\Lob(F_0) = \Lob(F_1)
\]

\begin{align*}
F_0 &\defeq \Lam[r]{\Lam[x, y]{
\Pair{
\ZApp{\ZApp{\MkBox[\delta]{f}}{\Proj[0]{x}}{\delta}}{\Proj[0]{y}}{\delta}
\ZApp{\ZApp{r}{\Proj[1]{\Alert{x}}}{\ell}}{\Proj[1]{\Alert{y}}}{\ell}
}} \\
F_1 &\defeq \Lam[r]{\Lam[x, y]{
\Pair{
\ZApp{\ZApp{\MkBox[\delta]{f}}{\Proj[0]{y}}{\delta}}{\Proj[0]{x}}{\delta}
\ZApp{\ZApp{r}{\Proj[1]{\Alert{y}}}{\ell}}{\Proj[1]{\Alert{x}}}{\ell}
\end{align*}

because then

\[
\ZipWith'(\MkBox[\delta]{f}, v, u)
\defeq
\Lob(F_0)(u, v)
\Lob(F_1)(u, v)
\ZipWith'(\MkBox[\delta]{f}, u, v)
\]

By Theorem <ref> we know guarded fixed points are
unique, so it suffices to show that

\begin{equation}
\Lob(F_1) = F_0(\Next(\Lob(F_1)))
\label{eq:guarded-recursion:goal}
\end{equation}

We use Löb induction to construct a term of type $\Eq{}{\Lob(F_1)}{F_0(\Next(\Lob(F_1)))}$.

\begin{align*}
&F_0(\Next(\Lob(F_1))) \\
&= \Lam[x,y]{\Pair{\ZApp{\ZApp{\MkBox[\delta]{f}}{\Proj[0]{x}}{\delta}}{\Proj[0]{y}}{\delta}}{\ZApp{\ZApp{\Next(\Lob(F_1))}{\Proj[1]{x}}{\ell}}{\Proj[1]{y}}{\ell}}}\\
&\qquad\qquad \text{by induction let $\MkBox[\delta]{a} \defeq \Proj[0](x)$ and $\MkBox[\delta]{b} \defeq \Proj[0](y)$} \\
&= \Lam[x,y]{\Pair{\MkBox[\delta]{f(a, b)}}{\ZApp{\ZApp{\Next(\Lob(F_1))}{\Proj[1]{x}}{\ell}}{\Proj[1]{y}}{\ell}}}\\
&= \Lam[x,y]{\Pair{\MkBox[\delta]{f(b, a)}}{\ZApp{\ZApp{\Next(\Lob(F_1))}{\Proj[1]{x}}{\ell}}{\Proj[1]{y}}{\ell}}}\\
&= \Lam[x,y]{\Pair{\MkBox[\delta]{f(b, a)}}{\ZApp{\ZApp{\Next(F_1(\Next(\Lob(F_1))))}{\Proj[1]{x}}{\ell}}{\Proj[1]{y}}{\ell}}}\\
&\qquad\qquad \text{by induction let $\MkBox[\ell]{s} \defeq \Proj[1]{x}$ and $\MkBox[\ell]{t} \defeq \Proj[1]{y}$}\\
% &= \Lam[x,y]{\Pair{\MkBox[\delta]{f(b, a)}}{\ZApp{\ZApp{\Next(\Lob(F_1))}{\MkBox[\ell]{s}}{\ell}}{\MkBox[\ell]{t}}{\ell}}}\\
&= \Lam[x,y]{\Pair{\MkBox[\delta]{f(b, a)}}{\Next(F_1(\Next(\Lob(F_1))(s, t))}}\\
&= \Lam[x,y]{\Pair{\MkBox[\delta]{f(b, a)}}{\Next(F_0(\Next(\Lob(F_1))(t, s))}}\\
&= \Lam[x,y]{\Pair{\MkBox[\delta]{f(b, a)}}{\ZApp{\ZApp{\Next(F_0(\Next(\Lob(F_1))))}{\Proj[1]{y}}{\ell}}{\Proj[1]{x}}{\ell}}}\\
&\qquad\qquad \text{using the IH through Lemma \ref{lem:guarded:later-eq}}\\
&= \Lam[x,y]{\Pair{\MkBox[\delta]{f(b, a)}}{\ZApp{\ZApp{\Next(\Lob(F_1))}{\Proj[1]{y}}{\ell}}{\Proj[1]{x}}{\ell}}}\\
&= \Lam[x,y]{\Pair{\ZApp{\ZApp{\MkBox[\delta]{f}}{\Proj[0]{y}}{\delta}}{\Proj[0]{x}}{\delta}}{\ZApp{\ZApp{\Next(\Lob(F_1))}{\Proj[1]{y}}{\ell}}{\Proj[1]{x}}{\ell}}}\\
&= \Lob(F_1) \qedhere
\end{align*}

Using guarded type theories to reason about coinduction has been a problem for some time. The type
theory gDTT of <cit.> also featured Löb induction. However, in
gDTT the problem of `totalising' a type—which corresponds to reasoning by
coinduction—was not handled through the `always' modality, but by using the technical device of
clocks <cit.>. In essence, gDTT does not come with a single $\Later$
modality, but rather with a collection of them, each one indexed by a clock name. There is a
quantifier which allows clock names to be bound inside a particular type, and a crucial

\[
\forall \kappa.\ A \cong \forall \kappa.\ \Later^\kappa A
\TagEq[$\ast$] \label{eq:guarded-recursion:clock-force-iso}
\]

gDTT suffers from several technical complications. The syntactic problems pertaining to
delayed substitutions were resolved by the introduction of Clocked Type Theory (CloTT)
<cit.>, which uses additional judgmental structure. It is conjectured that
type-checking is decidable for CloTT.

The complexity of using clocks is not merely on the syntactic level: it also appears in the
semantics of clocked type theory. CloTT is modelled in a collection of presheaf categories, with
multiple functors navigating between them <cit.>. While this model is
well-understood, it was hoped that some of the complexity could be circumvented by replacing
clocks with a modality. This led <cit.> to introduce the comonadic `always'
modality $\Box$, which replaced the isomorphism (<ref>) with
$\Box \Later A \cong \Box A$.

The main advantage of using $\Box$ is that it can be interpreted in $\PSH{\omega}$, which is a
much simpler model. On the other hand, the interactions between $\Box$ and $\Later$ have proven
difficult to capture in the syntax. In fact, the mere addition of $\Box$ to a dependent type
theory poses a significant technical challenge:
see <cit.>. Despite this concentrated
effort, there are still serious technical obstacles to adding $\Later$ to a type theory for
$\Box$.  is the first syntax to accomodate both $\Box$, $\Later$, and validate $\Box \Later
A \cong \Box A$.

§ INTERNAL ADJOINTS

In many cases of interest, the need for a pair of adjoint modalities arises: we would like a
pair of modalities $\mu : n \to m$ and $\nu : m \to n$ so that, in some sense,

\[
\Modify[\nu]{-} \Adjoint \Modify{-}
\]

But what does it mean to have an adjunction between two modalities within ? Does it
correspond to an external adjunction? And do all known results from category theory apply? The only
thing that is certain is that this scenario is fundamental to modal type theory, as a number of
intended models can be elegantly presented through
adjunctions <cit.>.

In this section we show that when  equipped with the walking adjunction as a mode
theory it becomes a useful syntax for reasoning about adjoint modalities. Of course, the adjoint
modalities themselves are not exactly adjoint functors: they are something slightly weaker than
DRAs, whose `left adjoints' constitute an adjunction. Nevertheless, we prove that the induced
modalities largely behave as expected: the unit and counit are internally definable; some limited
forms of internal transposition can be recovered; and left adjoints preserve colimits, as expressed
through crisp induction principles.

§.§ The walking adjunction

As ever, we begin by freely defining a mode theory $\ModeAdj$. Its generators are two 1-cells $\nu :
m \to n$ and $\mu : n \to m$, and two 2-cells

\begin{align*}
\eta &: 1_m \To \mu \circ \nu
\epsilon &: \nu \circ \mu \To 1_n
\end{align*}

subject to the triangle equations

\[
\begin{tikzcd}
\mu
\arrow[r, Rightarrow, "{\eta \Whisker 1_\mu}"]
\arrow[dr, equal]
& \mu \circ \nu \circ \mu
\arrow[d, Rightarrow, "{1_\mu \Whisker \epsilon}"]
\\
% empty
& \mu
\end{tikzcd}
\quad
\begin{tikzcd}
\nu
\arrow[r, Rightarrow, "{1_\nu \Whisker \eta}"]
\arrow[dr, equal]
& \nu \circ \mu \circ \nu
\arrow[d, Rightarrow, "{\epsilon \Whisker 1_\nu}"]
\\
% empty
& \nu
\end{tikzcd}
\]

$\ModeAdj$ is sometimes called the walking adjunction <cit.>. It is the
classifying 2-category for an adjunction: 2-functors $\Mor{\ModeAdj}{\CC}$ correspond
precisely to (2-categorical) adjunctions in $\CC$.

The mode theory $\ModeAdj$ has a very curious property: it is self-dual,  there is an
equivalence $\Coop{\ModeAdj} \Equiv \ModeAdj$. This equivalence is witnessed by swapping the modes,
the left and right adjoints, and the unit and counit.

§.§ Models of adjoint modalities

Recall that a modal context structure of a model of  with mode theory $\ModeAdj$ is a strict
2-functor $\Interp{-} : \Coop{\ModeAdj} \to \CAT$. The self-duality of $\ModeAdj$ implies that such
a context structure consists of two categories and an adjunction between them. We immediately obtain
the following result.

If $\CC$ and $\DD$ carry models of , and there is a pair of dependent right adjoints
between them whose `left adjoints' are themselves adjoint, then we can construct a model of
with mode theory $\ModeAdj$.

Write $\InterpModal{\nu} : \CC \to \DD$ and $\InterpModal{\mu} : \DD \to \CC$ for the functors
given as part of the DRAs. The notation is then suggestive: $\InterpModal{\nu} \Adjoint
\InterpModal{\mu}$, and Theorem <ref> applies.

Any model of $\ModeAdj$ must interpret $\InterpModal{\nu}$ and $\InterpModal{\mu}$ as adjoint
functors. Moreover, if $\CModify[\mu]$ and $\CModify[\nu]$ are induced by the adjunctions
$\InterpModal{\mu} \Adjoint R_\mu$ and $\InterpModal{\nu} \Adjoint R_\nu$ lifted to a dependent
right adjoints (by Lemma <ref>), then $R_\nu \Adjoint

Adjoint functors are precisely adjoint morphisms in the 2-category $\CAT$. As $\ModeAdj$ is the
walking adjunction, and 2-functors preserve adjunctions, we have that $\InterpModal{\nu} \Adjoint
\InterpModal{\mu}$.

If $\InterpModal{\nu} \Adjoint R_\nu$ and the interpretation of $\Modify[\nu]{-}$ is given by
using Lemma <ref> to lift the right adjoint to types and
terms, then by the uniqueness of adjoint pairs we must have that $R_\nu \cong \InterpModal{\mu}$.
If moreover $\InterpModal{\mu} \Adjoint R_\mu$, and $\Modify{-}$ is also induced by $R_\mu$, then
$R_\nu \Adjoint R_\mu$.

The last situation in this lemma is sometimes known as an `adjunction of adjunctions' <cit.>. In particular, it is one of the rare cases where the action of the left adjoint
$\InterpModal{\nu}$ is in some sense internalized on types and terms by the modality corresponding
to its right adjoint, viz. $\Modify{-}$.

§.§ Recovering the adjunction internally

The foregoing construction of a model interpreted the lock functors required by $\ModeAdj$ by an
adjunction. Consequently, substitutions $\Delta \to \LockCx{\Gamma}$ are in natural bijection with
substitutions $\LockCx{\Delta}<\nu> \to \Gamma$. We would like to strengthen this setting by
bootstrapping this adjunction into an internal adjunction.

It is not immediately clear what an internal adjunction should be. However, we can construct an
appropriate definition by internalizing the unit and counit as functions. But that is not immediate
either: if $\IsTy{A}[1]$, the construction $\Modify[\mu]{\Modify[\nu]{A}}$ that we would naïvely
try as the codomain of the unit is ill-typed. This can be mended through key substitutions. Recall
that $\eta : 1_m \To \mu \circ \nu$. The corresponding key substitution at $\Gamma
\Mute{{}\mathop{@} m}$ is $\Key{\eta}{\Gamma} : \LockCxV{\Gamma}<\mu \circ \nu> \to \Gamma
\Mute{{}\mathop{@} m}$. We can use this to formally define the notation of
<ref> by

\[
A^\eta \defeq \Sb{A}{\Key{\eta}{\Gamma}}
\]

As substitutions can be eliminated (e.g. through a subset of the canonicity algorithm), this defines
an admissible operation from type $\IsTy{A}[1]$ to type $\IsTy[\LockCxV{\Gamma}<\mu \circ
\nu>]{A^\eta}[1]$. We can thus define the unit component at $\IsTy{A}[1]$ by

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\Unit    &:&      A \to \Modify[\mu]{\Modify[\nu]{A^\eta}} \Mute{{}\mathop{@} m} \\
\Unit(x) &\defeq& \MkBox[\mu]{\MkBox[\nu]{x^\eta}}
\end{array}
\]

Dually, for any type $\IsTy[\LockCxV{\Gamma}<\nu \circ \mu>]{A}[1]<n>$ we can define the counit
component by

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\Counit    &:& \Modify[\nu]{\Modify[\mu]{A}} \to A^\epsilon \Mute{{}\mathop{@} n} \\
\Counit(x) &\defeq& \Open{x}[y_0]{\Open{y_0}[y_1]{y_1^\epsilon}<\mu>[\nu]}<\nu>[1]
\end{array}
\]

We thus obtain the unit and counit internally, but the types of the components have to be adjusted
in the presence of dependence. Moreover, we can prove internal versions of the triangle equations;
they are given by modal induction:

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\_ &:& (x : \Modify[\nu]{A}) \to \Id{\Modify[\nu]{A}}{x}{\Counit(\ZApp{\MkBox[\nu]{\Unit}}{x}{\nu})}\\
\_ &\defeq& \Lam[x]{\Open{x}[y]{\Refl{\MkBox[\nu]{y}}}<\nu>[1]}\\[0.3cm]
\_ &:& (x : \Modify[\mu]{A}) \to \Id{\Modify[\mu]{A}}{x}{\ZApp{\MkBox[\mu]{\Counit}}{\Unit(x)}{\mu}}\\
\_ &\defeq& \Lam[x]{\Open{x}[y]{\Refl{\MkBox[\mu]{y}}}<\mu>[1]}
\end{array}
\]

The most difficult part is proving that these terms are well-typed. For example, in the first
instance we must show that $\MkBox[\nu]{y} =
\Counit(\ZApp{\MkBox[\nu]{\Unit}}{\MkBox[\nu]{y}}{\nu})$ definitionally:

\begin{align*}
\Counit(\ZApp{\MkBox[\nu]{\Unit}}{\MkBox{y}}{\nu})
&= \Counit(\MkBox[\nu]{\App{\Unit}{y}})\\
&= \Counit(\MkBox[\nu]{\MkBox[\mu]{\MkBox[\nu]{y^\eta}}})\\
&= \MkBox[\nu]{y^\eta}^\epsilon\\
&= \MkBox[\nu]{(y^\eta)^{\epsilon \Whisker 1_\nu}}\\
&= \MkBox[\nu]{y^{(\epsilon \Whisker 1_\nu) \circ (1_\nu \Whisker \eta)}}\\
&= \MkBox[\nu]{y}
\end{align*}

Because we are using slightly informal syntax here, it is difficult to see that the steps that
introduce whiskering are correct. They become much more perspucious if we expand
$\MkBox[\nu]{y^\eta}^\epsilon$ into algebraic syntax, and use the last equation of
Fig. <ref> twice to absorb locks:

\[
\Sb{\MkBox[\nu]{\Sb{y}{\Key{\eta}{\LockCx{\Gamma}<\nu>}}}}{\Key{\epsilon}{\Gamma}}
= \MkBox[\nu]{\Sb{y}{\Key{\eta}{\LockCx{\Gamma}<\nu>} \circ \LockSb{\Key{\epsilon}{\Gamma}}<\nu>}}
= \MkBox[\nu]{\Sb{y}{\Key{1_\nu \Whisker \eta}{\Gamma} \circ \Key{\epsilon \Whisker 1_\nu}{\Gamma}}}
= \MkBox[\nu]{\Sb{y}{\Key{1_\mu}{\Gamma}}}
\]

§.§ Internal transposition

The previous section offers a perfectly good internal representation of an external adjunction.
However, it is usually much more economical to present an adjunction by a natural isomorphism

\[
\Hom{L(A)}{B} \cong \Hom{A}{R(B)}
\]

Unfortunately, this is not achievable in  for a multitude of reasons. First, notice that
$\Modify[\nu]{A} \to B  \Mute{{}\mathop{@} n}$ and $A \to \Modify{B} \Mute{{}\mathop{@} m}$ are
types in different modes, so the putative type $(\Modify[\nu]{A} \to B) \Equiv (A \to \Modify{B})$
that would represent the isomorphism is ill-typed.

Second, even if the two modes coincide—so that $\nu, \mu$ are endomodalities—the aforementioned
type is a bit too strong for our purpose: it is inhabited by internal equivalences, which are
stronger than bijections of hom-sets. Such equivalences correspond to isomorphisms $B^{L(A)} \cong
R(B)^A$ of exponential objects. In turn, these are equivalent to hom-set bijections only if the
involved functors are internal, which is to say that we have functions

\begin{align*}
(A \to B) &\to (\Modify[\nu]{A} \to \Modify[\nu]{B})
(A \to B) &\to (\Modify{A} \to \Modify{B})
\end{align*}

that compute the action of the modality $\Modify{-}$ on morphisms within .[Such functors are usually called enriched (recall that cartesian closure is a self-enrichment).]

Third, even if we could internalize our modalities, we would be flying too close to the sun. As we
have $(1 \to A) \Equiv A$ for any $A$ and $\Modify[\xi]{1} \Equiv 1$ for any $\xi$, we may calculate

\[
A\ \Equiv\ 1 \to A\ \Equiv\ \Modify[\nu]{1} \to A\ \Equiv\ 1 \to \Modify{A}\ \Equiv\ \Modify{A}
\]

Hence, $\Modify{-}$ must be the identity functor up to equivalence. This short argument, which is
due to <cit.>, is a no-go theorem that obstructs the
internalization of an adjunction whose left adjoint preserves terminal objects.

<cit.> overcame this barrier by introducing the global sections
modality $\flat$. Terms of $\Box A$ represent global elements of $A$: terms of $\flat(A \to
B)$ are in bijection with morphisms in $\Hom{A}{B}$. Thus, the previously problematic equivalence
holds under $\flat$.

We can rephrase this argument in our syntax. The key thing to notice is that the functor $\flat :
\PSH{\CC} \to \PSH{\CC}$ which maps a presheaf to the constant presheaf $\_ \mapsto
\Hom[\PSH{\CC}]{1}{P}$ of global sections is initial amongst functors that preserve the terminal
object. Thus, we postulate an initial modality: suppose that $n = m$, and that $\Hom{m}{m}$ is
equipped with an initial object,  a 1-cell $\flat : m \to m$ and a unique 2-cell ${!} : \flat \To
\xi$ for all $\xi$. As a consequence, we are able to use variables $\DeclVar{x}{A}<\flat>$ in any
context. Assuming function extensionality, we have that

There is an equivalence $\Modify[\flat]{\Modify[\nu]{A^{!}} \to B} \Equiv \Modify[\flat]{A \to
\Modify{B^{!}}}$.

The equivalence is given by the functions

\[
\arraycolsep=1.4pt
\begin{array}{lclclcl}
F & : & \Modify[\flat]{\Modify[\nu]{A^{!}} \to B} \to \Modify[\flat]{A \to
\Modify{B^{!}}} \\
F(f) &\defeq& \Open{f}[g]{\MkBox[\flat]{\Lam[x]{\ZApp{\MkBox[\mu]{g^!}}{\Unit(x)}{\mu}}}}<\flat>[1] \\[0.3cm]
G &:& \Modify[\flat]{A \to \Modify{B^{!}}} \to \Modify[\nu]{A} \to\Modify[\flat]{\Modify[\nu]{A^{!}} \to B}\\
G(g)&\defeq& \Open{g}[f]{\MkBox[\flat]{\Lam[x]{\Counit(\ZApp{\MkBox[\nu]{f^!}}{x}{\nu})}}}<\flat>[1]
\end{array}
\]

These are well-typed because, by initiality of $\flat$, $A^\eta = (A^{!})^\eta = A^!$,
$(B^!)^\epsilon = B^!$. By function extensionality and $\eta$ for modalities, they are mutually

The closest we can get to defining internal transposition (without using an initial modality)
amounts to the following two functions.

\[
\arraycolsep=1.4pt
\begin{array}{lclclcl}
\TranspAdj{\nu}{\mu} & : & \Modify[\mu]{\Modify[\nu]{A^\eta} \to B} \to A \to \Modify{B} \\
\TranspAdj{\nu}{\mu} &\defeq& \Lam[f]{\Lam[x]{\ZApp{f}{\Unit(x)}{\mu}}} \\[0.3cm]
\UntranspAdj{\nu}{\mu} &:& \Modify[\nu]{A \to \Modify{B}} \to \Modify[\nu]{A} \to B^\epsilon\\
\UntranspAdj{\nu}{\mu} &\defeq& \Lam[f]{\Lam[x]{\Counit(\ZApp{f}{x}{\nu})}}
\end{array}
\]

Both of these are equivalences, but they do not have the right type.

§.§ Crisp induction

Having internalized the definition of an adjunction, it is natural to ask whether standard facts about adjoint functors carry over. In this section we prove an internal version of the fact that left adjoints preserve colimits. Within type theory this result takes the form of crisp induction principles for various types that arise from colimits.

As a first approximation to the notion of crisp induction, recall the rule for modal induction, i.e. the elimination rule for modal types from <ref>:

\[
\inferrule{
\mu : n \to m \\
\nu : m \to o \\
\IsTy[\ECxV{\Gamma}{x}{\Modify[\mu]{A}}<\Alert{\nu}>]{B}[1]<o> \\\\
\IsTm[\LockCxV{\Gamma}<\Alert{\nu}>]{M_0}{\Modify[\mu]{A}}<m> \\
\IsTm[\ECxV{\Gamma}{x}{A}<\Alert{\nu} \circ \mu>]{M_1}{\Sb{B}{\MkBox[\mu]{x}/x}}<o>
\IsTm{\Open{M_0}[x]{M_1}<\mu>[\Alert{\nu}]}{\Sb{B}{M_0/x}}<o>
\]

Notice that there is an “extra” modality parameterizing this rule, $\nu$, which modifies $M_0$ as
well as the data supplied to $M_1$. This extra generality is not frivolous: we can only define the
equivalence $\MComp{}{\mu}{\nu}$ of <ref> because we can eliminate one
modality `under' another.

One might hope for a similar level of flexibility in all positive eliminators. However, the
elimination rule for booleans—stated here in its algebraic form of
<ref>—does not allow it:

\[
\inferrule{
\IsCx{\Gamma}\\
\IsTy[\ECx{\Gamma}{\Bool}<\Alert{1}>]{A}[1]\\
\IsTm{M_t}{\Sb{A}{\ESb{\ISb}{\True}}}\\
\IsTm{M_f}{\Sb{A}{\ESb{\ISb}{\False}}}\\
\IsTm[\LockCx{\Gamma}<\Alert{1}>]{N}{\Bool}
\IsTm{\BoolRec{A}{M_t}{M_f}{N}}{\Sb{A}{\ESb{\ISb}{N}}}
\]

Were we to replace $1$ with an arbitrary modality, then this rule would state something considerably
stronger: not only would we have the expected elimination principle for $\Bool$, but all of our
modalities would preserve $\Bool$. Semantically, this is nonsense: modalities intuitively
correspond to right adjoints, and therefore do not necessarily preserve colimits. For example, the
later $\Later$ modality of <ref> does not preserve booleans.

Yet, in some circumstances—when a modality is a left adjoint—the stronger rule is valid.
This is the idea behind Shulman's crisp induction principles <cit.>: cohesive
type theory enables the proof of elimination principles for the coproducts and the identity type
under the left adjoint in the adjunction $\flat \Adjoint \sharp$. We will demonstrate that similar
principles are derivable within  with mode theory $\ModeAdj$.

Fix a motive $\IsTy[\ECxV{\LockCxV{\Gamma}<\nu \circ \mu>}{b}{\Bool}<\nu>]{C}[1]<n>$. Crisp
induction is given by a term

\[
\Gamma \vdash{} \CrispBoolRec_C :
(\DeclVar{b}{\Bool}<\nu>) \to
\Modify[\nu \circ \mu]{C(\True)} \to
\Modify[\nu \circ \mu]{C(\False)} \to
%\Sb{C}{\ESb{(\Key{\epsilon}{\Gamma} \circ \Wk)}{b}}
\Mute{{}\mathop{@} n}
\]

This is a well-formed type, as $\ECxV{\Gamma}{b}{\Bool}<\nu> =
\IsTy[\ECxV{\LockCxV{\Gamma}<1>}{b}{\Bool}<\nu>]{C^\epsilon}[1]$.

To obtain the crisp induction principle we first use the ordinary one at mode $n$, and apply a
number of modal combinators to bring it to mode $m$.

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\LockCxV{\Gamma}<\nu> \vdash{} h & : & (b : \Bool) \to \Modify{C(\True)} \to \Modify{C(\False)} \to \Modify{C(b^\eta)} \Mute{{}\mathop{@} m}\\
h(b, t, f) & \defeq & \BoolRec{b.\ \Modify{C(b^\eta)}}{t}{f}{b}\\[0.3cm]
\Gamma \vdash{} \CrispBoolRec_C & : &
(\DeclVar{b}{\Bool}<\nu>) \to
\Modify[\nu \circ \mu]{C(\True)} \to
\Modify[\nu \circ \mu]{C(\False)} \to
C^\epsilon(b) \Mute{{}\mathop{@} m}\\
\CrispBoolRec_C(b,t,f) & \defeq &
\Counit(\ZApp{\ZApp{\MkBox[\nu]{h(b)}}{\MComp*{t}{\nu}{\mu}}{\nu}}{\MComp*{f}{\nu}{\mu}}{\nu})
\end{array}
\]

The reasons why this term is well-typed is subtle. We have that
$\IsTm[\LockCxV{\ECxV{\LockCxV{\Gamma}<\nu>}{b}{\Bool}<1>}<\mu \circ \nu>]{b^\eta}{\Bool}<m>$, so
$\IsTy[\LockCxV{\ECxV{\LockCxV{\Gamma}<\nu>}{b}{\Bool}<1>}<\mu>]{C(b^\eta)}[1]<n>$ by the
application rule. Thus, $h$ is well-typed. It remains to show that $C(b^\eta)^\epsilon =
C^\epsilon(b)$, which intuitively follows from the triangle identities. We may show it by precisely
specifying what these operations mean in the algebraic syntax. First, we construct the substitutions

σ_0    <μ>0ηΓ<ν><1>
: Γ<ν><1><μ> →Γ<ν∘μ><ν> @ n

σ_1    <ν>0        : Γ<ν><ν∘μ> →Γ<ν><1><μ> @ n

σ_2    *ϵΓ ∘0        : Γ<ν> →Γ<ν∘μ><ν>
@ n

We can then interpret $C(b^\eta)$ as the type
$\IsTy[\LockCx{\ECx{\LockCx{\Gamma}<\nu>}{\Bool}<1>}<\mu>]{\Sb{C}{\sigma_0}}[1]<n>$. Similarly,
$C(b^\eta)^\epsilon$ is the type
Finally, $C^\epsilon(b)$ is the type $\IsTy[\ECx{\Gamma}{\Bool}<\nu>]{\Sb{C}{\sigma_2}}[1]<n>$, so
it suffices to show that $\sigma_0 \circ \sigma_1 \circ \Key{\epsilon}{\ECx{\Gamma}{\Bool}<\nu>} =
\sigma_2$. This is a monstrous equation which is primarily structural. Moreover, $\eta$ occurs in
$\sigma_0$, and $\epsilon$ in the key that follows it, so one of the triangle equations must
somehow be implicated. Indeed, we can use one of the two equations along with the rules of
<ref> to prove the desired result.

We can now prove that

$\Modify[\nu]{\Bool} \Equiv \Bool$

We define the two functions

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\BoolIso &:& \Modify[\nu]{\Bool} \to \Bool \Mute{{}\mathop{@} m}\\
\BoolIso(x) &\defeq& \Open{x}[y]{\CrispBoolRec_{\Bool}(y, \MkBox[\nu \circ \mu]{\True}, \MkBox[\nu \circ \mu]{\False})}<\nu>[1]\\[0.3cm]
\BoolIso* &:& \Bool \to \Modify[\nu]{\Bool} \Mute{{}\mathop{@} m}\\
\BoolIso* &\defeq& \Lam[x]{\BoolRec{\_.\ \Modify[\nu]{\Bool}}{\MkBox[\nu]{\True}}{\MkBox[\nu]{\False}}{x}}
% \_ & : & (b : \Modify[\nu]{\Bool}) \to \Id{\Modify[\nu]{\Bool}}{b}{\BoolIso*(\BoolIso(b))} \Mute{{}\mathop{@} m}\\
% \_(x) & \defeq & \Open{x}[x']{h(x')}<\nu>[1]\\
% && \text{where } h(x) \defeq
%       \CrispBoolRec_{b.\ \Id{\Modify[\nu]{\Bool}}{\MkBox[\nu]{b}}{\BoolIso*(h(b))}}(
%         \MkBox[\nu \circ \mu]{\Refl{\MkBox[\nu]{\True}}},
%         \MkBox[\nu \circ \mu]{\Refl{\MkBox[\nu]{\False}}},
%         x)
%       )\\[0.3cm]
% %
% \_ & : & (b : \Bool) \to \Id{\Bool}{b}{\BoolIso(\BoolIso*(b))} \Mute{{}\mathop{@} m}\\
% \_(x) & \defeq & \BoolRec{b.\ \Id{\Bool}{b}{\BoolIso(\BoolIso*(b))}}{\Refl{\True}}{\Refl{\False}}{x}
\end{array}
\]

We now use full crisp induction to construct for every $x : \Modify[\nu]{\Bool}$ a proof of
$\Id{\Modify[\nu]{\Bool}}{x}{\BoolIso*(\BoolIso(x))}$. First, use modal induction to write $x =
\MkBox[\nu]{y}$ for some $\DeclVar{y}{\Bool}<\nu>$. We then have to prove that
$\Id{\Modify[\nu]{\Bool}}{\MkBox[\nu]{y}}{\BoolIso*(\BoolIso(\MkBox[\nu]{y}))}$, so we perform
crisp induction on $y$. If $y \defeq \True$, we have that $\BoolIso*(\BoolIso(\MkBox[\nu]{\True}))
= \MkBox[\nu]{\True}$, so $\MkBox[\nu \circ \mu]{\Refl{\MkBox[\nu]{\True}}}$ has the right type.
The case for $y \defeq \False$ is similar. The other direction is simpler, and follows by induction on $\Bool$.

Similar results hold for other types with `positive,' `pattern-matching,' or `closed-scope'
elimination rules. For example, we can also formulate a crisp induction principle for identity
types, which can be used to prove that

$\Modify[\nu]{\Id{A}{M_0}{M_1}} \Equiv \Id{\Modify[\nu]{A}}{\MkBox[\nu]{M_0}}{\MkBox[\nu]{M_1}}$

§ RELATED WORK

Modal type theory has been an active area of research for two decades and, as with any active field,
a precise taxonomy of modal type theories would be a paper in and of itself. Accordingly, we have
not attempted such a task here, and have instead focussed on separating modal type theories into
distinct strands based on their judgmental structure. Some of our characterizations are slightly
artificial, in that these lines of work are not nearly so separate as we seem to suggest. We feel,
however, that this is the simplest way to position  in relation to current work.

§.§ Dual-context modal calculi

One of the first papers on (non-linear)[The idea of dual contexts arose in linear logic:
see <cit.>.] modal type theory was by
<cit.>, who constructed a proof theory for ,  a comonadic
modality. The central idea of this approach was to reflect the distinction between modal and
non-modal assumptions (referred to as `truth vs. validity' in op. cit.) in the judgmental
structure of the system itself.  The judgments for this calculus then contained not just a context
of true propositions, but rather two contexts: one for intuitionstic propositions, and one for
modal ones. Following this methodology, Davies and Pfenning internalized previously known patterns
of sequent calculus in a natural deduction style <cit.>.

This kind of judgment straightforwardly allows the incorporation of a product-preserving comonad.
The type $\Box A$ merely internalizes a restriction to modal contexts only:

Δ; ⊢A 𝗍𝗋𝗎𝖾

Δ; Γ⊢A 𝗍𝗋𝗎𝖾

A ∈Δ∪Γ
Δ; Γ⊢A 𝗍𝗋𝗎𝖾

Δ; Γ⊢A 𝗍𝗋𝗎𝖾

Δ, A; Γ⊢B 𝗍𝗋𝗎𝖾

Δ; Γ⊢B 𝗍𝗋𝗎𝖾

The second author showed that this pattern adapts well to the necessity fragment of a number of
normal modal logics <cit.>. The dual-context style has been succesfully adapted to
dependent types: see e.g. the work of <cit.>, and the spatial and cohesive type
theories of <cit.>. Similarly, contextual modal type
theory <cit.> has used a dual-context-like
structure in order to give a systematic account of higher-order abstract syntax.

<cit.> continues this program by formulating a precise categorical semantics
based on Awodey's natural models for a dependent type theory with either an adjunction
(AdjTT) or comonad (CoTT) <cit.>. The categorical semantics of
and AdjTT are closely related, though with minor differences in the precise
definition of the modality. For instance, in  only the $\Lock$ operator is required to act
upon the context, while in AdjTT the modalities themselves must extend to
contexts.[This is similar to the relation between a CwF+A and a CwDRA from
<cit.>, and we expect a similar relation to exist between the semantics of
with a single modality and AdjTT.] These differences arise because Zwanziger characterizes
only a certain, semantically well-behaved subclass of models, while in <ref> we
describe more general models, which also support the syntactic model and the gluing model of
<ref>. Syntactically, AdjTT is a multimode type theory that includes a
mode for both ends of the adjunction.

Despite these stories of success, the dual-context style is difficult to generalize: as the
complexity of the modal situation increases, so must the complexity of the context structure. For
instance, the structure of a dependent dual-context type theory enforces that a `modal' type (one
belonging to $\Delta$) may not depend on an `intuistionistic' type (one belonging to $\Gamma$). This
is a reasonable restriction in the case of $\Box$, but it is already somewhat limiting. For
instance, it should be allowed for a valid type to depend on a merely true $\Box A$. Making such an
adjustment would not only present a typographical problem (with a type occurring to the left of one
of its dependencies), it would render the introduction rule for $\Box A$ nonsensical.

This restriction proves even more difficult to manage once there is not merely one modality, but two
distinct modalities ones, say $\mu$ and $\nu$. Questions such as “should the $\mu$-modified types
be allowed to depend on $\nu$-modified types?” defy general answers. These questions can be
addressed for each specific modal situation. For example, both <cit.> and
<cit.> hand-craft a system for two modalities. However, these constructions strongly
depend on the structure of the underlying model, encouraging the proliferation of tiresome
metatheoretic work as we discussed in <ref>.

What is lacking with the dual-context style is the ability to work systematically with a large class
of modal situations without reconsidering the properties of the system in each case. Some of the
rules of  rules can be directly traced to rules in dual-context calculi (in particular, the
elimination rule for modal types), but the structure of our contexts is radically different, in a
way which is far more accommodating.

§.§ Modal type theories based on left division

A separate strand of modal type theories has built around a structure termed left division by
“left division”. Rather than having a fixed number of distinct modal and intuitionistic contexts,
there is a single context consisting of variables with modal annotations. The earliest
appearance of this pattern is in the work of <cit.>, where the annotations described
a variable as having various degrees of proof (ir)relevance.

In a non-dependent type system, the distinction between annotations and different contexts is
artificial: we could simply sort variables by their annotation, and separate them into different
context zones. However, once generalized to a dependent type theory have a distinct advantage: they
do not impose a fixed dependence schedule between different contexts. Instead, a type may depend on
anything preceding it in the context, but the nature of that dependence is moderated by the modal

The term `left division' is chosen to describe this structure because of the behavior of the
introduction rules for modal types. For instance, in <cit.>, there is a rule for
introducing a term in an irrelevant context:

\[
\inferrule{
\Gamma^{\oplus} \vdash M : A
\Gamma \vdash M :_{\mathsf{irr}} A
\]

Here $-^{\oplus}$ is a metatheoretic operation, which traverses the context and removes irrelevance
annotations. The effect of this is that all the variables in $\Gamma^{\oplus}$ can be used freely
when type-checking $M$. This is acceptable, because $M$ itself is irrelevant. Viewed properly this
is a division operation which `divides' all the annotations in $\Gamma$ by $\mathsf{irr}$. The
metatheory of a full dependent type theory based on this idea was considered by <cit.>,
who prove that modelling irrelevance in this way is sound and decidable.

More recent work by the third author <cit.> has carried this idea to its
natural conclusion by incorporating an entire hierarchy of modalities. In a related but distinct
line of work, the  Project <cit.> has exploited a
similar structure to give a systematic account of substructurality. There is ongoing work to extend
this to a full dependent type theory.

The modal annotations of  very similar to the modal annotations of variables in calculi with
left division. Contrasting  with <cit.> in particular, we find that there are
three classes of variables in op. cit.: normal variables (written $x : A$), irrelevant
variables ($x \div A$), and valid variables ($x :: A$). Such a situation would be modeled in
by a single mode that has three endomodalities: irrelevance, extensionality (the identity modality),
and validity. A composition table for these modalities can be built from the relations in
<cit.>'s calculus.

The rules for interacting with the modalities in op. cit. traverse the context and modify the
binding used for each variable. This bulk operation is very different to -style locks, but
amounts to similar constraints on variable use. By tagging the context with a lock, every time we
use a variable we must ensure that the annotated modality sufficiently strong to overcome the lock.
When we bulk-update the context, the same restrictions occur but they are performed `eagerly.'

The use of `lazy' locks rather than `eager' updated has several advantages over eager bulk updates.
For instance, we do not have to explain what it means to divide one modality by another, and
non-trivial 2-cells are possible. Furthermore, when interpreting the calculus in a model, it is
unnecessary to describe variable by variable how modality update affects the interpretation of the
entire context (which can be challenging: see  <cit.>).

§.§ Fitch-style modal type theories

A recent series of papers has used a judgmental structure that is similar to  in order to
manage a variety of modalities <cit.>. This kind of
structure, often informally referred to as the Fitch-style <cit.>,
divides the context into regions of variables separated by locks. Locks are dynamically included or
removed by the typing rules.

The central advantage of the Fitch-style is the impressively simple introduction rule for
modalities: whenever we wish to introduce a modality we simply append a lock to the context to tag
the modal shift, and continue. In particular, we do not ever need to remove variables from the
context during the introduction of a modal term, which alleviates a significant sore point of the
dual-context calculi. Of course, like in  this style of rule is only sound for a modality
which comes equipped with some sort of left-adjoint-like operation.

Another desirable property of the Fitch-style calculi are their strong elimination rules for
modalities. Rather than the pattern matching-style rules of other systems, Fitch-style calculi have
had an open-scope elimination rule for their modalities. This stronger rule also often
permits a definitional $\eta$-rule for $\Box A$. The elimination rule is generally of the following

\[
\inferrule{
\mathfrak{F}(\Gamma) \vdash M : \Box A
\Gamma \vdash \mathsf{open}(M) : A
\]

$\mathfrak{F}$ is a meta-theoretic operation on contexts which removes some number of locks and
variables from $\Gamma$. For instance, in <cit.>, $\mathfrak{F}(\Gamma)$ was
defined by

\[
\mathfrak{F}(\Gamma, \text{\faUnlock}, \Gamma') = \Gamma \text{ where } \text{\faUnlock} \not\in \Gamma'
\]

This rule is convenient, and strictly more powerful than the elimination rule of  (see
<ref>). However, it is metatheoretically less than ideal. The source of the trouble in
this case is that we must show that substitutions can be pushed under the $\mathsf{open}$ construct.
For instance, suppose we have some substitution $\gamma : \Delta \to \Gamma, \text{\faUnlock},
\Gamma'$. It is necessary to ensure that this substitution uniquely gives rise to a substitution
$\mathfrak{F}(\gamma) : \mathfrak{F}(\Delta) \to \Gamma$, which will then be applied to the body $M$
of the term. This property can only be shown by lengthy induction on syntax. Such a property is
proven laboriously in <cit.> for the $\MLTTLock$ type theory, and several complex and
artificial typing rules are necessary to show it. The situation is in some ways similar to
dual-context calculi, where meticulous expert attention in needed to show the admissibility of
substitution in each modal setting.

The other, more serious, issue with the Fitch-style is the difficulty of accounting for multiple
distinct modalities. Each modality should give rise to a different lock, but the structural rules
governing their interactions are complex even in relatively simple cases. It is well-understood how
to model the $\Later$ modality in a Fitch-style type theory, and <cit.> developed an
extensive account of the $\Box$ modality. However, it is an open problem whether the two may be
combined. There is work to this effect in a simple type theory <cit.>, but even in this
case there are restrictions on $\Box$ and $\Later$ which prevent recovering the type
theory of <cit.> as a subsystem.

The root of the issue seems to mirror the problems in Section <ref>, having
a rule which removes elements of the context is difficult to account for in more complex
situations. Drawing on this intuition,  has adopted the simple introduction rules from
Fitch-style calculi, but not the elimination rules. The result is that  has a less powerful
elimination rule, and a weaker definitional equality than Fitch-style calculi. In particular, there
is no equivalent of the definitional $\eta$-equality. In return for these weaker rules,  can
smoothly incorporate multiple interacting modalities.

§.§ Other work

A recent line of work <cit.> has tackled the same question as : how
can we design one calculus which can be systematically adapted to many different modal situations?
There has been ongoing work on extending this system to a full dependent type theory, but as of late
2020 this work remains unpublished.

This line of research is commonly referred to as LSR framework (after the initials of the
authors). LSR is designed to handle a wide variety of modal situations in combination with a variety
of different substructural settings. The impetus for that is derived from a long-standing
wish to address the major problems that arise in the interaction between dependent types and
substructural logics. This is an axis of generalization which is entirely outside the scope of
. However, we may compare LSR to  along the modal axis.

The idea of parametrizing a type theory by a mode theory, as we have done with , originates in
a paper preceding the LSR framework <cit.>. In fact, the modal situations that can be
handled by  are a strict subset of those which can be handled by pre-LSR/LSR, which also
includes a modality representing the left adjoint as an operation on types (and not just
contexts). By contrast,  has a simpler syntax which is amenable to current proof and
implementation techniques. This is reflected in our proof of canonicity, and our experimental
implementation efforts <cit.>. We therefore believe that  is a natural halfway point
between current modal type theories (which are custom-fitted for each modal situation) and the full
generality of LSR: it is a simpler theory which accounts for many situations of interest.

§ CONCLUSIONS

We introduced and studied , a dependent type theory parametrized by a mode theory that
describes interacting modalities. We have demonstrated that  may be used to reason about
several important modal settings, and proven basic metatheorems about its syntax, including

Several distinct directions of future work present themselves.

Towards an Implementation of
A major point of future work is the development of an implementation of . Substantial
preliminary implementation efforts are already underway with  <cit.>. In
addition to the engineering effort, a systematic account for an algorithmic syntax of  as well
as proof of normalization is needed. We believe that the general ideas of <cit.> are
applicable to this situation and there is ongoing work to apply them to  through more modern
gluing techniques <cit.>. Eventually, this work should prove that
$\EqTm{M}{N}{A}$ and $\EqTy{A}{B}$ are decidable relative to a decision procedure for equality in
the underlying mode theory.

Left Adjoints
As discussed in  <ref>,  trades a measure of generality for a degree of
simplicity, as compared to LSR. One might hope, however, that it would be possible to include a
connective for left adjoints, as well as the current connective which models right adjoints
without losing all of this simplicity. It is not obvious that this can be done without significantly
changing : the introduction rule for modalities is exceptionally specific to a right adjoint.
This additionally flexibility would allow us to model several modalities which are currently out of
reach. For instance, when modeling a string of adjoints, we always fail to model the final left
adjoint. Concretely speaking, the inclusion of left adjoints would allow  to model
computational effects <cit.>, as we will be able to internally recover the
corresponding monad.

§.§ Acknowledgements

We are grateful for productive conversations with Carlo Angiuli, Dominique Devriese, Adrien
Guatto, Magnus Baunsgaard Kristensen, Daniel Licata, Rasmus Ejlers Møgelberg, Matthieu Sozeau,
Jonathan Sterling, and Andrea Vezzosi.

Alex Kavvos was supported in part by a research grant (12386, Guarded Homotopy Type Theory) from
the VILLUM Foundation.
Andreas Nuyts was supported by a PhD Fellowship from the Research Foundation -
Flanders (FWO) at imec-DistriNet, KU Leuven.
This work was supported in part by a Villum Investigator grant (no.  25804),
Center for Basic Research in Program Verification (CPV), from the VILLUM Foundation.