We introduce , a dependent type theory which supports multiple modalities.   is
parametrized by a mode theory which specifies a collection of modes, modalities, and
transformations between them.

We show that different choices of mode theory allow us to use the same type theory to compute and
reason in many modal situations, including guarded recursion, axiomatic cohesion, and parametric
quantification. We reproduce examples from prior work in guarded recursion and axiomatic cohesion
— demonstrating that  constitutes a simple and usable syntax whose instantiations
intuitively correspond to previous handcrafted modal type theories. In some cases, instantiating
to a particular situation unearths a previously unknown type theory that improves upon
prior systems.

Finally, we investigate the metatheory of . We prove the consistency of  and establish
canonicity through an extension of recent type-theoretic gluing techniques. These results hold
irrespective of the choice of mode theory, and thus apply to a wide variety of modal situations.

§ INTRODUCTION

In order to increase the expressivity of Martin-Löf Type Theory () we often wish to extend
it with unary type operators that we call modalities or modal operators. Some modal
operators arise as shorthands for internally definable structure <cit.>, while others
are used as a device for internalising non-definable structure from particular models. In the latter
case, we are sometimes even able to prove that a modality cannot be internally expressed—at least
not without extensive changes to the judgmental structure of type theory: see  the `no-go'
theorems by <cit.> and <cit.>. This paper is concerned with the
development of a systematic approach to the judgmental formulation of type theories with multiple
interacting modalities.

The addition of a modality to a dependent type theory is a non-trivial exercise. Modal operators
often interact with the context of a type or term in a complicated way, and naïve approaches
lead to undesirable interplay with other type formers and substitution. However, the consequent gain
in expressivity is substantial, and so it is well worth the effort. For example, modalities have
been used to express guarded recursive
definitions <cit.>, parametric
quantification <cit.>, proof
irrelevance <cit.>, and to define global operations which cannot
be localized to an arbitrary context <cit.>. There has also been concerted
effort towards the development of a dependent type theory corresponding to Lawvere's axiomatic
cohesion <cit.>, which has many interesting applications <cit.>.

Despite this recent flurry of developments, a unifying account of modal dependent type theory has
yet to emerge. Faced with a new modal situation, a type theorist must handcraft a brand new system,
and then prove the usual battery of metatheorems. This introduces formidable difficulties on two
levels. First, an increasing number of these applications are multimodal: they involve
multiple interacting modalities, which significantly complicates the design of the appropriate
judgmental structure. Second, the technical development of each such system is entirely separate, so
that one cannot share the burden of proof even between closely related systems.  To take a recent
example, there is no easy way to transfer the work done in the 80-page-long normalization proof for
$\MLTTLock$ <cit.> to a normalization proof for the modal dependent type theory of
<cit.>, even though these systems are only marginally different. Put simply, if
one wished to prove that type-checking is decidable for the latter, then one would have to start

We intend to avoid such duplication in the future. Rather than designing a new dependent type theory
for some preordained set of modalities, we will introduce a system that is parametrized by a
mode theory,  an algebraic specification of a modal situation.  This system, which we
call , solves both problems at once. First, by instantiating it with different mode theories
we will show that it can capture a wide class of situations. Some of these,  the one for
guarded recursion, lead to a previously unknown system that improves upon earlier work. Second, the
predictable behavior of our rules allows us to prove metatheoretic results about large classes of
instantiations of our system. For example, our canonicity theorem applies irrespective of the
chosen mode theory. As a result, we only need to prove such theorems once. Returning to the
previous examples, careful choices of mode theory yield two systems that closely resemble the calculi of
<cit.> and $\MLTTLock$ <cit.> respectively, so that our proof of
canonicity applies to both.

In fact, we take things one step further:  is not just multimodal, but also multimode.
That is, each judgment of  can be construed as existing in a particular mode. All modes
have some things in common— there will be dependent sums in each—but some might
possess distinguishing features. From a semantic point of view, different modes correspond to
different context categories. In this light, modalities intuitively correspond to functors
between those categories: in fact, they will be structures slightly weaker than dependent
right adjoints (DRAs) <cit.>.

Mode theories

At a high level,  can be thought of as a machine that converts a concrete description of modes
and modalities into a type theory. This description, which is often called a mode theory, is
given in the form of a small strict 2-category <cit.>. A
mode theory gives rise to the following correspondence:

\begin{align*}
\text{object} &\sim \text{mode} \\
\text{morphism} &\sim \text{modality} \\
\text{2-cell} &\sim \text{natural map between modalities}
\end{align*}

The equations between morphisms and between 2-cells in a mode theory can be used to precisely specify
the interactions we want between different modalities. We will illustrate this point with an example.

Suppose we have a mode theory $\Mode$ with a single object $m$, a single generating morphism $\mu :
m \to m$, and no non-trivial 2-cells. Equipping  with $\Mode$ produces a type theory with a
single modal type constructor, $\Modify$. This is the simplest non-trivial setting, and we can prove
very little about it without additional 2-cells.

If we add a 2-cell $\epsilon : \mu \To 1$ to $\Mode$, we can define a function

\[
\mathsf{extract}_A : \Modify{A} \to A
\]

inside the type theory. If we also add a 2-cell $\delta : \mu \To \mu \circ \mu$ then we can also

\[
\mathsf{duplicate}_A : \Modify{A} \to \Modify{\Modify{A}}
\]

Furthermore, we can control the precise interaction between $\mathsf{duplicate}_A$ and $\mathsf{extract}_A$ by
adding more equations that relate $\epsilon$ and $\delta$. For example, we may ask that $\Mode$ be
the walking comonad <cit.> which leads to a type theory with a dependent
-like modality <cit.>. We
can be even more specific,  by asking that $(\mu, \epsilon, \delta)$ be idempotent.

Thus, a morphism $\mu : n \to m$ introduces a modality $\Modify$, and a 2-cell
$\alpha : \mu \To \nu$ of $\Mode$ allows for the definition of a function of type
$\Modify{A} \to \Modify[\nu]{A}$ at mode $m$.

Relation to other modal type theories

Most work on modal type theories still defies classification. However, we can informatively position
with respect to two qualitative criteria,  usability and generality.

Much of the prior work on modal type theory has focused on bolting a specific modality onto a type theory. The benefit of this
approach is that the syntax can be designed to be as convenient as possible for the application at
hand. For example, spatial/cohesive type theory <cit.> features two modalities,
$\flat$ and $\sharp$, and is presented in a dual-context style. This judgmental structure, however,
is applicable only because of the particular properties of $\flat$ and $\sharp$. Nevertheless, the numerous
pen-and-paper proofs in op. cit. demonstrate that the resulting system is easy
to use.

At the other end of the spectrum, the framework of Licata-Shulman-Riley (LSR) <cit.>
comprises an extremely general toolkit for simply-typed, substructural modal type theory. Its
dependent generalization, which is currently under development, is able to handle a very large class
of modalities. However, this generality comes at a price: its syntax is complex and unwieldy,
even in the simply-typed case.

attempts to strike a delicate balance between those two extremes. By avoiding substructural
settings and some kinds of modalities we obtain a noticeably simpler apparatus. Unlike LSR, we need
not annotate our term formers with delayed substitutions, and our approach extends to dependent
types in a straightforward manner. Most of the pleasant type-theoretic behaviour of  is
achieved by ensuring that none of its rules `trim' the context, which would necessitate either
delayed substitutions <cit.> or delicate proofs of the admissibility of
substitution <cit.>. We also show that  can be
employed to reason about many models of interest, and that it is simple enough to be used in
pen-and-paper calculations.

In summary, we make the following contributions:

* We introduce , a general type theory for multiple modes and multiple interacting

* We present a semantics, which constitute a category of models deriving from the generalized algebraic theory that underlies .

* Using the semantics, we prove that—subject to a technical restriction— satisfies
canonicity, an important metatheoretic property. This is achieved through a modern
gluing argument <cit.>.

* Finally, we instantiate  with various mode theories, and show its use in reasoning about two specific modal situations, viz. guarded recursion <cit.>, and internal adjunctions <cit.>.

§ THE SYNTAX OF

As mentioned in the introduction, the syntax of  is parameterized by a small 2-category called
a mode theory. We will later show how to instatiate  with a mode theory in order to
reason about particular scenarios, but for now we will work over an arbitrary mode theory. We thus
fix a mode theory $\Mode$, and use $m, n, o$ to stand for modes (the objects of $\Mode$), $\mu, \nu,
\tau$ for modalities (the morphisms), and $\alpha, \beta, \gamma$ for 2-cells.

In broad terms,  consists of a collection of type theories, one for each mode $m \in \Mode$.
These type theories will eventually appear in one another, but only as spectres under a modality. We
thus begin by describing the individual type theories at each mode, and then discuss how modalities
are used to relate them.

§.§ The Type Theory at Each Mode

Each mode of  is inhabited by a standard Martin-Löf Type Theory (), and accordingly
includes the usual judgments. For example, we have the judgment $\IsCx{\Gamma}$ which states that
$\Gamma$ is a well-formed context in that particular mode $m$. There are likewise judgments
for types, terms, and substitutions at each mode.

[1]

[Γ, x : A]B

(x : A) →B
(x : A) ×B

Selected mode-local rules.

In lieu of an exhaustive list of rules, which we will present in <ref>, we
illustrate this point by only showing the important ones in
Figure <ref>. In brief, each mode comprises an ordinary intensional type
theory with dependent sums, dependent products, intensional identity types, booleans, and one
universe. Both sums and products satisfy an $\eta$-rule.

Universes à la Coquand

There are several ways to introduce universes in type theory <cit.>
<cit.>. We use the approach of <cit.>, which is close to
Tarski-style universes. However, instead of inductively defining codes that represent
particular types, Coquand-style universes come with an explicit isomorphism between types and
terms of the universe $\Uni$. However, we must remember to exercise caution: if this isomorphism
were to cover all types then Girard's paradox <cit.> would apply, so we must
restrict it to small types. This, in turn, forces us to stratify our types into small and large.

The judgment $\IsTy{A}[0]$ states that $A$ is a small type, and $\IsTy{A}[1]$ that it
is large. The universe itself must be a large type, but otherwise both levels are closed under all
other connectives. Finally, we introduce an operator that lifts a small type to a large one:

\[
\inferrule{
\ell \le \ell'\\
\IsTy{A}[\ell]
\IsTy{\TyLift{A}}[\ell']
\]

The lifting operation commutes definitionally with all the connectives,
$\TyLift{(A \to B)} = \TyLift{A} \to \TyLift{B}$. We will use large types for the most part:
only they will be allowed in contexts, and the judgment $\IsTm{M}{A}$ will presuppose that $A$ is
large. As we will not have terms at small types, we will not need the term lifting operations
used by <cit.> and <cit.>.

Following this stratification, we may introduce operations that exhibit the isomorphism:

along with the equations $\Enc{\Dec{M}} = M$ and $\Dec{\Enc{A}} = A$.

The advantages of universes à la Coquand are now evident: rather than having to introduce
Tarski-style codes, we now find that they are definable. For example, assuming $M : \Uni$ and
$x : \Dec{M} \vdash N : \Uni$, we let

\[
(x : M) \mathrel{\widehat{\to}} N \defeq \Enc{(x : \Dec{M}) \to \Dec{N}} : \Uni
\]

We can then calculate that

\[
\Dec{(x : M) \mathrel{\widehat{\to}} N} = \Dec{\Enc{(x : \Dec{M}) \to \Dec{N}}}
= (x : \Dec{M}) \to \Dec{N}
\]

We will often suppress $\TyLift{-}$ as well as the explicit isomorphism.

§.§ Introducing a Modality

Having sketched the basic type theory inhabiting each mode, we now turn to the interaction between them. This is the domain of the modalities.

Suppose $\Mode$ contains a modality $\mu : n \to m$. We would like to think of $\mu$ as a `map' from
mode $n$ to mode $m$. Then, for each $\IsTy[]{A}[]<n>$ we would like a type
$\IsTy[]{\Modify{A}}[]<m>$. On the level of terms we would similarly like for each
$\IsTm[]{M}{A}<n>$ an induced term $\IsTm[]{\MkBox{M}}{\Modify{A}}<m>$.

These constructs would be entirely satisfactory, were it not for the presence of open terms.
To illustrate the problem, suppose we have a type $\IsTy{A}[]<n>$. We would hope that the
corresponding modal type lives in the same context,  that $\IsTy{\Modify{A}}[]<m>$. However,
this is not possible, as $\Gamma$ is only a context at mode $n$, and cannot be
carried over verbatim to mode $m$. Hence, the only pragmatic option is to introduce an operation
that allows a context to be mapped to another mode.

Forming a modal type

There are several different proposed solutions to this problem in the literature
<cit.>. We will use a Fitch-style
discipline <cit.>: we will require that a modality $\mu$
induce an operation on contexts in the opposite direction. We will denote this operation by a lock:

\[
\inferrule[cx/lock]{
\IsCx{\Gamma}
\IsCx{\LockCxV{\Gamma}}<n>
\]

Intuitively, $\Lock_\mu$ will behave somewhat like a left adjoint to $\Modify{-}$. However,
$\Modify{-}$ acts on types while $\LockCxV{-}$ acts on contexts, so this cannot be an ordinary
adjunction. Instead, $\Modify{-}$ will be what <cit.> call a dependent
right adjoint (DRA). A DRA essentially consists of a type former $\mathbf{R}$ and a context
operation $\mathbf{L}$ such that

\begin{equation*}
\{N \mid \mathbf{L}(\Gamma) \vdash N : A \} \cong \{ M \mid \Gamma \vdash M : \mathbf{R}(A) \}
\TagEq[$\dagger$]\label{eq:towards-mtt:dra}
\end{equation*}

See <cit.> for a formal definition.

Just as with DRAs, the  formation and introduction rules for modal types effectively
transpose types and terms across this adjunction:

μ: m →n

μ: m →n

It remains to show how to eliminate modal types. Previous work on Fitch-style calculi
<cit.> has employed elimination rules which essentially invert the
introduction rule tm/modal-intro. Such rules remove one or more locks from the
context during type-checking, and sometimes even trim a part of it. For example, a rule of this sort
would be

\[
\inferrule{
\Lock_\mu \not\in \Gamma'\\
\IsTm{M}{\Modify{A}}
\IsTm[\LockCxV{\Gamma}, \Gamma']{\mathsf{open}(M)}{A}<n>
\]

This kind of rule tends to be unruly, and delicate work is required to prove even basic results
about it. For example, see the technical report <cit.> for a particularly
laborious proof of the admissibility of substitution. The results in op. cit. could not
possibly reuse any of the work of <cit.>, as a small change in the syntax leads
to many subtle differences in the metatheory. Consequently, it seems unlikely that one could adapt
this approach to a modality-agnostic setting like ours.

We will use a different technique, which is reminiscent of dual-context
calculi <cit.>. First, we will let the variable rule control the use of modal
variables. Then, we will take a `modal cut' rule, which will allow
the substitution of modal terms for modal variables, to be our modal elimination rule.

Accessing a modal variable

The behavior of modal types can often be clarified by asking a simple question: when can we use a
variable $x : \Modify{A}$ of modal type to construct a term of type $A$? In previous Fitch-style
calculi we would use the modal elimination rule to reduce the goal to $\Modify{A}$, and
then—had the modal elimination rule not eliminated $x$ from the context—we would simply
use the variable. We may thus write down a term of type $A$ using a variable $x : \Modify{A}$ only
when our context is structured in a way that does not obstruct the use of $x$, and the final arbiter
of that is the modal elimination rule.

turns this idea on its head: rather than handing control over to the modal elimination rule,
we delegate this decision to the variable rule itself. In order to ascertain whether we can use a
variable in our calculus, the variable rule examines the locks to the right of the variable.
The rule of thumb is this: we should always be able to access $\Modify{A}$ behind $\Lock_\mu$.
Carrying the illustrative analogy of an adjunction $\LockCxV{-} \Adjoint \Modify{-}$ further, we see
that the simplest judgment that fits this, namely $\IsTm[\LockCxV{\Gamma, x :
\Modify{A}}]{x}{A}<n>$, corresponds to the counit of the adjunction.

To correctly formulate the variable rule, we will require one more idea: following modal type
theories based on left
division <cit.>, every variable in the
context will be annotated with a modality, $\DeclVar{x}{A}$. Intuitively a variable $\DeclVar{x}{A}$
is the same as a variable $x : \Modify{A}$, but the annotations are part of the structure of
a context while $\Modify{A}$ is a type. This small circumlocution will ensure that the variable rule
respects substitution.

The most general form of the variable rule will be able to handle the interaction of modalities, so
we present it in stages. A first counit-like approximation is then

[Γ_0xA, Γ_1]xA<n>

The first premise requires that no further locks occur in $\Gamma_1$, so that the conclusion remains in the same mode $n$. The second premise is just enough to derive $\IsTy[\Gamma_0]{\Modify{A}}[1]$.

Context extension

The switch to modality-annotated declarations $\DeclVar{x}{A}$ also requires us to revise the
context extension rule. The revised version, cx/extend, appears in
Figure <ref> and closely follows the formation rule for $\Modify{-}$: if
$\IsTy[\LockCxV{\Gamma}]{A}[1]<n>$ is a type in the locked context $\Gamma$, then we may extend the
context $\Gamma$ to include a declaration $\DeclVar{x}{A}$, so that $x$ stands for a term of type
$A$ under the modality $\mu$.

The elimination rule

The difference between a modal type $\Modify{A}$ and an annotated declaration $\DeclVar{x}{A}<\mu>$
in the context is navigated by the modal elimination rule. In brief, its role is to enable the
substitution of a term of the former type for a variable with the latter declaration. The full rule
is complex, so we first discuss the case of a single modality $\mu : n \to m$. The correspoding rule is

Forgetting dependence for a moment, we see that this rule is close to the dual-context style
<cit.>: if we think of annotations as separating the context into
multiple zones, then $\DeclVar{y}{A}<\mu>$ clearly belongs to the `modal' part.

In the dependent case we also need a motive $\IsTy[\ECxV{\Gamma}{x}{\Modify{A}}<1>]{B}[1]$, which
depends on a variable of modal type, but under the identity modality $1$. This premise is then
fulfilled by $M_0$ in the conclusion. In a sense, this rule permits a form of modal
induction: every variable $\DeclVar{x}{\Modify{A}}<1>$ can be assumed to be of the form $\MkBox{y}$
for some $\DeclVar{y}{A}<\mu>$. This kind of rule has appeared before in the spatial and cohesive type theories of <cit.>.

In the type theory of <cit.> modalities are taken to be dependent right adjoints,
with terms witnessing Equation <ref>. This isomorphism can encode
tm/modal-elim/single-modality, but that rule alone cannot encode
Equation <ref>. As a result, modalities in  are weaker than DRAs.

§.§ Multiple Modalities

μ: n →m

μ: n →m

ν: o →n

μ: n →m

A     MA

μ: n →m

ν: m →n

α: νΓ_1

[Γ_0xA<ν>, Γ_1]x^αA^α

μ: n →m

μ: n →m

ν: m →o

ν: m →o

μ: n →m

= 1 ΓxA = Γ Γ = Γ ∘μ
Selected modal rules.

So far we have only considered a single modality. In this section we discuss the few additional
tweaks that are needed to support multiple interacting modalities. The final version of the modal
rules is given in Figure <ref>.

Multimodal locks

Up to this point the operation $\LockCxV{-}$ on contexts has referred to a single modality $\mu : n
\to m$. The rule cx/lock generalizes it to work with any modality. The only question then
is how the resulting operations should interact. This is where the mode theory comes in: locks
should be functorial, so that $\nu : o \to n$, $\mu : n \to m$, and $\IsCx{\Gamma}$ imply
$\EqCx{\LockCxV{\LockCxV{\Gamma}}<\nu>}{\LockCxV{\Gamma}<\mu \circ \nu>}<o>$. We additionally ask
that the identity modality $1 : m \to m$ at each mode has a trivial, invisible action on contexts,
that $\LockCxV{\Gamma}<1> = \Gamma$.

These two actions, which are encoded by cx/compose and cx/id, ensure that
$\Lock$ is a contravariant functor on $\Mode$, mapping each mode $m$ to the category of
contexts $\IsCx{\Gamma}$. The contravariance originates from the fact that $\Mode$ is a
specification of the behavior of the modalities $\Modify{-}$, so that their left-adjoint-like
counterparts $\LockCxV{-}$ act with the opposite variance.

The full variable rule

We have seen that $\Lock$ induces a functor from $\Mode$ to categories of contexts, but we have not
yet used the 2-cells of $\Mode$. In short, a 2-cell $\alpha : \mu \To \nu$ contravariantly induces a
substitution from $\LockCxV{\Gamma}<\nu>$ to $\LockCxV{\Gamma}<\mu>$. We will discuss this further
in Section <ref>, but for now we only mention that this arrangement gives rise to
an admissible operation on types: for each 2-cell we obtain an operation $(-)^\alpha$ such
that $\IsTy[\LockCxV{\Gamma}]{A}[]$ implies $\IsTy[\LockCxV{\Gamma}<\nu>]{A^\alpha}[]$.

In order to prove the admissibility of this operation we need a more expressive variable rule
that builds in the action of 2-cells. The first iteration (tm/var/counit) required that
the lock and the variable annotation were an exact match. We relax this requirement by allowing
for a mediating 2-cell:

μ,ν: n →m

α: μν

The superscript in $x^\alpha$ is now part of the syntax: each variable must be annotated with the
2-cell that `unlocks' it and enables its occurrence, though we will still write $x$ to mean
$x^{1_\mu}$.  The final form of the variable rule, which appears as tm/var in
Figure <ref>, is only a slight generalization of this last rule: it allows the variable to
occur at positions other than the very front of the context. In fact, tm/var can be
reduced to tm/var/combined by using weakening to remove variables to the right of $x$, and
then invoking functoriality to fuse all the locks to the right of $x$ into a single one with
modality $\Locks{\Gamma_1}$.

The full elimination rule

Recall that the elimination rule for a single modality allowed us to plug in a term of type
$\Modify{A}$ for an assumption $\DeclVar{x}{A}<\mu>$. Some additional generality is needed to cover
the case where the motive $\IsTy[\DeclVar{x}{\Modify{A}}<\nu>]{B}[]$ depends on $x$ under a modality
$\nu \neq 1$. This is where the composition of modalities in $\Mode$ comes in handy: our new rule
will use it to absorb $\nu$ by replacing the assumption $\DeclVar{x}{\Modify{A}}<\nu>$ with
$\DeclVar{x}{A}<\nu \circ \mu>$.

The new rule, tm/modal-elim, is given in Figure <ref>. The simpler
rule may be recovered by setting $\nu \defeq 1$. In this simpler case, we will suppress the
subscript $1$ on $\mathsf{let}$, just as in tm/modal-elim/single-modality.  However,
many natural examples require eliminations where $\nu \neq 1$. For instance, in
Section <ref> we show that $\Modify[\nu \circ \mu]{A} \Equiv
\Modify[\nu]{\Modify{A}}$. The function from the right-hand side to the left crucially depends on
the ability to pattern-match on a variable $\DeclVar{x}{\Modify{A}}<\nu>$, which requires the
stronger tm/modal-elim.

Definitional equality in

A perennial problem in type theory is that of deciding where the boundary between those equalities
that are provable in the system (e.g. using various forms of induction), and those that are
definitional, i.e. hold by fiat. While have simply followed standard practices in the $\MLTT$
connectives at each mode, the situation is somewhat more complicated regarding modal types. On the
one hand, we have the expected $\beta$-rule tm/modal-beta: see
Figure <ref>. On the other hand, we do not include any definitional
$\eta$-rules: as the eliminator is a positive pattern-matching construct, the proper
$\eta$-rule would need commuting conversions, which would enormously complicate the

Notational conventions

In the rest of the paper we shall make use of the following notational conventions.

When opening a modal term under the modality $1$ we will suppress the $1$ in the $\textsf{let}_1$
part of the term, and write $\Open{M}{N}[1]$ instead.

As remarked before, Coquand-style universes do not require the introduction of codes that
represent various types in the universe, for they are definable. Nevertheless, in examples we will
often suppress both $\Dec{-}$ and $\Enc{-}$, and in some straightfoward cases even elide the
coercion $\TyLift{-}$. This not only makes our terms more perspicuous, but can also be formally
justified by an elaboration procedure which inserts the missing isomorphisms and coercions
when needed.

§ PROGRAMMING WITH MODALITIES

In this section we show how  can be used to program and reason with modalities. We we identify
a handful of basic modal combinators which demonstrate the behaviour of our modal types. Then, in
<ref> we use them to present a type theory featuring an
idempotent comonad with almost no additional effort.

§.§ Modal Combinators

We first show how each 2-cell $\alpha : \mu \To \nu$ with $\mu, \nu : n \to m$ induces a natural
transformation $\Modify{-} \to \Modify[\nu]{-}$. We call the components of this natural
transformation coercions. Given $\IsTy[\LockCxV{\Gamma}]{A}[1]$, define

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\Coe{-}{\mu}{\nu}{\alpha} & : & \Modify{A} \to \Modify[\nu]{A^\alpha}\\
\Coe{x}{\mu}{\nu}{\alpha} & \defeq & \Open{x}[z]{\MkBox[\nu]{z^\alpha}}<\mu>[1]
\end{array}
\]

The heart of this combinator is a use of the rule tm/var. This operation completes the
correspondence sketched in <ref>: objects of $\Mode$ correspond to modes, morphisms to
modalities, and 2-cells to coercions.

Additionally, the assignment $\mu \mapsto \Modify{-}$ is functorial. Unlike the action of
locks, this functoriality is not definitional, but only a type-theoretic equivalence
<cit.>. Fixing $\nu : o \to n$, $\mu : n \to m$, and $\IsTy[\LockCxV{\Gamma}<\mu
\circ \nu>]{A}[1]$, we let

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\multicolumn{3}{l}{\MComp{}{\mu}{\nu} : \Modify{\Modify[\nu]{A}} \to \Modify[\mu \circ \nu]{A}}\\
\MComp{x}{\mu}{\nu} & \defeq & \Open{x}[x_0]{}<\mu>[{\ \ }]\\
&& \Open{x_0}[x_1]{}<\nu>[\mu]\\
&& \MkBox[\mu \circ \nu]{x_1}
\end{array}
\]

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\multicolumn{3}{l}{\MComp*{}{\mu}{\nu} : \Modify[\mu \circ \nu]{A} \to \Modify{\Modify[\nu]{A}}}\\
\MComp*{x}{\mu}{\nu} & \defeq & \Open{x}[x_0]{}<\mu \circ \nu>[1] \MkBox[\mu]{\MkBox[\nu]{x_0}}
\end{array}
\]

We elide the 2-cell annotations on variables, as they are all identities ( we only need
tm/var/counit). Even in this small example the context equations for locks are
essential: for $\Modify{\Modify[\nu]{A}}$ to be a valid type we need that
$\LockCxV{\LockCxV{\Gamma}}<\nu> = \LockCxV{\Gamma}<\mu \circ \nu>$, which is ensured by
cx/compose. Furthermore, observe that $\MComp{}{\mu}{\nu}$ crucially relies on the
multimodal elimination rule tm/modal-elim: we must pattern-match on $x_0$, which is under
$\mu$ in the context.

Similarly, fixing $\IsTy{A}[1]$ we have

- : [1]A →A                     *- : A →[1]A

x x[x_0]x_0<1>[1]           *x [1]x

In both cases, these combinators are only propositionally inverse. For example, the proof for one direction of the composition combinator is

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\_ & : & (x : \Modify{\Modify[\nu]{A}}) \to \Id{\Modify{\Modify[\nu]{A}}}{x}{\MComp*{\MComp{x}{\mu}{\nu}}{\mu}{\nu}}\\
\_ & \defeq & \Lam[x]{}\Open{x}[x_0]{}<\mu>[1] \Open{x_0}[x_1]{}<\nu>[\mu] \Refl{\MkBox{\MkBox[\nu]{x}}}
\end{array}
\]

This is in many ways a typical example: we use the modal elimination rule to induct on a
modally-typed term, which reduces it to a term of the form $\MkBox[]{-}$. This is just enough to
make various terms compute, and the result then follows by reflexivity.

As a final example, we will show that each modal type satisfies the
axiom,[Not to be confused with Streicher's axiom K.] a central axiom of
Kripke-style modal logics. This combinator will be immediately recognizable to functional
programmers: it is the term that witnesses that $\Modify{-}$ is an applicative
functor <cit.>.

\[
\arraycolsep=1.4pt
\begin{array}{lcl}
\ZApp{-}{-}{\mu} & : & \Modify{A \to B} \to \Modify{A} \to \Modify{B}\\
\ZApp{f}{a}{\mu} & \defeq & \Open{f}[f_0]{\Open{a}[a_0]{\MkBox{\App{f_0}{a_0}}}<\mu>[1]}<\mu>[1]
\end{array}
\]

We can also define a stronger combinator which corresponds to a dependent form of the Kripke axiom
<cit.> along the same lines. As it generalizes $\ZApp{}{}{\mu}$ to dependent
products, this operation has precisely the same implementation but a more complex type:

\[
\Modify{(x : A) \to B} \to{} (x_0 : \Modify{A}) \to (\Open{x_0}[x]{\Modify{B}}<\mu>[1])
\]

In order to ensure that $\Modify{B}$ is well-typed, the context must contain $\DeclVar{x}{A}$, but
instead we have bound $\DeclVar{x_0}{\Modify{A}}<1>$. We correct this mismatch by eliminating $x_0$
and binding the result to $x$.

§.§ Idempotent Comonads in

A great deal of prior work in modal type theory has focused on comonads
<cit.>, and in particular
idempotent comonads. <cit.> has shown that such modalities
necessitate changes to the judgmental structure, as the only idempotent comonads that are internally
definable in type theory are of the form $- \times U$ for some proposition $U$. In this section we
present a mode theory for idempotent comonads, and prove that the resulting type theory internally
satisfies the expected equations. In fact, we only use the combinators of the previous section.

We define the mode theory $\IComonadMode$ to consist of a single mode $m$, and a single non-trivial
morphism $\mu : m \to m$. We will enforce idempotence by setting $\mu \circ \mu = \mu$.  Finally, in
order to induce a morphism $\Modify{A} \to A$ we include a unique non-trivial 2-cell
$\epsilon : \mu \To 1$. In order to ensure that this 2-cell to be unique, we add equations such as
$\epsilon \Whisker 1_\mu = 1_\mu \Whisker \epsilon : \mu \circ \mu \To \mu$, where $\Whisker$
denotes the horizontal composition of 2-cells. The resulting mode theory is a 2-category, albeit a
very simple one: it is in fact only a poset-enriched category.

We can show that $\Modify{A}$ is a comonad by defining the expected operations using the combinators
of Section <ref>:

_A : A →A           _A : A →A^ϵ

_A *μμ                     _A *- ∘μ1ϵ

We must also show that $\Dup_A$ and $\Unbox_A$ satisfy the comonad laws, but that automatically
follows from general facts pertaining to $\mathbf{coe}$ and $\mathbf{comp}$.[In
particular, our modal combinators satisfy a variant of the interchange law of a 2-category.]
This is indicative of the benefits of using : every general result about it also applies to
this instance, including the canonicity theorem of Section <ref>.

§ ALGEBRAIC SYNTAX

Until this point we have presented a curated, high-level view of , and we have avoided any
discussion of its metatheory. Yet, syntactic matters can be quite complex, and have historically
proven to be sticking points for modal type theory. While such details are not necessary for the
casual reader, it is essential to validate that  is syntactically well-behaved, enjoying
a substitution principle. The aim of this section is to provide a setting for this study: we
introduce the formal counterpart of , which is given as a generalized algebraic theory
(GAT) <cit.>.

Historically, GATs were used in the semantics of type theory, but modern techniques show that they
are also useful in the analysis of syntax. For example, recasting  as a GAT naturally leads us
to include explicit substitutions <cit.> in the
syntax. Thus, substitution in  is not a metatheoretic operation on raw terms, but a syntactic
operation within the theory. This presentation helps us carefully state the equations that govern
substitutions and their interaction with type formers. We consequently obtain an elegant
substitution calculus, which can often be quite complex for modal type theories.

This approach proffers a number of technical advantages. Amongst other things, the theorems proven in the aforementioned works on GATs imply the following points:

* We absolve ourselves from having to prove tedious syntactic metatheorems, e.g. admissibility of

* We automatically obtain a notion of model of our theory, which is given in entirely
algebraic terms.

* We obtain a notion of homomorphism of models. (NB that this notion is rather
strict and not fit for every purpose.)

* In an equally automatic fashion, we obtain an initial model for the algebraic theory,
which we consider as our main formal object of study.

* The unique morphism of models from this initial model to any other is the semantic
interpretation map. We then have no need to explicitly describe these semantic maps and prove
that they are well-defined on derivations, as done  by <cit.>.

While this approach is straightforward and uncluttered, some readers might object to the lack of a
more traditional formulation,  a named syntax with variables and a metatheoretic
substitution operation, like the one we informally presented in <ref>. We believe
that it is indeed possible to define such a syntax and systematically show how to elaborate
its terms to the algebraic syntax.

However, such a named syntax would not be directly suitable for implementation: for that purpose we
ought to develop an entirely different algorithmic syntax. We believe that such a syntax can
be constructed as an extension of existing bidirectional presentations of type
theory <cit.> as has been done for existing modal
calculi <cit.>. Such a bidirectional presentation would occupy a midpoint between the
maximally annotated algebraic syntax we present here, and the more typical named syntax of
<ref>: it would contain only a select few annotations to ensure the decidability
of typechecking, yet maintain readability. The development of such a syntax is a substantial
undertaking that requires a proof of normalization, and is orthogonal to the foundational
metatheoretic results that we seek to develop here. We thus refrain from developing it, and instead
work directly with the GAT.

§.§ Sorts

We begin by defining the different sorts (contexts, types, terms, ) that constitute our
type theory. In order to support multiple modes, our sorts will be parameterized in modes. Thus,
rather than having a single sort of types, we will have a sort of types at mode $m \in
\Mode$, and likewise for contexts at mode $m$, terms at mode $m$,

Moreover, we take care to index our types by levels. The reason for doing so was discussed in
<ref>: we seek to introduce a hierarchy of sizes, which we can then use to
introduce universes à la <cit.>. We stratify our types in two levels, drawn from the
set $\Lvl = \{0, 1\}$. There are no technical obstacles on the way to a richer hierarchy, but two
levels suffice for our purposes: we aim to divide our types into small types ( those that
can be reified in a universe) and large types (which also include the universe itself). In
order to enforce cumulativity we will also include an explicit coercion operator, which
includes small types into large types.

The levelled approach raises an obvious question: on which level should we admit terms? We could
follow the approach of <cit.> in allowing terms at both, but this requires the
introduction of term-level coercions, which then require equations relating term formers at
different levels. Thus, for the sake of simplicity we will only allow the formation of terms at
large types. Similarly, we will only allow the extension of a context by a large type.

has four sorts, which are introduced by the following rules:

m :

m :

Γ: m

m :

Γ: m

A : m[1](Γ)

m(Γ, A)

m :

Γ,Δ: m

m(Γ, Δ)

In the interest of clarity we will use the following shorthands:

\begin{align*}
\IsCx{\Gamma} &\defeq \Gamma : \Cx{m} &
\IsTy{A} &\defeq A : \Ty{m}(\Gamma) \\
\IsTm{M}{A} &\defeq M : \Tm{m}(\Gamma, A) &
\IsSb{\delta}{\Delta} &\defeq \delta : \Sub{m}(\Gamma, \Delta)
\end{align*}

Even though we will use this more familiar notation, we will take no prisoners in terms of rigour: we will carefully avoid overloading and ambiguity, and we will enforce presupposition.

§.§ Judgments

We shall now introduce the type theory itself by writing down the constructors and equalities of its GAT. In the interest of brevity, we elide a number of standard rules, including

* the congruence rules pushing substitutions inside terms and types;

* the congruence rules pushing explicit lifts inside of type formers;

* the associativity, unit, and weakening laws for the explicit substitutions;

* the $\beta$ laws for $\Pi$, $\Sigma$, $\Bool$ and $\textsf{Id}$;

* the $\eta$ laws for $\Pi$ and $\Sigma$;

The specification of the GAT is given in Figures
<ref>–<ref>. As the judgments are defined in a mutually
recursive manner, the division of the rules between different figures is merely presentational.
Given $\IsSb[\Delta]{\gamma}{\Gamma}$ and $\IsTy[\LockCx{\Gamma}]{A}$ we write

\[
\IsSb[\ECx{\Delta}{\Sb{A}{\LockSb{\gamma}}}]
{\gamma^{+} \defeq \ESb{(\gamma \circ \Wk)}{\Var{0}}}
\]

for the `weakened' substitution.

μ: []nm

μ: []nm

ν: []on

μ: []nm

[1]

μ: []nm

μ: []nm

μ: []nm

Γ, Δ,Ξ

Γ, Δ

μ: []nm

μ, ν: []nm

α: νμ

μ: []nm

Γ, Δ

μ: []nm

μ: []nm

ν: []on

μ: []nm

μ: []nm

μ: []nm

μ: []nm

Γ, Δ

μ: []nm

Γ, Δ

ℓ_0 ≤ℓ_1 ≤ℓ_2

Γ, Δ

Equality of Types

μ: []nm

ν: []on

μ: []nm

μ: []nm

ν: []on

μ: []nm

Equality of Terms

μ: []mn

(δM) ∘γ

μ: []mn

ν: []no

μ: []mn

μ: []mn

[Γ](ξ∘δ)ξ ∘δΞ

μ: []mn

μ,ν: []mn

α: νμ
αΓ ∘δ

δ<ν> ∘αΔ

μ_0, μ_1, μ_2 : []nm

α_0 : μ_0 μ_1

α_1 : μ_1 μ_2

α_1 ∘α_0Γ

α_0Γ ∘α_1Γ

ν_0, ν_1 : []on

μ_0, μ_1 : []nm

β: ν_0 ⇒ν_1

α: μ_0 ⇒μ_1

Γ<μ_0 ∘ν_0>

αΓ<ν_1> ∘βΓ<μ_0>

Γ<μ_1 ∘ν_1>

Equality of Substitutions

§.§ Discussion

We record some points on the generalized algebraic theory.

Modal substitutions

In addition to the usual rules,  features substitutions corresponding to the 1-cells and
2-cells of the mode theory. First, recall that for each modality $\mu : n \to m$ we have the
operation $\Lock_\mu$ on contexts. Its action extends to substitutions:

μ: n →m

Second, each 2-cell $\alpha : \mu \To \nu$ induces a natural transformation between
$\Lock_\nu$ and $\Lock_\mu$, whose component at $\Gamma$ is the `key' substitution

α: μν

Recalling that $\Coop{\Mode}$ is the 2-category with morphisms and 2-cells opposite from $\Mode$, we
see that these substitutions come with equations postulating that $\LockSb{-}<\mu>$ is a functor,
$\Key{\alpha}{\Gamma}$ is a natural transformation, and that together they form a 2-functor
$\Coop{\Mode} \to \CAT$. As a consequence, our type theory is forced to contain a calculus of
(strict) 2-categories. Indeed, the given equations for keys above suffice to derive the two ways of
internally stating the interchange laws, viz.

ν_0,ν_1,ν_2 : []on

μ_0,μ_1,μ_2 : []nm

α_0 : μ_0 μ_1

α_1 : μ_1 μ_2

β_0 : ν_0 ν_1

β_1 : ν_1 ν_2

[Γ<μ_2 ∘ν_2>]
α_0 β_0Γ
∘α_1 β_1Γ

α_1 ∘α_0Γ<ν_0>
∘β_1 ∘β_0Γ<μ_2>

Γ<μ_0 ∘ν_0>

ν_0,ν_1,ν_2 : []on

μ_0,μ_1,μ_2 : []nm

α_0 : μ_0 μ_1

α_1 : μ_1 μ_2

β_0 : ν_0 ν_1

β_1 : ν_1 ν_2

[Γ<μ_2 ∘ν_2>]
α_0 β_0Γ
∘α_1 β_1Γ

β_1 ∘β_0Γ<μ_0>
∘α_1 ∘α_0Γ<ν_2>

Γ<μ_0 ∘ν_0>

In fact, the second version of the interchange law follows from the first one and the equation that
expresses the naturality of $\Key{-}{-}$. Conversely, except the two laws for the identity 2-cell
and naturality, the given equations follow from either one of the two interchange laws.

While it is no longer necessary to prove that substitution is admissible in the setting of
the GAT, we would still like to show that explicit substitutions can be eliminated on closed terms.
The proof of canonicity implicitly contains such an algorithm, but that is overkill: a simple,
direct argument proves that explicit substitutions can be propagated down to variables. Moreover, we
may define the admissible operation mentioned in <ref> by

\begin{align*}
A^\alpha &\defeq \Sb{A}{\Key{\alpha}{\Gamma}}
M^\alpha &\defeq \Sb{M}{\Key{\alpha}{\Gamma}}
\end{align*}

We may then use the aforementioned algorithm to eliminate the keys.

Pushing substitutions under modalities

In order for the aforementioned algorithm to work, we must specify how substitutions commute with
the modal connectives of . Unlike previous work <cit.>, the
necessary equations are straightforward:

\begin{align*}
\Sb{\Modify{A}}{\delta} &= \Modify{\Sb{A}{\LockSb{\delta}}} &
\Sb{\MkBox{M}}{\delta} &= \MkBox{\Sb{M}{\LockSb{\delta}}}
\end{align*}

This simplicity is not coincidental. Previous modal type theories included rules that, in one way or
another, trimmed the context during type checking: some removed
variables <cit.>, while others erased context
formers,  locks <cit.>. In either case, it was necessary to show
that the trimming operation, which we may write as $\Verts{\Gamma}$, is functorial: $\Gamma \vdash
\delta : \Delta$ should imply $\Verts{\Gamma} \vdash \Verts{\delta} : \Verts{\Delta}$.
Unfortunately, the proof of this fact is almost always very complicated. Some type theories avoid it
by `forcing' substitution to be admissible using delayed substitutions <cit.>, but this causes serious complications in the equational theory.

circumvents this by avoiding any context trimming. As a result, we need neither delayed
substitutions nor a complex proof of admissibility.

§ MODELS

In the preceding section we presented the formal definition of  in the form of a GAT. As a
consequence we automatically obtained a category of models of , as well as
(strict) homomorphisms between them <cit.>. Moreover, this
category of models had an initial object,  the syntax of  itself. This category of models
is inhabited by algebras for this GAT. Hence, showing that a mathematical structure is a model of
becomes a laborious task: one must show that each and every construct can be interpreted in a
manner that makes the postulated equations hold. In this section we shall take on the task of
decomposing these algebraic models into more tractable pieces.

A moment's thought reveals that many of the equations of the GAT given in <ref>
are rather close to the familiar notion of categories with families
(CwFs) <cit.>, which can be adapted to the present setting.[The conference
version of this paper used such a presentation in the interest of brevity.] However, we will take
things a bit further by opting for a category-theoretic reformulation of CwFs known as natural
models <cit.>.

Natural models build on the view of CwFs as consisting of a presheaf of types (over the category of
contexts), coupled with a presheaf of terms (over the elements of those types). We find this
relatively recent technology helpful for two reasons. First, it concisely encodes the many
naturality conditions normally required of a CwF. Second, it aids in uncovering the implicit
universal properties of type-theoretic connectives, which are not quite so evident in the usual
GAT-like formulation of CwFs.

In <ref> we demonstrate how the basic notions of context, type, term, and
context extension in  can be presented in terms of natural models. Then, in
<ref> we show how to interpret the various connectives—including the
modality—in the language of natural models; this discussion concludes with a concise definition of
a model of  in <ref>. Following that, in <ref>
we briefly discuss a strict notion of morphism of models.

§.§ Contexts, Types, and Terms

§.§.§ Contexts

First, we observe that a model of our type theory must contain a set of contexts at each mode $m \in
\Mode$. Equipped with the substitutions at the same mode, which can be composed associatively and
have the identity substitution as a unit, these sets are readily seen to form a category—the context category at $m \in \Mode$—for which we write $\InterpMode{m}$.

Moreover, recall that for $\IsCx{\Gamma}$ and $\mu : n \to m$ we have a context
$\IsCx{\LockCxV{\Gamma}}<n>$, and that this construction extends to substitutions in a functorial
fashion. Hence, we will require for each modality $\mu : n \to m$ a functor

\[
\InterpModal{\mu} : \InterpMode{m} \to \InterpMode{n}
\]

Similarly, each $\alpha : \mu \To \nu$ induces a natural transformation. Accordingly, a model should
come with a natural transformation

\[
\InterpKey{\alpha} : \InterpModal{\nu} \To \InterpModal{\mu}
\]

The equalities of the GAT require that the assignments $\mu \mapsto
\Lock_\mu$ and $\alpha \mapsto \Key{\alpha}{}$ be strictly 2-functorial. Thus, this part of the
model can be succinctly summarized as follows.

A modal context structure for a mode theory $\Mode$ is a (strict) 2-functor

\[
\Interp{-}  : \Coop{\Mode} \to \CAT_1
\]

where $\Coop{\Mode}$ is the 2-category $\Mode$ with the direction of both 1-cells and
2-cells reversed, and $\CAT_1$ is the full subcategory of (large) categories with a terminal

This double contravariance may seem peculiar at first sight. Recall that the 2-category $\Mode$
specifies the behaviour of the modal types $\Modify{-}$, which are supposed to have a
right-adjoint-like behaviour, with the corresponding left-adjoint-like operators being the lock
functors $\LockCx{-}$. Being left-adjoint-like, the interpretation $\InterpModal{-}$ of each lock
will behave with variance opposite to the specification of $\Mode$. Of course, this is merely an
analogy, as these constructions are not truly adjoint.

§.§.§ Types and Context Extension

The following definition plays a central role.

[Representable natural transformation]

Let $\mathbb{C}$ be a small category, and let $P, Q : \PSH{\mathbb{C}}$ be presheaves on
$\mathbb{C}$. A natural transformation $\alpha : P \Rightarrow Q$ is representable just if
for every $\Gamma : \mathbb{C}$ and $x : \Yo{\Gamma} \Rightarrow P$ there exists a $y :
\Yo{\Delta} \Rightarrow Q$ and a morphism $\gamma : \Delta \rightarrow \Gamma$ in $\mathbb{C}$
such that there is a pullback square

\[
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node[pullback] (Delta) {$\Yo{\Delta}$};
\node (El) [right = 3cm of Delta] {$Q$};
\node (Gamma) [below = 2cm of Delta] {$\Yo{\Gamma}$};
\node (UU) [below = 2cm of El] {$P$};
\path[->] (Delta) edge node [left] {$\Yo{\gamma}$} (Gamma);
\path[->] (Delta) edge node [above] {$y$} (El);
\path[->] (Gamma) edge node [below] {$x$} (UU);
\path[->] (El) edge node [right] {$\alpha$} (UU);
\end{tikzpicture}
\]

This enables a very succinct definition of a model of type theory <cit.>.

Let $\mathbb{C}$ be a small category with a terminal object $\mathbf{1}$, and let $\CTm{}, \CTy{}
: \PSH{\mathbb{C}}$. A natural model of type theory is a representable natural
transformation $\El{} : \CTm{} \Rightarrow \CTy{}$.

It is shown in op. cit. that this corresponds to the usual notion of CwF: the
representability of n $\El{} : \CTm{} \Rightarrow \CTy{}$ is a clever way to encode context
extension and comprehension in a manner that automatically ensures naturality with respect to
substitution: see also <cit.>. Moreover, one can use this economy to write down very
concise interpretations of type formers. Our objective here is to adapt this to modes and

To begin, given a mode $m \in \Mode$ we define two presheaves on the context category

\begin{align*}
\CTy{m}(\Gamma) &\defeq \Ty{m}[1](\Gamma) &
\CTm{m}(\Gamma) &\defeq
\{ \parens{A, M} \mid A \in \Ty{m}[1](\Gamma), M \in \Tm{m}(\Gamma, A) \}
\end{align*}

The first one maps a context at mode $m \in \Mode$ to the set of large types over it. The second one
maps a context to the set of pointed types, i.e. to the set of pairs consisting of a type and a term
of that type. The presheaf action is given by substitution. We immediately obtain a natural
transformation $\El{m} : \CTm{m} \Rightarrow \CTy{m}$: at each context $\Gamma$, $\El{m, \Gamma}$
projects a pair $(A, M)$ to the underlying type $A$. As a result, the fibres of $\El{m}$ are the
terms of a given type.

Context extension postulates that for any object $\Gamma : \InterpMode{m}$, modality $\mu
\in \Hom{n}{m}$, and large type $A \in \Ty{n}[1](\InterpModal{\mu}\Gamma)$ there exists an object
$\ECx{\Gamma}{A} : \InterpMode{m}$ along with a morphism and a term

\begin{align*}
\CWk :\Hom[\InterpMode{m}]{\ECx{\Gamma}{A}}{\Gamma} &&
\CVar \in \Tm{n}(\InterpModal{\mu}(\ECx{\Gamma}{A}),\Sb{A}{\InterpModal{\mu}(\CWk)})
\end{align*}

The object $\ECx{\Gamma}{A}$ is universal with respect to $\CWk$ and $\CVar$: for any $\gamma \in
\Hom[\InterpMode{m}]{\Delta}{\Gamma}$ and term $M \in
\Tm{n}(\InterpModal{\mu}\Delta,\Sb{A}{\LockSb{\gamma}})$ there is a unique $\ESb{\gamma}{M} :
\Delta \to \ECx{\Gamma}{A}$ such that

∘(γM)    = γ      : Δ→Γ

= M       : n(μ(Γ),Aγ)

As usual, (<ref>) is only well-typed because of (<ref>). The only difference to the usual context extension of CwFs is that $A$ and $\Gamma$ are in different modes.

This can be encoded in the style of natural models as follows. We write $\YoEm{-}$ for the Yoneda
isomorphism. Given $\mu : \Hom[\Mode]{n}{m}$, context $\Gamma : \InterpMode{m}$, and a type $A :
\Ty{n}[1]{\parens{\InterpModal{\mu}(\Gamma)}}$, there is a chosen context $\Gamma'$ (cf.
$\ECx{\Gamma}{A}$), a chosen morphism $\CWk : \Gamma' \to \Gamma$, and a chosen morphism
$\YoEm{\CVar} : \Yo{\InterpModal{\mu}\Gamma'} \to \CTm{n}$ that make the following square commute:

\[
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node (Gammax) {$\Yo{\InterpModal{\mu}{\Gamma'}}$};
\node (El) [right = 3cm of Gammax] {$\CTm{n}$};
\node (Gamma) [below = 1.5cm of Gammax] {$\Yo{\InterpModal{\mu}{\Gamma}}$};
\node (UU) [below = 1.5cm of El] {$\CTy{n}$};
\path[->] (Gammax) edge node [left] {$\Yo{\InterpModal{\mu}\CWk}$} (Gamma);
\path[->] (Gammax) edge node [above] {$\YoEm{\CVar}$} (El);
\path[->] (Gamma) edge node [below] {$\YoEm{A}$} (UU);
\path[->] (El) edge node [right] {$\El{n}$} (UU);
\end{tikzpicture}
\]

We have surreptitiously `decoded' the top arrow into a term $\CVar \in
\Tm{n}(\InterpModal{\mu}(\Gamma'),\Sb{A}{\InterpModal{\mu}\CWk})$.

The universality of these objects is expressed by asking that for a given $\Delta : \InterpMode{m}$,
$\gamma : \Hom[\InterpMode{m}]{\Delta}{\Gamma}$, and $\YoEm{M} : \Yo{\InterpModal{\mu}\Delta}
\Rightarrow \CTm{n}$, there must be a unique morphism $\gamma' : \Delta \to \Gamma'$ (which stands
for $\ESb{\gamma}{M}$) such that the following square commutes:

\[
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node (Delta) {$\Yo{\InterpModal{\mu}(\Delta)}$};
\node (Gammax) [below right = 2cm and 2cm of Delta] {$\Yo{\InterpModal{\mu}{\Gamma'}}$};
\node (El) [right = 4cm of Gammax] {$\CTm{n}$};
\node (Gamma) [below = 2cm of Gammax] {$\Yo{\InterpModal{\mu}\Gamma}$};
\node (UU) [below = 2cm of El] {$\CTy{n}$};
\path[->, densely dashed] (Delta) edge node[upright desc] {$\Yo{\InterpModal{\mu}{\gamma'}}$} (Gammax);
\path[->, bend right] (Delta) edge node[upright desc] {$\Yo{\InterpModal{\mu}\gamma}$} (Gamma);
\path[->, bend left]  (Delta) edge node[upright desc] {$\YoEm{M}$} (El);
\path[->] (Gammax) edge node [upright desc] {$\Yo{\InterpModal{\mu}\CWk}$} (Gamma);
\path[->] (Gammax) edge node [above] {$\YoEm{\CVar}$} (El);
\path[->] (Gamma) edge node [below] {$\YoEm{A}$} (UU);
\path[->] (El) edge node [right] {$\El{n}$} (UU);
\end{tikzpicture}
\]

This diagram is not a pullback, but we can make it into one. Recall that for any functor $f :
\mathcal{C} \to \mathcal{D}$ we can define the precomposition functor $\Pre{f} : \PSH{\mathcal{D}}
\to \PSH{\mathcal{C}}$ by

\[
\Pre{f}(P) \defeq \Op{\mathcal{C}} \xrightarrow{\Op{f}} \Op{\DD} \xrightarrow{P} \SET
\]

Then, for any $c : \mathcal{C}$ and $Q : \PSH{\mathcal{D}}$ we can use the Yoneda lemma to establish
a series of natural isomorphisms

\[
\Hom[\PSH{\mathcal{D}}]{\Yo{f(c)}}{Q}
\cong
\Pre{f}{Q}(c)
\cong
\Hom[\PSH{\mathcal{C}}]{\Yo{c}}{\Pre{f}{Q}}
\]

We can then transpose the diagram in order to obtain

\begin{equation}
\begin{tikzpicture}[node distance=2.5cm, on grid, baseline=(current  bounding  box.center)]
\node (Delta) {$\Yo{\Delta}$};
\node (Gammax) [below right = 2cm and 2cm of Delta] {$\Yo{\Gamma'}$};
\node (El) [right = 4cm of Gammax] {$\Pre{\InterpModal{\mu}}{\CTm{n}}$};
\node (Gamma) [below = of Gammax] {$\Yo{\Gamma}$};
\node (UU) [below = of El] {$\Pre{\InterpModal{\mu}}{\CTy{n}}$};
\path[->, densely dashed] (Delta) edge node[upright desc] {$\gamma'$} (Gammax);
\path[->, bend right] (Delta) edge node[upright desc] {$\gamma$} (Gamma);
\path[->, bend left]  (Delta) edge node[upright desc] {$\YoEm{M}$} (El);
\path[->] (Gammax) edge node [left] {$\Yo{\CWk}$} (Gamma);
\path[->] (Gammax) edge node [above] {$\YoEm{\CVar}$} (El);
\path[->] (Gamma) edge node [below] {$\YoEm{A}$} (UU);
\path[->] (El) edge node [right] {$\Pre{\InterpModal{\mu}}{\El{n}}$} (UU);
\end{tikzpicture}
\label{diag:modal-natural-model}
\end{equation}

where $\gamma' : \Delta \to \Gamma'$ is the unique arrow that makes the diagram commute.
The requirement that this diagram be a pullback leads us to the following definition.

A modal natural model on a context structure $\Interp{-}  : \Coop{\Mode} \to \CAT_1$
consists of a family of natural transformations of presheaves

\[
\parens*{\El{m} : \CTm{m} \Rightarrow \CTy{m}}_{m \in \Mode}
\]

where $\CTm{m}, \CTy{m} : \PSH{\InterpMode{m}}$ such that for every $\mu : \Hom[\Mode]{m}{n}$ the
natural transformation

\[
\Pre{\InterpModal{\mu}}{\El{n}} :
\Pre{\InterpModal{\mu}}{\CTm{n}} \To \Pre{\InterpModal{\mu}}{\CTy{n}}
\]

is a natural model.

We will write $\ECx{\Gamma}{A}$ for the object $\Gamma'$ that makes (<ref>)
a pullback, as we do in the type theory.

§.§ Connectives

We shall only discuss the key cases of $\Pi$ types, modal types, Boolean types, and universes. The
interpretation of the other connectives largely follows the style of <cit.>. More
details can be found in the tech report <cit.>.

§.§.§ $\Pi$ Structure

Even though  $\Pi$ types are close to traditional $\Pi$ types they are not quite the same, as
they involve a modality in the domain. Thus, we need to construct an appropriate variation of the
interpretation given by <cit.>. To begin, we need some way to represent the
binding of an additional assumption. This is achieved through the use of polynomial
Given a `display map' $\ell : E \to B$ we define a polynomial endofunctor $\Poly{\ell : E \to B} :
\PSH{\InterpMode{m}} \to \PSH{\InterpMode{m}}$ by[This is given in the internal language,
but may also be written purely categorically, as is done in op. cit.]

\[
\Poly{\ell : E \to B}{A} \defeq \sum_{b : B} A^{\ReIdx{\ell}{b}}
\]

When specialized to the `modalized' natural model $\ell \defeq \Pre{\InterpModal{\mu}}(\tau_n) :
\Pre{\InterpModal{\mu}}{\CTm{n}} \To \Pre{\InterpModal{\mu}}{\CTy{n}}$, this functor has a useful
property: morphisms $\Yo{\Gamma} \To \Poly{\Pre{\InterpModal{\mu}}{\El{n}}}{\CTy{m}}$ are in
bijection with tuples

\begin{equation}
\parens{A \in \CTy{n}(\InterpModal{\mu}(\Gamma)), B \in \CTy{m}(\ECx{\Gamma}{A})}
\label{eq:semantics:binding-pair}
\end{equation}

This enables the representation of a pair of types $\IsTy[\LockCx{\Gamma}]{A}[1]<n>$ and
$\IsTy[\ECx{\Gamma}{A}]{B}[1]<m>$—i.e. the premises of $\Pi$ formation—as a single morphism
$\Yo{\Gamma} \To \Poly{\Pre{\InterpModal{\mu}}{\El{n}}}{\CTy{n}}$. A similar observation applies to
the presheaf of terms $\CTm{m}$. See <cit.> for a detailed proof of this

A model is equipped with a $\prod$-structure if for $\mu : \Hom[\Mode]{n}{m}$ we have a pullback

\[
\begin{tikzpicture}[node distance=1.75cm, on grid]
\node[pullback] (PiTm) {$\Poly{\Pre{\InterpModal{\mu}}{\El{n}}}{\CTm{m}}$};
\node (Tm) [right = 4cm of PiTm] {$\CTm{m}$};
\node (PiTy) [below = of PiTm] {$\Poly{\Pre{\InterpModal{\mu}}{\El{n}}}{\CTy{m}}$};
\node (Ty) [below = of Tm] {$\CTy{m}$};
\path[->] (PiTm) edge node [left] {} (PiTy);
\path[->] (PiTm) edge node [above] {$\CLam$} (Tm);
\path[->] (PiTy) edge node [below] {$\CPi$} (Ty);
\path[->] (Tm) edge node [right] {$\El{m}$} (Ty);
\end{tikzpicture}
\]

The lower morphism $\prod$ models the formation rule: the premises of the rule constitute a pair of
the form (<ref>). We may thus combine them into an arrow $\Yo{\Gamma} \To
\Poly{\Pre{\InterpModal{\mu}}{\El{n}}}{\CTy{n}}$, and then postcompose $\prod$ to obtain a morphism
$\Yo{\Gamma} \To \CTy{m}$, i.e. a type at mode $m$ in context $\IsCx{\Gamma}$. In a similar fashion,
the top morphism $\CLam$ models the introduction rule. The $\beta$ and $\eta$ laws then follow from
the pullback property of the square: see <cit.>.

§.§.§ Modal Structure

The interpretation of the modal types is a bit more involved. Intuitively, the reason is that
$\Modify{A}$ behaves like a positive type former, i.e. one with a `let-style'
pattern-matching eliminator, and no $\eta$-rule. These features render its behaviour closer to that
of intensional identity types.

First, for each $\mu : \Hom[\Mode]{n}{m}$ the formation and introduction rules for $\Modify{-}$ are
given by a commuting square

\begin{equation}
\begin{tikzpicture}[node distance=2.5cm, on grid, baseline=(current  bounding  box.center)]
\node (ModTm) {$\Pre{\InterpModal{\mu}}{\CTm{n}}$};
\node (Tm) [right = 4cm of ModTm] {$\CTm{m}$};
\node (ModTy) [below = 1.75cm of ModTm] {$\Pre{\InterpModal{\mu}}{\CTy{n}}$};
\node (Ty) [below = 1.75cm of Tm] {$\CTy{m}$};
\path[->] (ModTm) edge node [left] {$\Pre{\InterpModal{\mu}}{\El{n}}$} (ModTy);
\path[->] (ModTm) edge node [above] {$\CMkBox$} (Tm);
\path[->] (ModTy) edge node [below] {$\CModify$} (Ty);
\path[->] (Tm) edge node [right] {$\El{m}$} (Ty);
\end{tikzpicture}
\label{diag:form-intro-modal}.
\end{equation}

By Yoneda, every type $\IsTy[\LockCx{\Gamma}]{A}[1]<n>$ can be seen as a morphism $\Yo{\Gamma} \To
\Pre{\InterpModal{\mu}}{\El{n}}$. Postcomposition with $\CModify$ gives a morphism $\Yo{\Gamma} \To
\CTy{m}$, which constitutes the interpretation of the type $\IsTy[\Gamma]{\Modify{A}}[1]<m>$.
$\CMkBox$ interprets the introduction rule in a similar fashion. Nevertheless, asking that this
square be a pullback is stronger than the elimination rule. In Section <ref> we
shall see that states that $\CModify$ is a dependent right adjoint.

Instead, we will model our elimination rule by a lifting structure. We phrase this definition
in the internal language of the presheaf topos $\PSH{\InterpMode{m}}$,  extensional type
theory.[This is derived from unpublished work by Jon Sterling, Daniel Gratzer, Carlo
Angiuli, and Lars Birkedal.] This has a serious technical advantage: as the definition is given in
an empty context, the given lifts are automatically natural.

[Left lifting structure]

Given $\vdash A, I, B\ \mathsf{type}$, a family $b : B \vdash E[b]\ \mathsf{type}$ and a section
$a : A \vdash i[a] : I$, we define the type $\vdash i[-]\pitchfork E[-]\ \mathsf{type}$ of
left lifting structures for $i$ with respect to $E$ to be

\[
\textstyle
i[-] \pitchfork E[-] \triangleq
\prod_{C: I \to B}
\prod_{c: \prod_{a:A} E[C(i[a])]}
\braces*{
j:\prod_{p:I} E[C(p)]
\mid
\forall a:A.\
\]

Informally, left lifting structures provide diagonal fillers for the diagram

\[
\begin{tikzpicture}[on grid, node distance = 1.75cm]
\node (A) {$A$};
\node (I) [below = of A] {$I$};
\node (E) [right = 4.5cm of A] {$\sum_{b : B} E[b]$};
\node (B) [below = of E] {$B$};
\path[->] (A) edge node [above] {$\angles{C(i[-]), c}$} (E);
\path[->] (A) edge node [left] {$i[-]$} (I);
\path[->] (E) edge node [right] {$\pi_1$} (B);
\path[->] (I) edge node [below] {$C$} (B);
\path[->, densely dotted] (I) edge node [upright desc] {$j$} (E);
\end{tikzpicture}
\]

Intuitively, $C : I \to B$ is the motive of an elimination: we would like to prove $E[C(p)]$
for all $p : I$. At the same time, $c : \prod_{a : A} E[C(i[a])]$ is a given section that specifies
the desired computational behaviour of this elimination at the `special case' $A$. The left lifting
structure then provides a section $j$ of $E[-]$ defined on all of $I$. This section is above $C$,
and extends $c$.  Note that these fillers are not necessarily unique.  Moreover, they are
automatically natural: as all the types involved in this definition are closed, we are at
liberty to weaken the context.

This style of lifting structure is an essential ingredient in recent work on models of intensional
identity types. First, they play an important rôl̂ê in natural models: <cit.> shows that they precisely correspond to enriched left lifting properties in the
sense of categorical homotopy theory <cit.>. In fact, the above definition
given above is a word-for-word restatement in the internal language. Second, such lifting structures
are also central devices in internal presentations of models of cubical type theory, in particular
the recent work of <cit.>.

We can now approach this in a manner similar to intensional identity types in op. cit. Recall
that the elimination rule for $\Modify[\nu]{A}$ is

\[
\inferrule{
\nu : \Hom[\Mode]{o}{n} \\
\mu : \Hom[\Mode]{n}{m} \\
\IsCx{\Gamma} \\
\IsTy[\LockCx{\LockCx{\Gamma}}<\nu>]{A}[1]<o> \\
\IsTm[\LockCx{\Gamma}]{M_0}{\Modify[\nu]{A}}<n> \\
\IsTy[\ECx{\Gamma}{\Modify[\nu]{A}}]{B}[1] \\
\IsTm[\ECx{\Gamma}{A}<\mu \circ \nu>]{M_1}{\Sb{B}{\ESb{\Wk}{\MkBox[\nu]{\Var{0}}}}}
\IsTm{\Open{M_0}{M_1}<\nu>[\mu]}{\Sb{B}{\ESb{\ISb}{M_0}}}
\]

First, we must to remove the `implicit cut' with $M_0$. We construct the substitution

\[
\IsSb[ \ECx{\ECx{\Gamma}{\Modify[\nu]{A}}}{\Sb{A}{\LockSb{\Wk}<\mu \circ \nu>}}<\mu \circ \nu> ]
{\sigma \defeq \ESb{\Wk[2]}{\Var{0}}}{\ECx{\Gamma}{A}<\mu \circ \nu>}
\]

It then suffices to construct the elimination rule

\[
\inferrule{
\nu : \Hom[\Mode]{o}{n} \\
\mu : \Hom[\Mode]{n}{m} \\
\IsCx{\Gamma} \\
\IsTy[\LockCx{\LockCx{\Gamma}}<\nu>]{A}[1]<o> \\
\IsTy[\ECx{\Gamma}{\Modify[\nu]{A}}]{B}[1] \\
\IsTm[\ECx{\Gamma}{A}<\mu \circ \nu>]{M_1}{\Sb{B}{\ESb{\Wk}{\MkBox[\nu]{\Var{0}}}}}
\IsTm[\ECx{\Gamma}{\Modify[\nu]{A}}]{\Open{\Var{0}}{\Sb{M_1}{\sigma}}<\nu>[\mu]}{B}
\]

because we can calculate that

\[
\EqTm[\Gamma]{
\Sb{\parens{\Open{\Var{0}}{\Sb{M_1}{\sigma}}<\nu>[\mu]}}{\ESb{\ISb}{M_0}}
\Open{M_0}{M_1}<\nu>[\mu]
\]

We can rephrase this as the existence of a diagonal filler in the diagram

\[
\begin{tikzpicture}[on grid, node distance = 2.5cm]
\node (Base) {$\Yo{\ECx{\Gamma}{A}<\mu \circ \nu>}$};
\node (Motive) [below = 2cm of Base] {$\Yo{\ECx{\Gamma}{\Modify[\nu]{A}}}$};
\node (Tm) [right = 6cm of Base] {$\CTm{m}$};
\node (Ty) [below = 2cm of Tm] {$\CTy{m}$};
\path[->] (Tm) edge node [right] {$\El{m}$} (Ty);
\path[->] (Base) edge node [left] {$\Yo{\ESb{\Wk}{\MkBox[\nu]{\Var{0}}}}$} (Motive);
\path[->] (Motive) edge node [below] {$\YoEm{B}$} (Ty);
\path[->] (Base) edge node [above] {$\YoEm{\Sb{M_1}{\sigma}}$} (Tm);
\path[->] (Motive) edge node [upright desc] {$\YoEm{\Open{\Var{0}}{\Sb{M_1}{\sigma}}<\nu>[\mu]}$}(Tm);
\end{tikzpicture}
\]

We can use a left lifting structure on a carefully chosen slice category to obtain such diagonal
fillers. The internal language approach still applies because of the well-known lemma stating that
the slice of a presheaf topos is also a presheaf topos, but over the corresponding category of
elements. In symbols, for any $P : \PSH{\CC}$ we have an equivalence $\SLICE{\PSH{\CC}}{P} \Equiv
\PSH{\int_\CC P}$: see <cit.>

First, given $\nu : \Hom[\Mode]{o}{n}$ we construct the following pullback:

\[
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node (ModTm) {$\Pre{\InterpModal{\nu}}{\CTm{o}}$};
\node[pullback] (M) [below right = 1cm and 2cm of ModTm] {$M$};
\node (Tm) [right = 4cm of M] {$\CTm{n}$};
\node (ModTy) [below = 1.75cm of M] {$\Pre{\InterpModal{\nu}}{\CTy{o}}$};
\node (Ty) [below = 1.75cm of Tm] {$\CTy{n}$};
\path[->, densely dashed] (ModTm) edge node [upright desc] {$m$} (M);
\path[->] (M) edge node {} (Tm);
\path[->] (M) edge node[left] {$h$} (ModTy);
\path[->] (ModTm) edge[bend right] node [left] {$\Pre{\InterpModal{\nu}}{\El{o}}$} (ModTy);
\path[->] (ModTm) edge[bend left] node [above] {$\CMkBox[\nu]$} (Tm);
\path[->] (ModTy) edge node [below] {$\CModify[\nu]$} (Ty);
\path[->] (Tm) edge node [right] {$\El{n}$} (Ty);
\end{tikzpicture}
\]

The outer commuting square is that given by the formation and introduction for $\Modify[\nu]{-}$, as
in (<ref>). Intuitively, $M$ is a `generic $\nu$-modal terms object' that
consists of terms $\IsTm[\Gamma]{M}{\Modify[\nu]{A}}<n>$, where
$\IsTy[\LockCx{\Gamma}<\nu>]{A}[1]<o>$. We know that $\Pre{\InterpModal{\mu}}$ has a left adjoint,
so it preserves pullbacks. Applying it to this diagram yields

\begin{equation}
\begin{tikzpicture}[node distance=2.5cm, on grid, baseline=(current  bounding  box.center)]
\node (ModTm) {$\Pre{\InterpModal{\mu \circ \nu}}{\CTm{o}}$};
\node[pullback] (M) [below right = 1cm and 3.25cm of ModTm] {$\Pre{\InterpModal{\mu}}{M}$};
\node (Tm) [right = 4.5cm of M] {$\Pre{\InterpModal{\mu}}{\CTm{n}}$};
\node (ModTy) [below = of M] {$\Pre{\InterpModal{\mu \circ \nu}}{\CTy{o}}$};
\node (Ty) [below = of Tm] {$\Pre{\InterpModal{\mu}}{\CTy{n}}$};
\path[->, densely dashed] (ModTm) edge node [above] {$\Pre{\InterpModal{\mu}}{m}$} (M);
\path[->] (M) edge node {} (Tm);
\path[->] (M) edge node[left] {$\Pre{\InterpModal{\mu}}{h}$} (ModTy);
\path[->] (ModTm) edge[bend right] node [left] {$\Pre{\InterpModal{\mu \circ \nu}}{\El{o}}$} (ModTy);
\path[->] (ModTm) edge[bend left] node [above] {$\Pre{\InterpModal{\mu}}{\CMkBox[\nu]}$} (Tm);
\path[->] (ModTy) edge node [below] {$\Pre{\InterpModal{\mu}}{\CModify[\nu]}$} (Ty);
\path[->] (Tm) edge node [right] {$\Pre{\InterpModal{\mu}}{\El{n}}$} (Ty);
\end{tikzpicture}
\label{diag:pullback-generic-modal}
\end{equation}

We have also used the fact that $\Pre{(-)}$ is functorial to contract the two locks into
one. Moreover, we get that the unique mediating morphism is indeed $\Pre{\InterpModal{\mu}}{m}$.

From this point onwards we will also work in the slice $\SLICE{\PSH{\InterpMode{m}}}{Z}$, where $Z
\defeq \Pre{\InterpModal{\mu \circ \nu}}{\CTy{o}}$. In order to model the elimination rule
we will ask for a left lifting structure in the slice category, of type

\begin{equation}
\vdash \COpen[\nu]^\mu :
\Pre{\InterpModal{\mu}}{m}
\pitchfork
\Pre*{Z}{\El{m}} % \Pre*{(\Pre{\InterpModal{\mu \circ \nu}}{\CTy{o}})}{\El{m}[-]}
\label{eq:semantics:modal-elimination-structure}
\end{equation}

where both of these are considered as morphisms in the slice $\SLICE{\PSH{\InterpMode{m}}}{Z}$,
respectively of type

\begin{align*}
\Pre{\InterpModal{\mu}}{m} :\
&\Pre{\InterpModal{\mu \circ \nu}}{\El{o}} \to \Pre{\InterpModal{\mu}}{h} \\
\Pre*{Z}{\El{m}} :\
&\Pre*{Z}{\CTm{m}} \to \Pre*{Z}{\CTy{m}}
\end{align*}

Following <cit.> we may calculate that this models the rule. We suppose its
premises, and construct the diagram of Figure <ref>.

[node distance=2.5cm, on grid]
(Cx-munu-A)  $\Yo{\ECx{\Gamma}{A}<\mu \circ \nu>}$;
[pullback] (Cx-mu-nu-A) [below = 4cm of Cx-munu-A] $\Yo{\ECx{\Gamma}{\Modify[\nu]{A}}}$;
(Tm-munu-o) [right = 5cm of Cx-munu-A] $\Pre{\InterpModal{\mu \circ \nu}}{\CTm{o}}$;
[pullback] (M) [below = 4cm of Tm-munu-o] $\Pre{\InterpModal{\mu}}{M}$;
(Cx) [below = 3cm of Cx-mu-nu-A] $\Yo{\Gamma}$;
(Ty-munu-o) [below = 3cm of M] $\Pre{\InterpModal{\mu \circ \nu}}{\CTy{o}}$;
(Tm-mu-n) [right = 4cm of M] $\Pre{\InterpModal{\mu}}{\CTm{n}}$;
(Ty-mu-n) [below = 3cm of Tm-mu-n] $\Pre{\InterpModal{\mu}}{\CTy{n}}$;
[->, densely dashed] (Cx-munu-A) edge node [upright desc]
$\Yo{\ESb{\CWk}{\CMkBox[\nu](\CVar)}}$ (Cx-mu-nu-A);
[->] (Cx-mu-nu-A) edge node[upright desc] $\Yo{\CWk}$ (Cx);
[->] (Cx-munu-A) edge node[upright desc] $\YoEm{\CVar}$ (Tm-munu-o);
[->] (Tm-munu-o) edge node[upright desc] $\Pre{\InterpModal{\mu}}{m}$ (M);
[->] (Tm-munu-o) edge node[upright desc] $\Pre{\InterpModal{\mu}}{\CMkBox[\nu]}$ (Tm-mu-n);
[->] (Tm-mu-n) edge node[right] $\Pre{\InterpModal{\mu}}{\El{n}}$ (Ty-mu-n);
[->] (Cx) edge[bend right] node[below] $\YoEm{\Modify[\nu]{A}}$ (Ty-mu-n);
[->] (Cx) edge node[upright desc] $\YoEm{A}$ (Ty-munu-o);
[->] (Ty-munu-o) edge node[below] $\Pre{\InterpModal{\mu}}{\CModify[\nu]}$ (Ty-mu-n);
[->] (Cx-munu-A) edge[bend left = 60] node[above, near start] $\YoEm{\MkBox[\nu]{\CVar}}$ (Tm-mu-n);
[->] (M) edge node[upright desc] $\Pre{\InterpModal{\mu}}{h}$ (Ty-munu-o);
[->] (M) edge (Tm-mu-n);
[->] (Cx-munu-A) edge[bend right = 50] node[left] $\Yo{\CWk}$ (Cx);
[->, densely dashed] (Cx-mu-nu-A) edge (M);
[->] (Cx-mu-nu-A) edge[bend left = 20] node[near start, upright desc] $\YoEm{\CVar}$ (Tm-mu-n);
[->] (Tm-munu-o) edge[bend right = 40] node[near start, left]
$\Pre{\InterpModal{\mu \circ \nu}}{\El{o}}$ (Ty-munu-o);

Modelling the elimination rule

The right (both top and bottom) part of the diagram is just (<ref>). The
bottom composite is easily seen to correspond to the application of the introduction rule of
$\Modify[\nu]{-}$ to the type $\IsTy[\LockCx{\LockCx{\Gamma}}<\nu>]{A}[1]<o>$, and hence to the type
$\IsTy[\LockCx{\Gamma}]{\Modify[\nu]{A}}[1]<n>$. The outer bottom square is the natural model pullback
square that defines the object $\ECx{\Gamma}{\Modify[\nu]{A}}$, and we thus get a mediating morphism
to $\Pre{\InterpModal{\mu}}{M}$, and that the bottom-left square is also a pullback. The left (both
top and bottom) part of the diagram is the natural model pullback square that defines the object
$\ECx{\Gamma}{\Modify[\mu \circ \nu]{A}}$. We hence get a mediating morphism
$\ESb{\CWk}{\CMkBox[\nu](\CVar)} : \ECx{\Gamma}{\Modify[\mu \circ \nu]{A}} \to
\ECx{\Gamma}{\Modify[\nu]{A}}$. Finally, for the same reasons as the bottom composite, the top
composite is easily seen to correspond to the term $\MkBox[\nu]{\CVar}$.

We write $\sum_Z : \SLICE{\PSH{\InterpMode{m}}}{Z} \to \PSH{\InterpMode{m}}$ for the usual domain
projection functor, so that $\sum_Z \dashv Z^*$. Now, using the usual approach to slice
categories—where the cartesian product $\times_Z$ is the pullback—we see from the diagram that

\begin{equation}
\begin{aligned}
\sum_Z\parens{\YoEm{A} \times_Z \Pre{\InterpModal{\mu \circ \nu}}{\CTm{o}}}
\Yo{\ECx{\Gamma}{A}<\mu \circ \nu>} \\
\sum_Z\parens{\YoEm{A} \times_Z \Pre{\InterpModal{\mu}}{h}}
\Yo{\ECx{\Gamma}{\Modify[\nu]{A}}<\mu>} \\
\sum_Z\parens{\ISb_{\YoEm{A}} \times_Z \Pre{\InterpModal{\mu}}{m}}
\Yo{\ESb{\CWk}{\CMkBox[\nu](\CVar)}}
\end{aligned}
\label{eq:modal-lift-isos}
\end{equation}

Recall that we are trying to find a diagonal filler to the $\PSH{\InterpMode{m}}$ diagram

\begin{equation}
\begin{tikzpicture}[on grid, node distance = 2.5cm, baseline=(current  bounding  box.center)]
\node (Base) {$\Yo{\ECx{\Gamma}{A}<\mu \circ \nu>}$};
\node (Motive) [below = 2cm of Base] {$\Yo{\ECx{\Gamma}{\CModify[\nu](A)}<\mu>}$};
\node (Tm) [right = 6cm of Base] {$\CTm{m}$};
\node (Ty) [below = 2cm of Tm] {$\CTy{m}$};
\path[->] (Tm) edge node [right] {$\El{m}$} (Ty);
\path[->] (Base) edge node [left] {$\Yo{\ESb{\CWk}{\CMkBox[\nu](\CVar)}}$} (Motive);
\path[->] (Motive) edge node [below] {$\YoEm{B}$} (Ty);
\path[->] (Base) edge node [above] {$\YoEm{M_1}$} (Tm);
\path[->, densely dashed] (Motive) edge (Tm);
\end{tikzpicture}
\label{diag:modal-fill}
\end{equation}

We use the adjunction $\sum_Z \Adjoint Z^*$ to transpose this diagram, and we compose with the
isomorphisms (<ref>) to obtain the following diagram in

\[
\begin{tikzpicture}[on grid, node distance = 2.5cm]
\node (Base) {$\YoEm{A} \times_Z \Pre{\InterpModal{\mu \circ \nu}}{\CTm{o}}$};
\node (Motive) [below = of Base]
{$\YoEm{A} \times_Z \Pre{\InterpModal{\mu}}{h}$};
\node (Tm) [right = 6cm of Base] {$Z^*\parens{\CTm{m}}$};
\node (Ty) [below = of Tm] {$Z^*\parens{\CTy{m}}$};
\path[->] (Tm) edge node [right] {$Z^*\parens{\El{m}}$} (Ty);
\path[->] (Base) edge node [left] {$\ISb \times_Z \Pre{\InterpModal{\mu}}m$} (Motive);
\path[->] (Motive) edge node [below] {$\Transpose{\YoEm{B}}$} (Ty);
\path[->] (Base) edge node [above] {$\Transpose{\YoEm{M_1}}$} (Tm);
\path[->, densely dashed] (Motive) edge node [upright desc] {$\COpen[\nu]^\mu$}(Tm);
\end{tikzpicture}
\]

We may then use the lifting structure to prove a diagonal filler, and transpose backwards along the
adjunction to obtain a filler for (<ref>). The naturality of all these steps
(composing isomorphisms, transposition, and lifting structure) ensure that the choice is natural.

§.§.§ Boolean Structure

A boolean structure is defined similarly to the structure for modal types. First, we require
two constants, as well as naturally given diagonal fillers for the appropriate squares:

\[
\begin{tikzpicture}[node distance=1.5cm, on grid]
\node (BoolTm) {$1$};
\node (Tm) [right = 4cm of BoolTm] {$\CTm{m}$};
\node (BoolTy) [below = 1.5cm of BoolTm] {$1$};
\node (Ty) [below = 1.5cm of Tm] {$\CTy{m}$};
\draw[double, double distance=1.5pt] (BoolTm) -- (BoolTy);
\path[->] (BoolTm) edge[bend left=20] node [above] {$\CTrue$} (Tm);
\path[->] (BoolTm) edge[bend right=20] node [below] {$\CFalse$} (Tm);
\path[->] (BoolTy) edge node [below] {$\CBool$} (Ty);
\path[->] (Tm) edge node [right] {$\El{m}$} (Ty);
\end{tikzpicture}
\quad
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node (Term) {$1 + 1$};
\node (Tm) [right = 3cm of Term] {$\CTm{m}$};
\node (Motive) [below = 2cm of Term] {$\ReIdx{\El{m}}{\CBool}$};
\node (Ty) [below = 2cm of Tm] {$\CTy{m}$};
\path[->] (Term) edge node [left] {$[\CTrue,\CFalse]$} (Motive);
\path[->] (Term) edge node [above] {} (Tm);
\path[->] (Motive) edge node [below] {} (Ty);
\path[->] (Tm) edge node [right] {$\El{m}$} (Ty);
\path[->,densely dotted] (Motive) edge node {} (Tm);
\end{tikzpicture}
\]

$\ReIdx{\El{m}}{\CBool}$ is the fibre of $\El{m}$ over $\CBool$, and the map $[\CTrue, \CFalse]$ is
obtained as the cotuple of the maps obtained by factoring $\CTrue$ and $\CFalse$ through the fibre.
Requiring a left lifting structure

\[
\CRec : \brackets*{\CTrue, \CFalse} \pitchfork \El{m}[-]
\]

in the internal language provides enough naturality to yield diagonal fillers for all squares

\[
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node (Gamma) {$\Yo{\Gamma} + \Yo{\Gamma}$};
\node (Tm) [right = 4cm of Gamma] {$\CTm{m}$};
\node (GammaB) [below = 2cm of Gamma] {$\Yo{\CECx{\Gamma}{\CBool}}$};
\node (Ty) [below = 2cm of Tm] {$\CTy{m}$};
\path[->] (Gamma) edge node [left] {$[\ESb{\ISb}{\CTrue},\ESb{\ISb}{\CFalse}]$} (GammaB);
\path[->] (Gamma) edge node [above] {} (Tm);
\path[->] (GammaB) edge node [below] {} (Ty);
\path[->] (Tm) edge node [right] {$\El{m}$} (Ty);
\path[->,densely dotted] (GammaB) edge node {} (Tm);
\end{tikzpicture}
\]

§.§.§ Universe

The universe itself is given by a presheaf $\CSTy{m}$ at each mode $m$. The Coquand-style
isomorphism is implemented by a natural transformation $\CUni : 1 \To \El{m}$, which stands for the
universe type at mode $m$, as well as a natural isomorphism

\[
\ReIdx{\El{m}}{\CUni} \cong \CSTy{m}
\]

As the pullback of $\El{m}$ along $\CUni$ is $\Yo{\CECx{1}{\CUni}}$, this exactly postulates an
isomorphism between terms of the universe and small types. The coercion from small to large type is
interpreted by a natural transformation $\CLift : \CSTy{m} \Rightarrow \CTy{m}$ that maps each small
type to its associated large type. Moreover, we ask that the formation rules factor through
small types: we require a mediating morphism in each of the following diagrams:[There are
also similar diagrams for $\Sigma$ and intensional identity types.]

\[
\begin{tikzpicture}[node distance = 2.5cm, on grid]
\node (SF) {$\Poly{\Pre{\InterpModal{\mu}}{\El{n}}}{\CSTy{m}}$};
\node (S) [right = 3.5cm of SF] {$\CSTy{m}$};
\node (TF) [below = 2cm of SF] {$\Poly{\Pre{\InterpModal{\mu}}{\El{n}}}{\CTy{m}}$};
\node (T) [below = 2cm of S] {$\CTy{m}$};
\path[->] (SF) edge node {} (TF);
\path[->, densely dotted] (SF) edge node {} (S);
\path[->] (S) edge node[right] {$\CLift$} (T);
\path[->] (TF) edge node[below] {$\CPi$} (T);
\end{tikzpicture}
\quad
\begin{tikzpicture}[node distance = 2.5cm, on grid]
\node (SF) {$\Pre{\InterpModal{\mu}}{\CSTy{n}}$};
\node (S) [right = 2.5cm of SF] {$\CSTy{m}$};
\node (TF) [below = 2cm of SF] {$\Pre{\InterpModal{\mu}}{\CTy{n}}$};
\node (T) [below = 2cm of S] {$\CTy{m}$};
\path[->] (SF) edge node {} (TF);
\path[->, densely dotted] (SF) edge node {} (S);
\path[->] (S) edge node[right] {$\CLift$} (T);
\path[->] (TF) edge node[below] {$\CModify$} (T);
\end{tikzpicture}
\quad
\begin{tikzpicture}[node distance = 2.5cm, on grid]
\node (SF) {$1$};
\node (S) [right = 2.5cm of SF] {$\CSTy{m}$};
\node (TF) [below = 2cm of SF] {$1$};
\node (T) [below = 2cm of S] {$\CTy{m}$};
\path[->] (SF) edge node {} (TF);
\path[->, densely dotted] (SF) edge node {} (S);
\path[->] (S) edge node[right] {$\CLift$} (T);
\path[->] (TF) edge node[below] {$\CBool$} (T);
\end{tikzpicture}
\]

These factorisations ensure that type formation is closed under small types, and commutation ensures
that the coercions commute with the type formers defintitionally.

§.§.§ The full definition

We have shown how to interpret each rule of  through natural models. In fact, every step of
our working is reversible: each contraption we have introduced precisely corresponds to the portion
of the generalized algebraic theory it was used to interpret. In summary, we can make the following

A model of  over $\Mode$ consists of

* a modal context structure for $\Mode$ (as in
Definition <ref>), and a

* a modal natural model on that context structure (as in
Definition <ref>)

such that the modal natural model supports

* dependent product types

* dependent sum types (at each mode)

* intensional identity types (at each mode)

* modal types

* a boolean type (at each mode), and

* a universe of small types.

§.§ Morphisms of Models

The generalized algebraic theory (GAT) of  also induces a notion of morphism between
models. Traditionally neglected, morphisms are of paramount importance when one produces semantic
proofs of metatheoretic properties, such as canonicity, a proof of which we will present in

The last decade has seen much use of relatively weak morphisms of CwFs,  morphisms which preserve
structures only up to isomorphism: see  <cit.>. However, our
proof of canonicity will require the strictest notion of CwF morphism,  a GAT homomorphism. Such
morphisms preserve all structure on-the-nose, including context extension, and were
introduced alongside CwFs by <cit.>. As we are using natural models, we will use an
adaptation due to <cit.>. We believe that one may construct a biequivalence
or biadjunction between a category based on strict morphisms and one based on weaker ones, as done
by  <cit.>, but we will leave that to future work.

[Strict morphism of natural models]

A morphism of natural models $(\CC, \Mor[\El{c}]{\CTm{c}}{\CTy{c}}) \to (\DD,
\Mor[\El{d}]{\CTm{d}}{\CTy{d}})$ comprises a functor $F : \CC \to \DD$ and a commuting diagram

\begin{equation}
\begin{tikzpicture}[on grid, node distance = 2.5cm, baseline=(current  bounding  box.center)]
\node (TmC) {$\CTm{c}$};
\node (TmD) [right = 4cm of TmC] {$\Pre{F}{\CTm{d}}$};
\node (TyC) [below = 2cm of TmC] {$\CTy{c}$};
\node (TyD) [below = 2cm of TmD] {$\Pre{F}{\CTy{d}}$};
\path[->] (TmC) edge node [left] {$\El{c}$} (TyC);
\path[->] (TmC) edge node [above] {$\widetilde{\varphi}$} (TmD);
\path[->] (TyC) edge node [below] {$\varphi$} (TyD);
\path[->] (TmD) edge node [right] {$\Pre{F}{\El{d}}$} (TyD);
\end{tikzpicture}
\label{diag:semantics:natmod-morphism}
\end{equation}

such that $F(\mathbf{1}) = \mathbf{1}$ and the canonical morphism $F(\CECx{\Gamma}{A}) \to
\CECx{F(\Gamma)}{\varphi(A)}$ is an identity.

The type $\varphi(A)$ in the last line is defined as follows. Given $\YoEm{A} : \Yo{\Gamma}
\Rightarrow \CTy{c}$ we let

\[
k \defeq \Yo{\Gamma} \xrightarrow{\YoEm{A}} \CTy{c} \xrightarrow{\varphi} \Pre{F}{\CTm{d}} \\
\]

By Yoneda this induces a natural isomorphism

\begin{equation}
\Hom[\PSH{\CC}]{\Yo{\Gamma}}{\Pre{F}{\CTy{d}}}
\cong
\Pre{F}{\CTy{d}}(\Gamma)
\CTy{d}(F(\Gamma))
\cong
\Hom[\PSH{\DD}]{\Yo{F\Gamma}}{\CTy{d}}
\label{eq:natmod-morphism-natiso}
\end{equation}

We define $\YoEm{\phi(A)} : \Yo{F\Gamma} \Rightarrow \CTy{d}$ to be $k$ transported under this isomorphism. Also, let

\[
\YoEm{M} : \Yo{\Gamma} \Rightarrow \CTy{c}
\quad
\longmapsto
\quad
\YoEm{\widetilde{\varphi}(M)} : \Yo{F(\Gamma)} \Rightarrow \CTy{d}
\]

which maps a term $\Gamma \vdash M : A$ to a term $F\Gamma \vdash \widetilde{\varphi
}(M) : \varphi(A)$ in a similar manner.

Returning to the last condition in the definition, we may now form the diagram

\[
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node (FGA) {$\Yo{F(\CECx{\Gamma}{A})}$};
\node[pullback] (FGFA) [below right = 1cm and 2cm of FGA] {$\Yo{\CECx{F\Gamma}{\varphi(A)}}$};
\node (El) [right = 4cm of FGFA] {$\CTm{d}$};
\node (FG) [below = 2cm of FGFA] {$\Yo{F\Gamma}$};
\node (UU) [below = 2cm of El] {$\CTy{d}$};
\path[->, densely dashed] (FGA) edge (FGFA);
\path[->, bend right] (FGA) edge node[upright desc] {$\Yo{F\CWk}$} (FG);
\path[->, bend left]  (FGA) edge node[upright desc] {$\YoEm{\widetilde{\varphi}(\CVar)}$} (El);
\path[->] (FGFA) edge node [left] {$\Yo{\CWk}$} (FG);
\path[->] (FGFA) edge node [above] {$\YoEm{\CVar}$} (El);
\path[->] (FG) edge node [below] {$\YoEm{\varphi(A)}$} (UU);
\path[->] (El) edge node [right] {$\El{d}$} (UU);
\end{tikzpicture}
\]

where the outer square is the diagram composed by pasting together the context extension diagram for
$\CECx{\Gamma}{A}$ and (<ref>), followed by transposing along the natural
isomorphism (<ref>).  We then ask that the unique induced arrow be the

We can lift these natural transformations to the formation data of the connectives (making
special use of the final equality for the polynomial functors). For instance, we can define a

\[
\Mor[(\varphi, \widetilde{\varphi})]{\Poly{\El{c}}{\CTy{c}}}{\Poly{\Pre{F}{\El{d}}}{\Pre{F}{\CTy{d}}}}
\defeq
\Poly{\El{c}}{\CTy{c}}
\xrightarrow{}
\Poly{\Pre{F}{\CTy{d}}}{\CTy{c}}
\xrightarrow{\Poly{\Pre{F}{\CTy{d}}}{\varphi}}
\Poly{\Pre{F}{\El{d}}}{\Pre{F}{\CTy{d}}}
\]

The first component comes from a natural transformation $\Poly{\El{c}}{-} \Rightarrow
\Poly{\Pre{F}{\CTy{d}}}{-}$, which exists because (<ref>) not only
commutes, but is a pullback square. That is a nontrivial fact proven laboriously by <cit.>.  A more conceptual proof is given by <cit.> in the
language of discrete fibrations.

We then require that all connectives ($\CPi$, $\CSig$, $\CRefl$) strictly commute with these
morphisms. Finally, we can extend this to a model of  by requiring not just a functor, but a
natural transformation $\mathcal{C} \To \mathcal{D}$, where $\Mod{C},\Mod{D} : \Coop{\Mode} \to
\CAT$ satisfy the obvious generalizations of the conditions written above. Specifying this formally:

A morphism between two models of , $\Mod{C},\Mod{D}$, is given by a 2-natural
transformation: $F : \Mod{C} \to \Mod{D}$. Moreover, we require a choice of commuting

\[
\begin{tikzpicture}[on grid, node distance = 2.5cm]
\node (TmC) {$\ModTm{C}{m}$};
\node (TmD) [right = of TmC] {$\Pre{F_m}{\ModTm{D}{m}}$};
\node (TyC) [below = 2cm of TmC] {$\ModTy{C}{m}$};
\node (TyD) [below = 2cm of TmD] {$\Pre{F}{\ModTy{D}{m}}$};
\path[->] (TmC) edge node [left] {$\ModEl{C}{m}$} (TyC);
\path[->] (TmC) edge node [above] {$\widetilde{\varphi}_m$} (TmD);
\path[->] (TyC) edge node [below] {$\varphi_m$} (TyD);
\path[->] (TmD) edge node [right] {$\Pre{F}{\ModEl{D}{m}}$} (TyD);
\end{tikzpicture}
\]

Moreover, we require that $(\varphi,\widetilde{\varphi})$ strictly commutes with all operations.

\begin{align*}
F_m(\ECx{\Gamma}{A}) &= \ECx{F_m(\Gamma)}{\varphi(A)}&&\\
\CPi \circ (\varphi, \varphi) &= \varphi \circ \CPi & \CLam \circ (\varphi, \widetilde{\varphi}) &= \widetilde{\varphi} \circ \CLam\\
\CSig \circ (\varphi, \varphi) &= \varphi \circ \CSig & \CPair \circ (\varphi, \widetilde{\varphi}) &= \widetilde{\varphi} \circ \CPair\\
\CModify \circ \Pre{\InterpModal{\mu}}{\varphi} &= \varphi \circ \CModify & \CMkBox \circ \Pre{\InterpModal{\mu}}{\widetilde{\varphi}} &= \widetilde{\varphi} \circ \CMkBox\\
&& \COpen[\mu]^\nu \circ (\widetilde{\varphi}, \Pre{\InterpModal{\mu}}{\widetilde{\varphi}}) &= \widetilde{\varphi} \circ \COpen[\mu]^\nu\\
\CBool &= \varphi \circ \CBool & \CTrue = \widetilde{\varphi} \circ \CTrue &\quad \CFalse = \widetilde{\varphi} \circ \CFalse\\
&& \CRec \circ (\widetilde{\varphi},\widetilde{\varphi},\widetilde{\varphi}) &= \widetilde{\varphi} \circ \CRec\\
\CId \circ (\varphi,\widetilde{\varphi},\widetilde{\varphi}) &= \varphi \circ \CId & \CRefl \circ \widetilde{\varphi} &= \widetilde{\varphi} \circ \CRefl\\
&& \CIdRec \circ (\widetilde{\varphi},\widetilde{\varphi}) &= \widetilde{\varphi} \circ \CIdRec
\end{align*}

Under this definition of homomorphism, we immediately have an initial
model <cit.>. We will define this model to be our
syntax and designate it $(\SynCat{m})_{m \in \Mode}$.

§ CANONICITY

Equipped with the generalized algebraic theory of <ref> and its reformulation
through natural models in <ref>, we are ready to show that the syntax of  is
well-behaved. In this section we will sketch the main parts of a proof of canonicity for
. This is a basic well-behavedness property which guarantees that terms of ground type, e.g. $\Bool$, can be normalized. As expected, the proof is independent of the mode theory.

If $\IsTm[{}]{M}{\Bool}$, then either $\EqTm[{}]{M}{\True}{\Bool}$ or

This kind of result would traditionally be established by producing a rewriting system along with a
lengthy PER model construction. We will instead opt for a proof given by constructing a glued
model <cit.>. The contexts, types, and terms of this model will
contain a syntactic component (resp. a context, type, or term), along with a proof-relevant
predicate that is appropriately fibred over it. The base types of this model are carefully chosen
so that a normal form can be extracted from proofs of the predicate. By interpreting a term of
ground type in the glued model we automatically obtain a proof of the predicate, from which we
extract a normal form.

Such proofs involve two steps: defining the glued construction, and proving that it is a model.
While the first step is often straightforward, the second usually involves checking innumerable
equations. In order to shorten the proof sketched here we will make a simplifying assumption: we
will assume that locks preserve the empty context, i.e. that

\[
\EqCx{\LockCx{\Emp}}{\Emp}
\]

for $\mu : \Hom[\Mode]{m}{n}$. Using the universal property of the terminal context, this implies

\begin{equation}
\EqSb[\LockSb{\Emp}]{\Key{\alpha}{\Emp}}{\Emp = \ISb}{\LockSb{\Emp}<\nu>}
\label{eq:canonicity:terminal-key}
\end{equation}

Requiring this equation unfortunately limits our class of models to those where the left adjoint
strictly preserves the terminal product. Despite this simplification the proof remains rather long,
so we will only sketch the construction of the modal natural models. The missing details may be
found in an accompanying technical report.

In what follows we will assume the existence of two Grothendieck universes $\VV' \subset \VV :
\SET$. We could make do with just one but at the price of some contortions, which are both
unnecessary and tiresome. We will assume that the sets of contexts, substitutions, types, and
terms of the syntactic model are $\VV'$-small.

§.§ The Glued Model

We begin by defining the context structure.

[Glued Contexts]
A glued context $\Gamma$ at mode $m$ consists of a context $\Syn{\Gamma} \in \Cx{m}$, a predicate
$\Sem{\Gamma} \in \VV$, and a function

\[
\Pred{\Gamma} : \Sem{\Gamma} \to \Sub{m}(\Emp, \Syn{\Gamma})
\]

A glued context $\Gamma = (\Syn{\Gamma}, \Sem{\Gamma})$ can be thought of as a proof-relevant
predicate over substitutions into the syntactic context $\Syn{\Gamma}$. An element $x \in
\Sem{\Gamma}$ can be thought of as a proof that the predicate holds of the substitution
$\Pred{\Gamma}(x) : \Emp \to \Syn{\Gamma}$. We will henceforth use the metavariable $\Gamma$ to
range over glued contexts, and denote contexts of the syntax by $\Syn{\Gamma}$.

[Glued Substitutions]
A glued substitution from $\Delta$ to $\Gamma$ at mode $m$ is a pair of a substitution
$\Syn{\gamma} \in \Sub{m}(\Syn{\Delta},\Syn{\Gamma})$ and a function $\Sem{\gamma} : \Sem{\Delta}
\to \Sem{\Gamma}$ such that

\[
\forall x \in \Sem{\Delta}.\ \Pred{\Gamma}(\Sem{\gamma}(x)) = \Syn{\gamma} \circ \Pred{\Delta}(x) : \Emp \to \Syn{\Gamma}
\]

Glued contexts and glued substitutions form a category,  the comma category

\[
\InterpMode{m} \defeq \COMMA{1_{\VV}}{\Sub{m}(\Emp, -)}
\]

which we take as the category of contexts at mode $m$. Next, we define a 2-functor from $\Mode$
sending each $m$ to $\InterpMode{m}$. For each $\mu : \Hom[\Mode]{m}{n}$ a functor
$\InterpModal{\mu} : \InterpMode{n} \to \InterpMode{m}$ as by taking the $\InterpMode{n}$ morphism

\[
\begin{tikzpicture}[on grid, node distance = 2.5cm, baseline = -1.25cm]
\node (SemD) {$\Sem{\Delta}$};
\node (SynD) [below = 2cm of SemD] {$\Sub{n}(\Emp, \Syn{\Delta})$};
\node (SemG) [right = 6cm of SemD] {$\Sem{\Gamma}$};
\node (SynG) [below = 2cm of SemG] {$\Sub{n}(\Emp, \Syn{\Gamma})$};
\path[->] (SemD) edge node [above] {$\Sem{\gamma}$} (SemG);
\path[->] (SynD) edge node [below] {$\Syn{\gamma} \circ -$} (SynG);
\path[->] (SemD) edge node [upright desc] {$\Pred{\Delta}$} (SynD);
\path[->] (SemG) edge node [upright desc] {$\Pred{\Gamma}$} (SynG);
\end{tikzpicture}
\]

to the $\InterpMode{m}$ morphism:

\[
\begin{tikzpicture}[on grid, node distance = 2.5cm, baseline = -1.25cm]
\node (SemD) {$\Sem{\Delta}$};
\node (SynD) [below = 2cm of SemD] {$\Sub{m}(\Emp, \LockCx{\Syn{\Delta}})$};
\node (SemG) [right = 6cm of SemD] {$\Sem{\Gamma}$};
\node (SynG) [below = 2cm of SemG] {$\Sub{m}(\Emp, \LockCx{\Syn{\Gamma}})$};
\path[->] (SemD) edge node [above] {$\Sem{\gamma}$} (SemG);
\path[->] (SynD) edge node [below] {$\LockSb{\Syn{\gamma}} \circ -$} (SynG);
\path[->] (SemD) edge node [upright desc] {$\Pred{\LockSb{\Delta}}$} (SynD);
\path[->] (SemG) edge node [upright desc] {$\Pred{\LockSb{\Gamma}}$} (SynG);
\end{tikzpicture}
\]

where the function $\Pred{\LockSb{\Delta}}$ is defined by

\[
\Pred{\LockSb{\Delta}}(x) \defeq \LockSb{\Pred{\Delta}(x)}\ :\ \Emp \to \LockSb{\Syn{\Delta}}
\]

Notice that the equation $\LockCx{\Emp} = \Emp$ is necessary to ensure that this definition is
well-typed. The diagram commutes because locks act functorially on substitutions. It is also
functorial in $\mu$, because $\LockCx{\LockCx{\Gamma}}<\nu> = \LockCx{\Gamma}<\mu \circ \nu>$, and
$\LockCx{\Gamma}<1> = \Gamma$.

We define a 2-cell $\InterpModal{\mu} \To \InterpModal{\nu}$ for each $\alpha : \nu \To \mu$. The
component at $(\Sem{\Gamma}, \Syn{\Gamma}, \Pred{\Gamma})$ is

\[
\begin{tikzpicture}[on grid, node distance = 2.5cm]
\node (SemD) {$\Sem{\Gamma}$};
\node (SynD) [below = 2cm of SemD] {$\Sub{m}(\Emp, \LockCx{\Syn{\Gamma}})$};
\node (SemG) [right = 6cm of SemD] {$\Sem{\Gamma}$};
\node (SynG) [below = 2cm of SemG] {$\Sub{m}(\Emp, \LockCx{\Syn{\Gamma}}<\nu>)$};
\draw[double] (SemD) -- (SemG);
\path[->] (SynD) edge node [below] {$\Key{\alpha}{\Syn{\Gamma}} \circ -$} (SynG);
\path[->] (SemD) edge node [upright desc] {$\Pred{\LockCx{\Gamma}}$} (SynD);
\path[->] (SemG) edge node [upright desc] {$\Pred{\LockCx{\Gamma}<\nu>}$} (SynG);
\end{tikzpicture}
\]

This diagram commutes because of (<ref>), so it is a morphism in comma
category. Naturality follows from the numerous equations pertaining to keys and their composition.

This completes the definition of a strict 2-functor $\Coop{\Mode} \to \CAT_1$ as per
<ref>. Next, we must define the modal natural model structure for
each category of contexts.

For the rest of this section we will freely use type-theoretic notation, viewing the predicate
$\Sem{\Gamma} \to \Sub{m}(\Emp, \Syn{\Gamma})$ as a family fibred over $\Sub{m}(\Emp,
\Syn{\Gamma})$,  a map $\Sub{m}(\Emp, \Syn{\Gamma}) \to \VV$.

We will follow the convention that symbols annotated with $\Sem{(-)}$ correspond to proof-relevant
constructions—i.e. members of the predicate, or maps between predicates—whereas symbols
annotated with $\Syn{(-)}$ correspond to pieces of syntax ( terms, contexts, substitutions). In
particular, $\Sem{\gamma}$ will not necessarily refer to a fibred map between proof-relevant
predicates, but also to a generalized element of $\Sem{\Gamma}$.

In other words, when $\Sem{\gamma} \in \Sem{\Gamma}$ and $\Pred{\Gamma}(\Sem{\gamma}) =
\Syn{\gamma}\ :\ \Emp \to \Syn{\Gamma}$, we will abusively write $\Sem{\gamma} :
\Sem{\Gamma}(\Syn{\gamma})$. That is, we will view $\Sem{\gamma}$ as living in the fibre of
$\Pred{\Gamma}$ over $\Syn{\gamma}$. This amounts to considering $\Sem{\gamma}$ as a proof
that the predicate $\Sem{\Gamma}$ holds at the substitution $\Syn{\gamma}$. Observe that if
$\Sem{\gamma} : \Sem{\LockCx{\Gamma}}(\Syn{\gamma})$ then $\Syn{\gamma}$ must be of the form
$\LockSb{\Syn{\theta}}$ for some $\Syn{\theta}\ :\ \Emp \to \Syn{\Gamma}$ with $\Sem{\gamma} :
\Sem{\Gamma}(\Syn{\theta})$.

Types over $\InterpMode{m}$ are given by the presheaf

\begin{align*}
&\CTy{m}(\Gamma) \defeq \{\\
&\quad \Syn{A} \in \Ty{m}[1](\Syn{\Gamma});\\
&\quad \Sem{A} :
(\Syn{\gamma} : \Sub{m}(\Emp,\Syn{\Gamma})) \to
(\Sem{\gamma} : \Sem{\Gamma}(\Syn{\gamma})) \to
\Tm{m}(\Emp, \Sb{\Syn{A}}{\Syn{\gamma}}) \to \VV\\
\end{align*}

Extending this presheaf with some additional data gives a presheaf of terms over $\InterpMode{m}$:

\begin{align*}
&\CTm{m}(\Gamma) \defeq \{\\
&\quad \Syn{A} \in \Ty{m}[1](\Syn{\Gamma});\\
&\quad \Sem{A} :
(\Syn{\gamma} : \Sub{m}(\Emp,\Syn{\Gamma})) \to
(\Sem{\gamma} : \Sem{\Gamma}(\Syn{\gamma})) \to
\Tm{m}(\Emp, \Sb{\Syn{A}}{\Syn{\gamma}}) \to \VV\\
&\quad \Syn{M} \in \Tm{m}(\Syn{\Gamma}, \Syn{A});\\
&\quad \Sem{M} :
(\Syn{\gamma} : \Sub{m}(\Emp,\Syn{\Gamma})) \to
(\Sem{\gamma} : \Sem{\Gamma}(\Syn{\gamma})) \to
\Sem{A}(\Syn{\gamma}, \Sem{\gamma}, \Sb{\Syn{M}}{\Syn{\gamma}})\\
\end{align*}

Thus, a type over $\Gamma = (\Syn{\Gamma}, \varphi_\Gamma)$ in the glued model consists of a
type $\IsTy[\Syn{\Gamma}]{\Syn{A}}[1]$ of , along with another predicate, a family of
$\VV$-small sets, indexed over both closing substitutions $\Syn{\gamma}$ that satisfy the predicate
$\Sem{\Gamma}$ and terms of type $\Sb{\Syn{A}}{\Syn{\Gamma}}$.

A term over $\Gamma$ in the glued model adds to the above a term
$\IsTm[\Syn{\Gamma}]{\Syn{M}}{\Syn{A}}$ of that type, and a section $\Sem{M}$ of the aforementioned
predicate. This section produces a proof that the predicate holds at that term after we close it by
applying any substitution $\Syn{\gamma}$ of which the $\Sem{\Gamma}$ holds. The reindexing action of
these presheaves is defined the action of substitution on contexts, types, and terms of .

It can be shown that the projection $\El{m}(\Gamma) \defeq (\Syn{A},\Sem{A},\Syn{M},\Sem{M}) \mapsto
(\Syn{A}, \Sem{A})$ that maps terms to types by forgetting the additional data defines a
representable natural transformation in the sense of <ref>; the full
proof can be found in the technical report. With respect to the connectives, we only show the
interpret the base type $\Bool$, as per <ref>. For the formation and
introduction rules we define:

\begin{align*}
\Syn{\CBool} &= \Bool &
\Sem{\CBool} &=
\lambda \Syn{\gamma},\Sem{\gamma}, \Syn{M}.\
(\Sb{\Syn{M}}{\Syn{\gamma}} = \True) + (\Sb{\Syn{M}}{\Syn{\gamma}} = \False)\\
\Syn{\CTrue} &= \True &
\Sem{\CTrue} &= \lambda \_.\ \iota_0(\star)\\
\Syn{\CFalse} &= \False &
\Sem{\CFalse} &= \lambda \_.\ \iota_1(\star)
\end{align*}

We must now define the left lifting structure $\CRec : [\CTrue,\CFalse] \pitchfork \El{m}$. In
type-theoretic notation:

\begin{align*}
\Syn{\CRec(C, [c_0,c_1], M)} &= \BoolRec{\Syn{C}}{\Syn{c_0}}{\Syn{c_1}}{\Syn{M}}\\
\Sem{\CRec(C, [c_0,c_1], M)} &= \lambda \Syn{\gamma},\Sem{\gamma}.\ %
\begin{cases}
\Sem{c_0}(\Syn{\gamma},\Sem{\gamma}) & \text{if $\Sem{M}(\Syn{\gamma},\Sem{\gamma}) = \iota_0(\star)$}\\
\Sem{c_1}(\Syn{\gamma},\Sem{\gamma}) & \text{if $\Sem{M}(\Syn{\gamma},\Sem{\gamma}) = \iota_1(\star)$}
\end{cases}
\end{align*}

§.§ Deriving Canonicity

With the gluing model constructed, the rest of the proof is surprisingly easy and boils down to one
fact, which is immediate by inspection:

The 2-natural transformation $\pi : \InterpMode{-} \To \mathbb{S}[-]$ from the glued model to the
syntactic model which forgets the predicates extends to a morphism of models.

For any closed term $\IsTm[]{M}{A}$, there is a witness for $\Sem{\Interp{A}}(M)$.

By Theorem <ref> and initiality we must have $\pi(\Interp{M}) = M$, and
so $\Sem{\Interp{M}}$ is a witness.

If $\IsTm[\Emp]{M}{A}$ is a closed term, then

* If $A = \Bool$ then $\EqTm[\Emp]{M}{\True}{\Bool}$ or

* If $A = \Id{A_0}{N_0}{N_1}$ then $\EqTm[\Emp]{N_0}{N_1}{A_0}$ and

* If $A = \Modify[\nu]{A_0}$ then there is an $\IsTm[\Emp]{N}{A_0}<n>$ such that

Immediate by Corollary <ref> and the definition of the semantic predicates
at $\Bool$, $\Id{A_0}{N_0}{N_1}$, and $\Modify[\nu]{A_0}$ respectively.

§ DEPENDENT RIGHT ADJOINTS

Over the past couple of years the structure of a dependent right adjoint (DRA) has arisen as
a natural notion of dependent modality in Martin-Löf type theory. In this section we will study
the relationship between  modalities and DRAs in detail. After reviewing the definition of a
DRA, we will prove that a suitably functorial collection of DRAs induces a model of . As
mentioned before, this implies that  modalities are weaker than DRAs. Following that, we will
investigate sufficient conditions for extending an ordinary right adjoint to a DRA.

§.§ Dependent right adjoints in natural models

A dependent right adjoint[DRAs were introduced by <cit.> as
endomodalities, but we generalise them to multiple modes.]
is an adaptation of the notion of adjunction to the dependent setting: instead of acting
on objects of the context category, the `right adjoint' only acts on types and terms.

Given a pair of natural models $(\DD, \El{\DD})$ and  $(\CC, \El{\CC})$, a DRA from the first to the
second comprises a functor $L : \DD \to \CC$ between the underlying context categories, as well as a
pullback diagram of the following shape in $\PSH{\DD}$:

\[
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node[pullback] (ModTm) {$\Pre{L}{\CTm{\CC}}$};
\node (Tm) [right = 4cm of ModTm] {$\CTm{\DD}$};
\node (ModTy) [below = of ModTm] {$\Pre{L}{\CTy{\CC}}$};
\node (Ty) [below = of Tm] {$\CTy{\DD}$};
\path[->] (ModTm) edge node [left] {$\Pre{L}{\El{\CC}}$} (ModTy);
\path[->] (ModTm) edge node [above] {$r$} (Tm);
\path[->] (ModTy) edge node [below] {$R$} (Ty);
\path[->] (Tm) edge node [right] {$\El{\DD}$} (Ty);
\end{tikzpicture}
\]

$R$ is the action on types, and $r$ is the action on terms. Note that, while the `left adjoint' $L$
acts on context categories, the `right adjoint' $(R, r)$ only acts on types and terms. The fact the
square is a pullback amounts to requiring a multimode generalization of the definition given by
<cit.>. Intuitively, for each term $\Gamma \vdash M : R(A)$, the pullback square
gives a unique term $L(\Gamma) \vdash N : A$ such that $\Gamma \vdash M = r(N) : R(A)$. If we wish
the modality to preserve the size of types, we must also require a $R'$ such that

\[
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node (SF) {$\Pre{L}{\CSTy{\CC}}$};
\node (S) [right = 4cm of ModTm] {$\CSTy{\DD}$};
\node (TF) [below = 2cm of ModTm] {$\Pre{L}{\CTy{\CC}}$};
\node (T) [below = 2cm of S] {$\CTy{\DD}$};
\path[->] (SF) edge node [left] {} (TF);
\path[->, densely dotted] (SF) edge node [above] {$R'$} (S);
\path[->] (TF) edge node [below] {$R$} (T);
\path[->] (S) edge node [right] {$\CLift$} (T);
\end{tikzpicture}
\]

§.§ DRAs as Models of

We will now show that DRAs can be used to construct models of . As a consequence,
modalities are slightly weaker than DRAs.

Suppose that we have

* for each $m \in \Mode$ a natural model $(\InterpMode{m},
\Mor[\El{m}]{\CTm{m}}{\CTy{m}})_{m \in \Mode}$ of ;

* for each modality $\mu : \Hom[\Mode]{m}{n}$ a size-preserving DRA $(\InterpModal{\mu},
\CModify, \CMkBox)$ from $(\InterpMode{m}, \Mor[\El{m}]{\CTm{m}}{\CTy{m}})$ to
$(\InterpMode{n}, \Mor[\El{n}]{\CTm{n}}{\CTy{n}})$;

* for each 2-cell $\alpha : \mu \To \nu$ in $\Mode$ a natural transformation
$\InterpKey{\alpha} : \InterpModal{\nu} \To \InterpModal{\mu}$.

Moreover, suppose that the above choices are 2-functorial. Then this data can be assembled into a
model of , where each each mode $m$ is interpreted by $(\InterpMode{m},
\Mor[\El{m}]{\CTm{m}}{\CTy{m}})$.

Define a 2-functor $\Coop{\Mode} \to \CAT$ by $m \mapsto \InterpMode{m}$, $\mu \mapsto
\InterpModal{\mu}$, and $\alpha \mapsto \InterpKey{\alpha}$. We must show how to define context extension, and how to interpret the connectives. As before, we only show the modal cases, the others being straightforward.

Modal Context Extension
For each type $\Mor[\YoEm{A}]{\Yo{\Gamma}}{\Pre{\InterpModal{\mu}}{\CTy{n}}}$ we need a pullback

\[
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node[pullback] (Gex) {$\Yo{\Gamma'}$};
\node (Tm) [right = 3.5cm of ModTm] {$\Pre{\InterpModal{\mu}}{\CTm{n}}$};
\node (G) [below = 2cm of Gex] {$\Yo{\Gamma}$};
\node (Ty) [below = 2cm of Tm] {$\Pre{\InterpModal{\mu}}{\CTy{n}}$};
\path[->] (Gex) edge node [left] {$\Yo{p'}$} (G);
\path[->] (Gex) edge node [above] {$\YoEm{q'}$} (Tm);
\path[->] (G) edge node [below] {$\YoEm{A}$} (Ty);
\path[->] (Tm) edge node [right] {$\Pre{\InterpModal{\mu}}{\El{n}}$} (Ty);
\end{tikzpicture}
\]

Write $\YoEm{\CModify(A)} \defeq \CModify \circ \YoEm{A}$. $\El{m}$ is a natural model, so form
the pullback square for $\Gamma' \defeq \CECx{\Gamma}{\CModify(A)}$. Pasting this with the DRA
pullback for $\CModify$ forms

\begin{equation}
\begin{tikzpicture}[node distance=2.5cm, on grid, baseline=(current  bounding  box.center)]
\node[pullback] (Gex) {$\Yo{\CECx{\Gamma}{\CModify(A)}}$};
\node (G) [below = 2cm of Gex] {$\Yo{\Gamma}$};
\node[pullback] (Tm) [right = 3.5cm of ModTm] {$\Pre{\InterpModal{\mu}}{\CTm{n}}$};
\node (Ty) [below = 2cm of Tm] {$\Pre{\InterpModal{\mu}}{\CTy{n}}$};
\node (TmM) [right = 3.5cm of Tm] {$\CTm{m}$};
\node (TyM) [below = 2cm of TmM] {$\CTy{m}$};
\path[->] (Gex) edge node [left] {$\Yo{\CWk}$} (G);
\path[->] (Gex) edge[bend left] node [above] {} (TmM);
\path[densely dotted, ->] (Gex) edge node [above] {$\Transpose{\YoEm{\CVar}}$} (Tm);
\path[->] (G) edge node [below] {$\YoEm{A}$} (Ty);
\path[->] (Tm) edge node [right] {$\Pre{\InterpModal{\mu}}{\El{n}}$} (Ty);
\path[->] (Tm) edge node [above] {$\CMkBox$} (TmM);
\path[->] (Ty) edge node [below] {$\CModify$} (TyM);
\path[->] (TmM) edge node [right] {$\El{m}$} (TyM);
\end{tikzpicture}
\label{diag:dra-to-modal}
\end{equation}

As the outer square commutes, we can fill in the dotted arrow. By the pullback lemma, the square
on the left is a pullback too. Letting $\ECx{\Gamma}{A} \defeq \CECx{\Gamma}{\CModify(A)}$
proves that $\left(\El{m}\right)_{m \in \Mode}$ is a modal natural model.

Modal Types

This is the heart of the proof. First, we need a commuting square

\begin{equation}
\begin{tikzpicture}[node distance=2.5cm, on grid, baseline=(current  bounding  box.center)]
\node[pullback] (ModTm) {$\Pre{\InterpModal{\mu}}{\CTm{n}}$};
\node (Tm) [right = 4cm of ModTm] {$\CTm{m}$};
\node (ModTy) [below = 1.5cm of ModTm] {$\Pre{\InterpModal{\mu}}{\CTy{n}}$};
\node (Ty) [below = 1.5cm of Tm] {$\CTy{m}$};
\path[->] (ModTm) edge node [left] {} (ModTy);
\path[->] (ModTm) edge node [above] {$\CMkBox$} (Tm);
\path[->] (ModTy) edge node [below] {$\CModify$} (Ty);
\path[->] (Tm) edge node [right] {$\El{m}$} (Ty);
\end{tikzpicture}
\label{diag:DRA-pullback-modal}
\end{equation}

Such a square is given as part of a DRA by definition, and is in fact a pullback!

To model the elimination rule, recall the definition of the object $M$ used in <ref>:

\[
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node (ModTm) {$\Pre{\InterpModal{\mu \circ \nu}}{\CTm{o}}$};
\node[pullback] (M) [below right = 2cm and 2cm of ModTm] {$\Pre{\InterpModal{\mu}}{M}$};
\node (Tm) [right = 4cm of M] {$\Pre{\InterpModal{\mu}}{\CTm{n}}$};
\node (ModTy) [below = 2cm of M] {$\Pre{\InterpModal{\mu \circ \nu}}{\CTy{o}}$};
\node (Ty) [below = 2cm of Tm] {$\Pre{\InterpModal{\mu}}{\CTy{n}}$};
\path[->, densely dashed] (ModTm) edge node [upright desc] {$\Pre{\InterpModal{\mu}}{m}$} (M);
\path[->] (M) edge node {} (Tm);
\path[->] (M) edge  node {} (ModTy);
\path[->] (ModTm) edge[bend right] node [left] {$\Pre{\InterpModal{\mu \circ \nu}}{\El{o}}$} (ModTy);
\path[->] (ModTm) edge[bend left] node [above] {$\Pre{\InterpModal{\mu}}{\CMkBox[\nu]}$} (Tm);
\path[->] (ModTy) edge node [below] {$\Pre{\InterpModal{\mu}}{\CModify[\nu]}$} (Ty);
\path[->] (Tm) edge node [right] {$\Pre{\InterpModal{\mu}}{\El{n}}$} (Ty);
\end{tikzpicture}
\]

As $\Pre{\InterpModal{\mu}}$ preserves pullbacks, the outer square is a pullback too. Hence
$\Pre{\InterpModal{\mu}}{m}$ must be an isomorphism. The elimination rule requires a
left-lifting structure:

\[
\vdash \COpen[\nu]^\mu :
\parens*{\Pre{\InterpModal{\mu}}{m}}
\pitchfork
\Pre*{(\Pre{\InterpModal{\mu \circ \nu}}{\CTy{o}})}{\El{m}[-]}
\]

Using the inverse of $\Pre{\InterpModal{\mu}}{m}$ we can construct this by

\[
\COpen[\nu]^\mu \defeq \lambda C.\ \lambda c.\ c \circ \Pre*{\InterpModal{\mu}}{m^{-1}}
\]

$\prod$ Structure

Equipping each $\Mor[\El{m}]{\CTm{m}}{\CTy{m}}$ with a modal $\prod$ structure is relatively
straightforward to do in the internal language; intuitively, the reason is the isomorphism

\[
\ReIdx{\parens{\Pre{\InterpModal{\mu}}{\El{n}}}}{A}
\cong
\ReIdx{\El{m}}{\CModify{A}}
\]

which is derived from the fact $\ECx{\Gamma}{A} \defeq \CECx{\Gamma}{\CModify{A}}$ (where
the first dot is the defined context extension, and the second dot is given by the natural
model). However, we can also prove it in a more abstract way: we paste together the two pullback

\[
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node[pullback] (PiTm) {$\Poly{\Pre{\InterpModal{\mu}}{\El{n}}}{\CTm{m}}$};
\node (PiTy) [below = 2cm of PiTm] {$\Poly{\Pre{\InterpModal{\mu}}{\El{n}}}{\CTy{m}}$};
\node[pullback] (PiTm2) [right = 4cm of PiTm] {$\Poly{\El{m}}{\CTm{m}}$};
\node (PiTy2) [below = 2cm of PiTm2] {$\Poly{\El{m}}{\CTy{m}}$};
\node (Tm) [right = 4cm of PiTm2] {$\CTm{m}$};
\node (Ty) [below = 2cm of Tm] {$\CTy{m}$};
\path[->] (Tm) edge node[right] {$\El{m}$} (Ty);
\path[->] (PiTm) edge node[above] {$\phi_{\CTm{m}}$} (PiTm2);
\path[->] (PiTy) edge node[below] {$\phi_{\CTy{m}}$} (PiTy2);
\path[->] (PiTm) edge node[left] {$\Poly{\Pre{\InterpModal{\mu}}{\El{n}}}{\El{m}}$} (PiTy);
\path[->] (PiTm2) edge node[left] {$\Poly{\El{m}}{\El{m}}$} (PiTy2);
\path[->] (PiTm2) edge node[above] {$\CLam$} (Tm);
\path[->] (PiTy2) edge node[below] {$\CPi$} (Ty);
\end{tikzpicture}
\]

The square on the right is the pullback that interprets $\CPi$ in the natural model $\El{m}$.
The square on the left is a naturality square of the natural transformation

\[
\phi :
\Poly{\Pre{\InterpModal{\mu}}{\El{n}}}{-}
\Rightarrow
\Poly{\El{m}}{-}
\]

which exists because the pullback square (<ref>) defines a morphism of
polynomials. Moreover, the naturality squares of $\phi$ are cartesian: see <cit.>.

This theorem is a particularly flexible tool, as many modalities naturally form DRAs, and it is
easier to check the DRA conditions than  model conditions as summarized in Definition
<ref>. As a first example of this flexibility we show that it leads to an
almost immediate proof of consistency.

No matter what the mode theory is, there is no term $\IsTm[\Emp]{M}{\Id{\Bool}{\True}{\False}}$.
In other words,  is consistent.

Suppose that we have a model of  with one universe in some category $\CC$. We may construct
a functor $\Coop{\Mode} \to \CAT$ by sending every mode to $\CC$, and everything else to the
identity. This is stricty 2-functorial, and each identity functor is a DRA. Hence, by
Theorem <ref> there is a model of  in which each mode is interpreted by
$\CC$. Therefore, if a term $M : \Id{\Bool}{\True}{\False}$ were definable in , we would
have a term of that type in every model of . But  itself is consistent: see
<cit.> for a short proof.

§.§ DRAs from right adjoints

Having established that a series of models of  related by DRAs can be used to interpret
, we now turn to the problem of constructing those DRAs themselves. We shall prove a lemma
that allows us to lift any well-behaved right adjoint to a DRA. Versions of this result have
appeared before, both in the paper on DRAs <cit.>, and in a technical
report by the third author <cit.>.

In <ref> we discussed the notion of a strict morphism of natural
models. Using the same notation we define the following weaker notion.

A weak morphism of natural models $(\CC, \CTy{c}) \to (\DD, \CTy{d})$ consists of a functor
$F : \CC \to \DD$, and a commuting square

\[
\begin{tikzpicture}[on grid, node distance = 2.5cm]
\node (TmC) {$\CTm{c}$};
\node (TmD) [right = of TmC] {$\Pre{F}{\CTm{d}}$};
\node (TyC) [below = 2cm of TmC] {$\CTy{c}$};
\node (TyD) [below = 2cm of TmD] {$\Pre{F}{\CTy{d}}$};
\path[->] (TmC) edge node [left] {$\El{c}$} (TyC);
\path[->] (TmC) edge node [above] {$\widetilde{\varphi}$} (TmD);
\path[->] (TyC) edge node [below] {$\varphi$} (TyD);
\path[->] (TmD) edge node [right] {$\Pre{F}{\El{d}}$} (TyD);
\end{tikzpicture}
\]

such that $F(1) = 1$ and the canonical morphism $F(\CECx{\Gamma}{A}) \to
\CECx{F\Gamma}{\varphi(A)}$ is an isomorphism. We say that this morphism preserves size
whenever there is a commuting square

\[
\begin{tikzpicture}[on grid, node distance = 2.5cm]
\node (STyC) {$\CSTy{c}$};
\node (STyD) [right = of STyC] {$\Pre{F}{\CSTy{d}}$};
\node (TyC) [below = 2cm of STyC] {$\CTy{c}$};
\node (TyD) [below = 2cm of STyD] {$\Pre{F}{\CTy{d}}$};
\path[->] (STyC) edge node [left] {$\CLift$} (TyC);
\path[->] (STyC) edge node [above] {$\CSTy{\varphi}$} (STyD);
\path[->] (TyC) edge node [below] {$\varphi$} (TyD);
\path[->] (STyD) edge node [right] {$\Pre{F}{\CLift}$} (TyD);
\end{tikzpicture}
\]

This kind of morphism can also be found in the thesis of <cit.>. We are
interested in it because it captures exactly the necessary good behaviour which is required to
extend a right adjoint to act on types and terms.

Suppose that $(\CC, \El{\CC})$ and $(\DD, \El{\DD})$ are natural models, and that $L \Adjoint R$
is an adjunction between $\CC$ and $\DD$. If the right adjoint $R : \CC \to \DD$ extends to a weak
morphism of natural models then it gives rise to a dependent right adjoint. Moreover, the
resulting DRA is size-preserving whenever $R$ is.

We first fix some notation: we write $\eta : \textsf{Id} \Rightarrow RL$ for the unit of the
adjunction $L \Adjoint R$. Moreover, we assume a commuting square

\begin{equation}
\begin{tikzpicture}[on grid, node distance = 2.5cm, baseline=(current  bounding  box.center)]
\node (TmC) {$\CTm{\CC}$};
\node (TmD) [right = of TmC] {$\Pre{R}{\CTm{\DD}}$};
\node (TyC) [below = 2cm of TmC] {$\CTy{\CC}$};
\node (TyD) [below = 2cm of TmD] {$\Pre{R}{\CTy{\DD}}$};
\path[->] (TmC) edge node [left] {$\El{\CC}$} (TyC);
\path[->] (TmC) edge node [above] {$\textsf{r}$} (TmD);
\path[->] (TyC) edge node [below] {$\textsf{R}$} (TyD);
\path[->] (TmD) edge node [right] {$\Pre{R}{\El{\DD}}$} (TyD);
\end{tikzpicture}
\label{diag:constructing-dra:lifting-adjunction:weakcwf}
\end{equation}

that witnesses the weak natural model morphism structure of $R$, and write

\[
\nu_{\Gamma, A} :
\CECx{R\Gamma}{\textsf{R}(A)}
\xrightarrow{\cong}
\]

for the canonical isomorphism corresponding to $\YoEm{A} : \Yo{\Gamma} \Rightarrow \CTy{\CC}$.  We
then define the square

\[
\begin{tikzpicture}[node distance=2.5cm, on grid]
\node (ModTm) {$\Pre{L}{\CTm{\CC}}$};
\node (ModTy) [below = 2cm of ModTm] {$\Pre{L}{\CTy{\CC}}$};
\node (LRTm) [right = 2.5cm of ModTm] {$\Pre{L}\Pre{R}{\CTm{\DD}}$};
\node (LRTy) [below = 2cm of LRTm] {$\Pre{L}\Pre{R}{\CTy{\DD}}$};
\node (Tm) [right = 2.5cm of LRTm] {$\CTm{\DD}$};
\node (Ty) [below = 2cm of Tm] {$\CTy{\DD}$};
\path[->] (ModTm) edge node [left] {$\Pre{L}{\El{\CC}}$} (ModTy);
\path[->] (ModTm) edge node [above] {$\Pre{L}{\textsf{r}}$} (LRTm);
\path[->] (ModTy) edge node [below] {$\Pre{L}{\textsf{R}}$} (LRTy);
\path[->] (Tm) edge node [right] {$\El{\DD}$} (Ty);
\path[->] (LRTm) edge node [upright desc] {$\Pre{L}\Pre{R}{\El{\DD}}$} (LRTy);
\path[->] (LRTm) edge node [above] {$\Pre{\eta}{}_{\CTm{\DD}}$} (Tm);
\path[->] (LRTy) edge node [below] {$\Pre{\eta}{}_{\CTy{\DD}}$} (Ty);
\end{tikzpicture}
\]

The left part of the square is the image of
(<ref>) under the $\Pre{L}$ functor, and the
right part is a naturality square for the natural transformation $\Pre{\eta} : \Pre{L}\Pre{R} =
\Pre{(RL)} \Rightarrow \textsf{Id}$ induced by the unit of the adjunction.

We must show that this defines a pullback, and it suffices to do so on the representables.  Assume
we have $\YoEm{A} : \Yo{\Delta} \Rightarrow \Pre{L}\CTy{\CC}$ and a $\YoEm{M} : \Yo{\Delta}
\Rightarrow \CTy{\DD}$ such that the diagram commutes. Switching to type-theoretic notation, this
amounts to a type $L(\Delta) \vdash A\ \mathsf{type}$—which gives rise to a type $R(L(\Delta))
\vdash \textsf{R}(A)\ \mathsf{type}$ by applying $\textsf{R}$—and a term $\Delta \vdash M :
\Sb{\textsf{R}(A)}{\eta_\Delta}$. The universal property of the pullback dictates that we must
show the existence of a unique term $L(\Delta) \vdash N : A$ such that

\begin{equation}
RL(\Delta) \vdash
\Sb{\textsf{r}(N)}{\eta_\Delta}
M : \Sb{\textsf{R}(A)}{\eta_\Delta}
\label{eq:constructing-dra:lifting-adjunction:weakcwf}
\end{equation}

First, observe that we can form the substitution $\ESb{\eta_\Delta}{M} : \Delta \to
\CECx{RL\Delta}{\textsf{R}(A)}$. We can then postcompose the isomorphism $\nu_{\Delta, A}$ to
obtain a morphism of type $\Delta \to R(\CECx{L\Delta}{A})$. To this we can apply $L$ and
postcompose the counit $\epsilon_{\CECx{L\Delta}{A}}$ to obtain a substitution

\[
k \defeq \epsilon_{\CECx{L\Delta}{A}} \circ L(\nu_{\Delta, A} \circ \ESb{\eta_\Delta}{M})
: L\Delta \to \CECx{L\Delta}{A}
\]

Using naturality of the counit and the equations satisfied by the canonical isomorphism
$\nu_{\Delta, A}$, it is easy to show that $\CWk \circ k = \ISb : L\Delta \to L\Delta$, and hence
that we can extract a term

\[
L(\Delta) \vdash N \defeq \Sb{\CVar}{k} : A
\]

Using naturality of $\textsf{r}(-)$, naturality of the unit, and one of the triangle identities,
we can calculate that this term satisfies equation
(<ref>). Finally, we can prove this choice is
unique by calculating that any such $N$ necessarily satisfies $k = \CECx{\ISb}{N}$, and hence that
$\Sb{\CVar}{k} = N$.

It is routine to show that this is size-preserving, using the fact that $\textsf{R}$ preserves

The converse is not in general true: a dependent right adjoint need not extend to a functor on the
category of contexts. Nevertheless, it does whenever the category of contexts is democratic
<cit.>, i.e. if every context is isomorphic to extending the empty context by
some type: see <cit.> for a proof.

§ PRESHEAF MODELS

It is well-known that the category $\PSH{C}$ of presheaves over any small category $\CC$ is a model
of Martin-Löf type theory. A functor $\mu : \CC \to \DD$ induces by precomposition a

\[
\Pre{\mu} : \PSH{\DD} \to \PSH{\CC}
\]

between categories of presheaves. This functor has a right adjoint

\[
\RKan{\mu} : \PSH{\CC} \to \PSH{\DD}
\]

given by right Kan extension <cit.> <cit.> <cit.>. We show that an appropriately functorial version of this structure can be
bootstrapped into a model of , where the modalities are right adjoints to this precomposition
functor. More concretely, starting with a small 2-category $\II$, and a functor

\[
J : \II \to \CAT
\]

we will construct a model of  where each mode corresponds to the category $\PSH{J(i)}$, and the modalities are the functors $\RKan{J(f)}$, for each $f \in \Hom[\II]{i_0}{i_1}$.

Context structure. We define a strict 2-functor $\Interp{-} : \Coop{\II} \to \CAT$ by

i                      ⟼i J(i)

f : i →j            ⟼f J(f) : J(j) →J(i)

α: f g       ⟼α J(α) : J(g) J(f)

The variance is correct: recall that precomposition is a strict 2-functor

\[
\Pre{(-)} : \Coop{\CAT} \to \CAT
\]

which maps a functor $f : \CC \to \DD$ to $\Pre{f} : \PSH{\DD} \to \PSH{\CC}$, and a natural
transformation $\alpha : f \To g$ to $\Pre{\alpha} : \Pre{g} \To \Pre{f}$, given by
$\Pre{\alpha}_{P, c} \defeq P(\alpha_c) : P(g(c)) \to P(f(c))$. 2-functoriality is immediate, as for
example $\Pre{J(f)} \circ \Pre{J(g)} = \Pre{(J(g) \circ J(f))} = \Pre{J(g \circ f)}$.

Modal natural models.

To interpret the `mode-local' structure we must construct a modal natural model in each
$\InterpMode{i}$. It is well-known that every presheaf topos $\PSH{\CC}$ gives rise to a rich model
of : see e.g. <cit.> or <cit.>.

Contexts are interpreted as objects of the presheaf category $\PSH{\CC}$. Types are
presheaves $\PSH{\EL{\Gamma}}$ over the category of elements $\EL{\Gamma}$ of a context $\Gamma :
\PSH{\CC}$.[There is an equivalence $\PSH{\EL{\Gamma}} \Equiv \SLICE{\PSH{\CC}}{\Gamma}$
which shows that types are families $P \To \Gamma$ in the slice category. However, using the latter
definition would lead to strictness issues.] We define the action of a substitution $\sigma : \Delta
\To \Gamma$ on a type $A : \PSH{\EL{\Gamma}}$ by

\[
A\brackets{\sigma} \defeq
\Op{(\EL{\Delta})} \xrightarrow{\Op{(\EL{\sigma})}} \Op{(\EL{\Gamma})} \xrightarrow{A} \SET
\]

This is functorial because $\EL{-} : \PSH{\CC} \to \CAT$ and $\Op{-} : \CAT \to \CAT$ are.

A term of type $A$ is a global section of $A$, i.e. a morphism
$\Hom[\PSH{\EL{\Gamma}}]{1}{A}$. We define the action of a substitution $\sigma : \Delta \To \Gamma$
on a term $M : \Hom{1}{A}$ by whiskering:

\[
M\brackets{\sigma} \defeq
M \ast \Op{(\EL{\sigma})} :
1 \circ \Op{(\EL{\sigma})} \To A \circ \Op{(\EL{\sigma})} = A\brackets{\sigma}
\]

As $1 \circ \Op{\EL{\sigma}} = 1$, this has the right type. It is functorial because whiskering is.

One cannot be too careful with size issues when considering presheaf models. In
<ref> we demanded that the category of contexts be small,
so that we can then formulate a large category of models. $\PSH{\CC}$ is certainly not small. We
can mend this by assuming a Grothendieck universe $\VV$ large enough to contain $\CC$ in the
ambient set theory, and re-defining $\PSH{\CC}$ to consist of the presheaves
$P : \Op{\CC} \to \VV$ with small fibers. As $\VV$ is closed under all set-theoretic
operations, this is still a model, and $\PSH{\CC}$ is small.

To interpret universes we need to know that the fibers of types in $\PSH{\EL{\CC}}$ are even
smaller. Thus, we further assume a second, inner Grothendieck universe $\VV' \subset \VV$.
To a type theorist, this is just the standard technique of `bumping' a universe level.

Presheaf models support dependent sums and products, and extensional identity types (and therefore
intensional identity types): see <cit.>. On the premise that the underlying set
theory has a set-theoretic universe, they also support a universe, through a construction of
<cit.>. See also <cit.>.

It remains to show that each $\InterpModal{f} \defeq \Pre{J(f)} : \PSH{J(j)} \to \PSH{J(i)}$ has a
corresponding modality acting on terms and types. We will do so by using previous results. By
Theorem <ref>, it suffices to construct a dependent right adjoint to
$\Pre{J(f)}$. But recall that each lock functor $\Pre{J(f)}$ already has an (ordinary) right
adjoint, viz. $\RKan{J(f)}$. Thus, by Lemma <ref> it will
suffice to show that the action of this right adjoint extends to types and terms. We then have DRAs,
and hence a model of $\MTT{}$.

The following result has previously been shown in a tech report by the third author <cit.>. We reproduce it here for the sake of completeness.

The right adjoint to precomposition $\RKan{\mu} : \PSH{\CC} \to \PSH{\DD}$ induces a DRA for any
$\mu : \CC \to \DD$. Moreover, $\RKan{\mu}$ is size-preserving for any Grothendieck universe.

We use Lemma <ref> once more. The action of $\RKan{\mu}$ on types and terms is given by

\begin{align*}
\RKan{\mu}{A} \in \PSH{\EL{\RKan{\mu}{\Gamma}}} &=
(D \in \DD, a \in \RKan{\mu}{\Gamma}(D)) \mapsto \Hom[\PSH{\EL{\Pre*{\mu}{\Yo{D}}}}]{1}{A\brackets*{\Transpose{\YoEm{a}}}}\\
\RKan{\mu}{M} \in \Hom{1}{\RKan{\mu}{A}} &= (D \in \DD, a \in \RKan{\mu}{\Gamma}(D)) \mapsto \Pre{(\EL{\Transpose{\YoEm{a}}})}{M}
\end{align*}

Both of these actions are well-typed. For types, as $a \in \RKan{\mu}{\Gamma}(D)$ we have
$\YoEm{a} : \Yo{D} \To \RKan{\mu}{\Gamma}$, so by transposition $\Transpose{\YoEm{a}} :
\Pre*{\mu}{\Yo{D}} \To \Gamma$. For terms, notice that $\EL{\Transpose{\YoEm{a}}} :
\EL{\Pre*{\mu}{\Yo{D}}} \to \EL{\Gamma}$, recall that $A\brackets*{\sigma} \defeq A \circ
\EL{\sigma}$, and that precomposition preserves the terminal object on-the-nose.

The presheaf action.
The action of $\RKan{\mu}{A}$ is subtle: it is given by the functor

\[
\Pre{(\EL{\Pre{\mu}{\Yo{f}}})} :
\PSH{\EL{\Pre{\mu}{\Yo{D}}}} \to \PSH{(\EL{\Pre{\mu}{\Yo{D'}}}}
\]

for each $f : \Hom[\DD]{D'}{D}$. In more detail, given $f : \Hom[\DD]{D'}{D}$, $a \in
\RKan{\mu}{\Gamma}(D)$, $A \in \PSH{\EL{\Gamma}}$, and $x \in \RKan{\mu}{A}(D, a) \defeq
\Hom{1}{A\brackets*{\Transpose{\YoEm{a}}}}$, we define $x \cdot f \in \RKan{\mu}{A}(D', a \cdot
f)$ by

\[
x \cdot f \defeq \Pre*{(\EL{\Pre{\mu}{\Yo{f}}})}{x}
: \Hom[\PSH{\EL{\Pre*{\mu}{\Yo{D'}}}}]
{\Pre*{(\EL{\Pre{\mu}{\Yo{f}}})}{A\brackets*{\Transpose {\YoEm{a}}}}}
\]

This is of the right type; reindexing preserves the terminal,
$\Pre{(\EL{\Pre{\mu}{\Yo{f}}})}{1} = 1$. Moreover,

\[
\Transpose{\YoEm{a}} \circ \Pre{\mu}{\Yo{f}}
= \Transpose{\YoEm{a} \circ \Yo{f}}
= \Transpose{\YoEm{a \cdot f}}
\]

by naturality of the adjunction and of Yoneda. Using this calculation, we see that

\[
\Pre*{(\EL{\Pre{\mu}{\Yo{f}}})}{A\brackets*{\Transpose {\YoEm{a}}}}
\defeq A \circ \EL{\Transpose {\YoEm{a}}} \circ \EL{\Pre{\mu}{\Yo{f}}}
= A \circ \EL{\Transpose{\YoEm{a \cdot f}}}
\defeq A\brackets*{\Transpose{\YoEm{a \cdot f}}}
\]

Hence $x \cdot f \in \RKan{\mu}{A}(D', a \cdot f)$. This assignment is functorial because
$\EL{-}$, $\Pre{(-)}$ and $\Yo{-}$ are.

We must show that both of these definitions are natural with respect to substitution, i.e. that
$(\RKan{\mu}{A})\brackets*{\RKan{\mu}{\gamma}} = \RKan*{\mu}{A\brackets*{\gamma}}$, and similarly
for terms.

For types, suppose we are given $\gamma : \Delta \to \Gamma$ and $A \in \PSH{\EL{\Gamma}}$.
Carefully unfolding both sides of the desired equation, for any $D \in \DD$ and $a \in
\RKan{\mu}\Delta(D)$ we must show that

\[
\Hom[\PSH{\EL{\Pre{\mu}{\Yo{D}}}}]{1}{A\brackets*{\Transpose{\YoEm{\RKan{\mu}\gamma_D(a)}}}}
\Hom[\PSH{\EL{\Pre{\mu}{\Yo{D}}}}]{1}{A\brackets{\gamma}\brackets*{\Transpose{\YoEm{a}}}}
\]

But, by naturality of both the adjunction and Yoneda:

\[
\gamma \circ \Transpose{\YoEm{a}}
= \Transpose{\RKan{\mu}\gamma \circ \YoEm{a}}
= \Transpose{\YoEm{\RKan{\mu}\gamma_D(a)}}
\]

Hence the two sets are the same. The calculation for terms is of a similar ilk.

Preservation of context extension.
We would like to show that the canonical morphism

\[
\Mor[\angles{\RKan{\mu}{\CWk}, \RKan{\mu}{\CVar}}]{\RKan*{\mu}{\CECx{\Gamma}{A}}}{\CECx{\RKan{\mu}{\Gamma}}{\RKan{\mu}{A}}}
\]

is invertible. Consider an element $e : \Yo{D} \To \RKan*{\mu}{\CECx{\Gamma}{A}}$. We can
transpose along the adjunction $\Pre{\mu} \dashv \RKan{\mu}$ and decompose it to obtain a
substitution and a term

\begin{align*}
e_0 &: \Pre{\mu}{\Yo{D}} \To \Gamma
e_1 &: \Hom[\PSH{\EL{\Pre{\mu}{\Yo{D}}}}]{1}{A\brackets*{e_0}}
\end{align*}

We can thus write $e = \Transpose{\angles{e_0, e_1}}$. Thus, we can use naturality of the
adjunction and of substitution to compute the action of $\angles{\RKan{\mu}{\CWk},
\RKan{\mu}{\CVar}}$ on this $e$:

\[
\angles{\RKan{\mu}{\CWk}, \RKan{\mu}{\CVar}} \circ e
= \angles{\RKan{\mu}{\CWk} \circ e, (\RKan{\mu}{\CVar})\brackets*{e}}\\
= \angles{\Transpose{\CWk \circ \angles{e_0,e_1}}, \CVar\brackets{\angles{e_0,e_1}}}\\
= \angles{\Transpose{e}_0, e_1}
\]

We can then specify an inverse on generalized elements by $\angles{\gamma, M} \mapsto
\Transpose{\angles{\Transpose{\gamma}, M}}$.

Size preservation is immediate: if $A$ is small then so are its reindexings and the collections of
points at each slice.

§.§ The other adjunction

We have so far concentrated on the adjunction $\Pre{\mu} \dashv \RKan{\mu}$ that arises through right Kan extension. Nevertheless, precomposition also has a left adjoint $\LKan{\mu}$ arising from left Kan extension. Might we also be able to interpret the lock functors by this left adjoint $\LKan{\mu}$, and lift precomposition $\Pre{\mu}$ to a modality instead?

It is in fact relatively easy to show that $\Pre{\mu}$ extends to a dependent right adjoint, the
left Kan extensions $\LKan{\mu}$ cannot be assembled into a modal context structure. The reason is
that context structures are strict 2-functors, but left Kan extensions do not compose strictly: we
only have an isomorphism $\LKan{F} \circ \LKan{G} \cong \LKan{(G \circ F)}$. We have proven a
strictification theorem that straightens these issues, but that is beyond the scope of this paper.

§ GUARDED RECURSION

We now show how  can be applied to a well-known modal situation: guarded recursion. By
instantiating  with a carefully chosen mode theory and axiomitizing certain operations
specific to guarded recursion ( Löb induction), we obtain a calculus for guarded recursion
simpler than prior hand-crafted calculi. We demonstrate the practicality of this guarded variant of
by reproducing some examples from prior work on guarded recursion <cit.>.

The key idea of guarded recursion <cit.> is to use a modality $\Later$, usually called
later, to mark the types of data that may be used only if some `computational progress' (e.g.
a tick of a clock) has taken place, thereby enforcing productivity at the level of types. The later
modality is usually equipped with three basic operations:

: A →A () : (A →B) →A →B : (A →A) →A

The first two make $\Later$ into an applicative functor <cit.>. The third,
which is commonly known as Löb induction, is a guarded fixed point operator
<cit.>: it enables us to make definitions by provably productive recursion.

$\Later$ also applies to the universe, so one can define data types by guarded recursion. The