# Transpension: The Right Adjoint to the Pi-type

Andreas Nuyts  *KU Leuven, Belgium anuyts.github.io and  Dominique
Devriese$\circ$ $\circ$Vrije Universiteit Brussel, Belgium
<EMAIL_ADDRESS>
###### Abstract.

Presheaf models of dependent type theory have been successfully applied to
model HoTT, parametricity, and directed, guarded and nominal type theory.
There has been considerable interest in internalizing aspects of these
presheaf models, either to make the resulting language more expressive, or in
order to carry out further reasoning internally, allowing greater abstraction
and sometimes automated verification. While the constructions of presheaf
models largely follow a common pattern, approaches towards internalization do
not. Throughout the literature, various internal presheaf operators
($\mathbin{\surd}$, $\Phi/\mathsf{extent}$, $\Psi/\mathsf{Gel}$,
$\mathsf{Glue}$, $\mathsf{Weld}$, $\mathsf{mill}$, the strictness axiom and
locally fresh names) can be found and little is known about their relative
expressivenes. Moreover, some of these require that variables whose type is a
shape (representable presheaf, e.g. an interval) be used affinely.

We propose a novel type former, the transpension type, which is right adjoint
to universal quantification over a shape. Its structure resembles a dependent
version of the suspension type in HoTT. We give general typing rules and a
presheaf semantics in terms of base category functors dubbed multipliers.
Structural rules for shape variables and certain aspects of the transpension
type depend on characteristics of the multiplier. We demonstrate how the
transpension type and the strictness axiom can be combined to implement all
and improve some of the aforementioned internalization operators (without
formal claim in the case of locally fresh names).

###### Key words and phrases:

dependent type theory, presheaf models, modal type theory, homotopy type
theory, parametricity, directed type theory, guarded type theory

*Holds a PhD Fellowship from the Research Foundation - Flanders (FWO)

##  1\. Introduction and Related Work

###  1.1. The Power of Presheaves

Presheaf semantics [Hof97, HS97] are an excellent tool for modelling
relational preservation properties of (dependent) type theory. They have been
applied to parametricity (which is about preservation of relations) [AGJ14,
BCM15, ND18a, NVD17], univalent type theory (preservation of equivalences)
[BCH14, CMS20, CCHM17, Hub16, KLV12, Ort18, OP18], directed type theory
(preservation of morphisms), guarded type theory (preservation of the stage of
advancement of computation) [BM18] and even combinations thereof [BBC+19,
CH20, RS17, WL20].111We omit models that are not explicitly structured as
presheaf models [AHH18, LH11, Nor19]. The presheaf models cited almost all
follow a common pattern: First one chooses a suitable base category
${\mathcal{W}}$. The presheaf category over ${\mathcal{W}}$ is automatically a
model of dependent type theory with important basic type formers [Hof97] as
well as a tower of universes [HS97]. Next, one identifies a suitable notion of
fibrancy and replaces or supplements the existing type judgement $\Gamma\vdash
T\,\mathsf{type}$ with one that classifies fibrant types:

HoTT:

For homotopy type theory (HoTT, [Uni13]), one considers Kan fibrant types,
i.e. presheaves in which edges can be composed and inverted as in an
$\infty$-groupoid. The precise definition may differ in different treatments.

Parametricity:

For parametric type theory, one considers discrete types [AGJ14, CH20, ND18a,
NVD17]: essentially those that satisfy Reynolds’ identity extension property
[Rey83] which states that homogeneously related objects are equal.

Directed:

In directed type theory, one may want to consider Segal, covariant, discrete
and Rezk types [RS17] and possibly also Conduché types [Gir64, Nuy18b][Nuy20a,
ex. 8.1.27].

Guarded:

In guarded type theory, one considers clock-irrelevant types [BM18]: types $A$
such that any non-dependent function ${\text{\clock}}\to A$ from the clock
type, is constant.

Nominal:

Nominal type theory [Che12, PMD15] can be modelled in the Schanuel topos
[Pit14].

To the extent possible, one subsequently proves that the relevant notions of
fibrancy are closed under basic type formers, so that we can restrict to
fibrant types and still carry out most of the familiar type-theoretic
reasoning and programming. Special care is required for the universe: it is
generally straightforward to adapt the standard Hofmann-Streicher universe to
classify only fibrant types, but the universe of fibrant types is in general
not automatically fibrant itself. In earlier work on parametricity with
Vezzosi [NVD17, ND18a], we made the universe discrete by modifying its
presheaf structure and introduced a parametric modality in order to use that
universe. In contrast, Atkey et al. [AGJ14] and Cavallo and Harper [CH20]
simply accept that their universes of discrete types are not discrete. In
guarded type theory, Bizjak et al. [BGC+16] let the universe depend on a
collection of in-scope clock variables lest the clock-indexed later modality
$\rhd:\forall(\kappa:{\text{\clock}}).\mathsf{U}_{\Delta}\to\mathsf{U}_{\Delta}$
(where $\kappa\in\Delta$) be non-dependent and therefore constant (not clock-
indexed) by clock-irrelevance of $\mathsf{U}_{\Delta}\to\mathsf{U}_{\Delta}$
[BM18].

###  1.2. Internalizing the Power of Presheaves

Purely metatheoretic results about type theory certainly have their value.
Parametricity, for instance, has originated and proven its value as a
metatheoretic technique for reasoning about programs. However, with dependent
type theory being not only a programming language but also a logic, it is
preferrable to formulate results about it within the type system, rather than
outside it. We highlight two particular motivations for doing so: to enlarge
the end user’s toolbox, and to be able to prove internally that a type is
fibrant.

#### Enlarging the end user’s toolbox

One motivation for internalizing metatheorems is to enlarge the toolbox of the
end user of the proof assistant. If this is the only goal, then we can prove
the desired results in the model on pen and paper and then internalize them ad
hoc with an axiom with or without computation rules.

HoTT:

Book HoTT [Uni13] simply postulates the univalence axiom without computational
behaviour, as justified e.g. by the model of Kan-fibrant simplicial sets
[KLV12].

CCHM cubical type theory [CCHM17] provides the $\mathsf{Glue}$ type, which
comes with introduction, elimination, $\beta$\- and $\eta$-rules and which
turns the univalence axiom into a theorem with computational behaviour. It
also contains CCHM-Kan-fibrancy of all types as an axiom, in the form of the
CCHM-Kan composition operator, with decreed computational behaviour that is
defined by induction on the type.

Parametricity:

Bernardy, Coquand and Moulin [BCM15, Mou16] (henceforth: Moulin et al.)
internalize their (unary, but generalizable to $k$-ary) cubical set model of
parametricity using two combinators $\Phi$ and $\Psi$ [Mou16], a.k.a.
$\mathsf{extent}$ and $\mathsf{Gel}$ [CH20]. $\Phi$ internalizes the presheaf
structure of the function type, and $\Psi$ that of the universe.

The combinator $\Phi$ and at first sight also $\Psi$ require that the cubical
set model lacks diagonals. Indeed, to construct a value over the primitive
interval, $\Phi$ and $\Psi$ each take one argument for every endpoint and one
argument for the edge as a whole. Nested use of these combinators, e.g. to
create a square, will take $(k+1)^{2}$ arguments for $k^{2}$ vertices, $2k$
sides and $1$ square as a whole but none for specifying the diagonal. For this
reason, Moulin et al.’s type system enforces a form of _affine_ use of
interval variables.

In earlier work with Vezzosi [NVD17], we have internalized parametricity
instead using the $\mathsf{Glue}$ type [CCHM17] and its dual $\mathsf{Weld}$.
Later on, we added a primitive $\mathsf{mill}$ [ND18b] for swapping
$\mathsf{Weld}$ and $\Pi(i:{\mathbb{I}})$. These operations are sound in
presheaves over any base category where we can multiply with ${\mathbb{I}}$,
and therefore strictly less expressive than $\Phi$ which is not. Discreteness
of all types was internalized as a non-computing _path degeneracy_ axiom.

Directed:

Weaver and Licata [WL20] use a bicubical set model to show that directed HoTT
[RS17] can be soundly extended with a directed univalence _axiom_.

Guarded:

In guarded type theory [BM18], one axiomatizes Löb induction and clock-
irrelevance.

Nominal:

One version of nominal type theory [PMD15] provides the locally fresh name
abstraction $\nu(i:{\mathbb{I}})$ which introduces a name but requires a body
that is fresh for the name (i.e. we do not get to use it) and which can be
used anywhere (i.e. the goal type remains the same after we abstract over a
fresh name). This would be rather useless, were it not that we are allowed to
_capture_ the fresh name (see section 8). Bridging the formal gap between the
syntactic phenomenon of name capture and the denotational presheaf semantics
is beyond the scope of this paper, which is why we make no formal claims
regarding nominal type theory but instead demonstrate the relevance of the
transpension type by example (section 8).

#### Internalizing fibrancy proofs

Another motivation to internalize aspects of presheaf categories, is for
building parts of the model inside the type theory, thus abstracting away
certain categorical details such as the very definition of presheaves, and for
some type systems enabling automatic verification of proofs. Given the common
pattern in models described in the previous section, it is particularly
attractive to try and define fibrancy and prove results about it internally.

In the context of HoTT, Orton and Pitts [Ort18, OP18] study CCHM-Kan-fibrancy
[CCHM17] in a type theory extended with a set of axioms, of which all but one
serve to characterize the interval and the notion of cofibration. One axiom,
_strictness_ , provides a type former $\mathsf{Strict}$ for strictifying
partial isomorphisms, which exists in every presheaf category. In order to
prove fibrancy of the universe, Licata et al. postulate an “amazing right
adjoint” ${\mathbb{I}}\mathbin{\surd}{\llcorner\lrcorner}$ to the non-
dependent path functor ${\mathbb{I}}\to{\llcorner\lrcorner}$ [LOPS18, Ort18],
which indeed exists in presheaves over cartesian base categories if
${\mathbb{I}}$ is representable. Since
${\mathbb{I}}\mathbin{\surd}{\llcorner\lrcorner}$ and its related axioms are
global operations (only applicable to closed terms, unless you want to open
Pandora’s box as we do in the current paper), they keep everything sound by
introducing a judgemental comonadic _global_ modality $\flat$.

Orton et al.’s formalization [LOPS18, Ort18, OP18] is only what we call _meta-
internal_ : the argument is internalized to _some_ type theory which still
only serves as a metatheory of the type system of interest. Ideally, we would
define and prove fibrancy of types _within_ the type theory of interest, which
we call _auto-internal_. Such treatments exist of discrete types in
parametricity [CH20], and discrete, fibrewise-Segal and Rezk types in directed
type theory [RS17], but not yet for covariant, Segal or Kan fibrant types due
to the need to consider paths in the context ${\mathbb{I}}\to\Gamma$.

###  1.3. The Transpension Type

What is striking about the previous section is that, while most authors have
been able to solve their own problems, a common approach is completely absent.
We have encountered $\Phi$ and $\Psi$ [Mou16], the amazing right adjoint
$\mathbin{\surd}$ [LOPS18], $\mathsf{Glue}$ [CCHM17, NVD17], $\mathsf{Weld}$
[NVD17], $\mathsf{mill}$ [ND18b] and the strictness axiom [OP18]. We have also
seen that $\Phi$ and $\Psi$ presently require an affine base category, and
that $\mathbin{\surd}$ presently requires the global modality $\flat$.

The goal of the current paper is to develop a smaller collection of internal
primitives that impose few restrictions on the choice of base category and
allow the internal construction of the aforementioned operators when sound. To
this end, we introduce the transpension type former
${\between}i:\mathrm{Ty}(\Gamma)\to\mathrm{Ty}(\Gamma,i:{\mathbb{I}})$ which
in cartesian settings is right adjoint to
$\Pi(i:{\mathbb{I}}):\mathrm{Ty}(\Gamma,i:{\mathbb{I}})\to\mathrm{Ty}(\Gamma)$
and is therefore not a quantifier binding $i$, but a coquantifier that
_depends_ on it. Using the transpension and $\mathsf{Strict}$, we can
construct $\Phi$ (when sound), $\Psi$, $\mathbin{\surd}$ and $\mathsf{Glue}$.
Given a type former for certain pushouts, we can also construct
$\mathsf{Weld}$ and $\mathsf{mill}$, and perform reasoning akin to what is
made possible by capturing locally fresh names.

The transpension coquantifier
${\between}(u:{\mathbb{U}}):\mathrm{Ty}(\Gamma)\to\mathrm{Ty}(\Gamma,u:{\mathbb{U}})$
is part of a sequence of adjoints
$\Sigma\,u\dashv\Omega\,u\dashv\Pi\,u\dashv{\between}\,u$, preceded by the
$\Sigma$-type, weakening and the $\Pi$-type. Adjointness of the first three is
provable from the structural rules of type theory. However, it is not
immediately clear how to add typing rules for a further adjoint. Birkedal et
al. [BCM+20] explain how to add a single modality that has a left adjoint in
the semantics. If we want to have two or more adjoint modalities internally,
then we can use a multimodal type system such as MTT [GKNB20b, GKNB20a]. Each
modality in MTT needs a semantic left adjoint, so we can only internalize
$\Omega\,u$, $\Pi\,u$ and ${\between}\,u$. A drawback which we accept, is that
$\Omega\,u$ and $\Pi\,u$ become modalities which are a bit more awkward to
deal with than ordinary weakening and $\Pi$-types.

###  1.4. Contributions

Our central contribution is to reduce the plethora of interal presheaf
operators in the literature to only a few operations.

  * •

To this end, we introduce the transpension type ${\between}(u:{\mathbb{U}})$,
right adjoint to $\Pi(u:{\mathbb{U}})$, with typing rules built on
_extensional_ MTT [GKNB20b, GKNB20a]. We explain how it is reminiscent of the
suspension type from HoTT [Uni13].

  * •

More generally, the transpension type can be right adjoint to any quantifier-
like operation $\forall(u:{\mathbb{U}})$ which need neither respect the
exchange rule, nor weakening or contraction. In this setting, we also
introduce the fresh weakening coquantifier $\Finv(u:{\mathbb{U}})$, which is
left adjoint to $\forall(u:{\mathbb{U}})$ and therefore coincides with
weakening $\Omega(u:{\mathbb{U}})$ in cartesian settings.

  * •

We provide a categorical semantics for ${\between}(u:{\mathbb{U}})$ in almost
any presheaf category $\mathrm{Psh}({\mathcal{W}})$ over base category
${\mathcal{W}}$, for almost any representable object
${\mathbb{U}}=\mathbf{y}U$, $U\in{\mathcal{W}}$. To accommodate non-cartesian
variables, our system is not parametrized by a representable object
${\mathbb{U}}=\mathbf{y}U$, but by an arbitrary endofunctor
${\llcorner\lrcorner}\ltimes U$ on ${\mathcal{W}}$: the multiplier. We
introduce criteria for characterizing the multiplier – viz. semi-cartesian,
cartesian, cancellative, affine, connection-free and quantifiable – which we
use as requirements for internal type theoretic features. We identify a
complication dubbed spookiness in certain models (most notably in guarded type
theory), and define dimensionally split morphisms (a generalization of split
epimorphisms) in order to include spooky models. We exhibit relevant
multipliers in base categories found in the literature (section 4.3.1).

  * •

We show that all general presheaf internalization operators that we are aware
of – viz. $\Phi$/$\mathsf{extent}$ (when sound), $\Psi$/$\mathsf{Gel}$ [Mou16,
BCM15], the amazing right adjoint $\mathbin{\surd}$ [LOPS18], $\mathsf{Glue}$
[CCHM17, NVD17], $\mathsf{Weld}$ [NVD17], $\mathsf{mill}$ [ND18b] and (with no
formal claim) locally fresh names – can be recovered from just the
transpension type, the strictness axiom and pushouts along
$\mathsf{snd}:\varphi\times A\to A$ where $\varphi:\mathsf{Prop}$. In the
process, some of these operators can be improved: We generalize $\Psi$ from
affine to arbitrary multipliers, including cartesian ones and we justify
${\mathbb{U}}\mathbin{\surd}{\llcorner\lrcorner}$ without a global modality
and get proper computation rules for it. Moreover, since our system provides
an operation $\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}{\between}\,u}}$
for quantifying over contexts, we take a step towards auto-internalizing Orton
et al.’s work [LOPS18, Ort18, OP18]. When $\Phi$ is not sound (e.g. in
cartesian or non-connection-free settings), we suggest the internal notion of
transpensive types to retain some of its power. Finally, a form of higher
dimensional pattern matching is enabled by exposing $\forall(u:{\mathbb{U}})$
internally as a left adjoint.

  * •

In a technical report [Nuy20b], we investigate how the modalities introduced
in this paper commute with each other, and with prior modalities (i.e. those
already present before adding the transpension type). We also consider natural
transformations between modalities (called 2-cells in MTT) arising from
natural transformations between multipliers.

While MTT [GKNB20b, GKNB20a] satisfies canonicity222The current state of
affairs is that MTT extended with a single typing rule satisfies canonicity.
That rule is not compatible with the model used in this paper, but Gratzer et
al. are working on a canonicity theorem for MTT proper., decidable type-
checking will at least require a computational understanding of the mode
theory, and of some new typing rules that we add to MTT. For this reason, we
build on extensional MTT [GKNB20a], and defer decidability and canonicity to
future work.

##### Overview of the paper

In section 2, we demonstrate in a simple setting how the transpension type
resembles the suspension type from HoTT and how it allows for higher-
dimensional pattern matching. In section 3, we give a brief overview of the
typing rules of MTT and introduce our notation using _ticks_. In section 4, we
define the mode theory on which we will instantiate MTT and highlight some
important modalities. The instantiation of MTT is the type system we are
after, but it is next to unreadable for humans, so in section 5, we define an
informal notation that is _much_ less precise but more readable. In section 6,
we supplement our MTT instance with a few specialized typing rules. In section
7, we investigate the structure of the transpension type. In section 8, we
explain how to recover known internal presheaf operators. We conclude in
section 9.

##  2\. A Naïve Transpension Type

In this section, for purposes of demonstration, we present simplified typing
rules for the transpension. Using these, we will already be able to exhibit
the transpension as similar to a dependent version of the suspension in HoTT
[Uni13]. Moreover, in order to showcase how the transpension type allows us to
internalize the presheaf structure of other types, we will demonstrate a
technique which we call higher-dimensional pattern matching and which has
already been demonstrated by Pitts [Pit14] in nominal type theory using
locally fresh names.

Affine shape variables:

$\dfrac{\begin{array}[]{l
l}\Gamma\,\mathsf{ctx}\end{array}\hfill}{\begin{array}[]{l
l}\Gamma,u:{\mathbb{U}}\,\mathsf{ctx}\end{array}\hfill}\text{}\qquad\dfrac{\begin{array}[]{l
l}\sigma:\Gamma\to\Gamma^{\prime}\end{array}\hfill}{\begin{array}[]{l
l}(\sigma,u/v):(\Gamma,u:{\mathbb{U}})\to(\Gamma^{\prime},v:{\mathbb{U}})\end{array}\hfill}\text{}\qquad\dfrac{\begin{array}[]{l
l}\sigma:\Gamma\to\Gamma^{\prime}\end{array}\hfill}{\begin{array}[]{l
l}\sigma:(\Gamma,u:{\mathbb{U}})\to\Gamma^{\prime}\end{array}\hfill}\text{}$

Affine function type:

$\dfrac{\begin{array}[]{l l}\Gamma,u:{\mathbb{U}}\vdash
A\,\mathsf{type}\end{array}\hfill}{\begin{array}[]{l
l}\Gamma\vdash\forall\,u.A\,\mathsf{type}\end{array}\hfill}\text{}\qquad\dfrac{\begin{array}[]{l
l}\Gamma,u:{\mathbb{U}}\vdash a:A\end{array}\hfill}{\begin{array}[]{l
l}\Gamma\vdash\lambda
u.a:\forall\,u.A\end{array}\hfill}\text{}\qquad\dfrac{\begin{array}[]{l
l}\Gamma\vdash f:\forall\,u.A\end{array}\hfill}{\begin{array}[]{l
l}\Gamma,u:{\mathbb{U}},\delta:\Delta\vdash f\,u:A\end{array}\hfill}\text{}$

Telescope quantification:

$\begin{array}[]{l c l}\forall\,u.()&=&()\\\
\forall\,u.(\delta:\Delta,x:A)&=&(\forall\,u.(\delta:\Delta)),x|_{u={\llcorner\lrcorner}}:\forall\,u.(A[\delta|_{u=u}/\delta])\\\
\forall\,u.(\delta:\Delta,v:{\mathbb{U}})&=&(\forall\,u.(\delta:\Delta)),v:{\mathbb{U}}\end{array}$

Transpension type:

$\dfrac{\begin{array}[]{l
l}\Gamma,u:{\mathbb{U}}\vdash(\delta:\Delta)\,\mathsf{telescope}\\\
\Gamma,\forall\,u.(\delta:\Delta)\vdash
A\,\mathsf{type}\end{array}\hfill}{\begin{array}[]{l
l}\Gamma,u:{\mathbb{U}},\delta:\Delta\vdash{\between}(u:{\mathbb{U}}).A\,\mathsf{type}\end{array}\hfill}\text{}\qquad\dfrac{\begin{array}[]{l
l}\Gamma,u:{\mathbb{U}}\vdash
t:{\between}\,u.A\end{array}\hfill}{\begin{array}[]{l
l}\Gamma\vdash\mathsf{unmer}(u.t):A\\\
\mathrm{where}\,\,\mathsf{unmer}(u.\mathsf{mer}\,u\,a)=a\end{array}\hfill}\text{}$

$\dfrac{\begin{array}[]{l l}\Gamma,\forall\,u.(\delta:\Delta)\vdash
a:A\end{array}\hfill}{\begin{array}[]{l
l}\Gamma,u:{\mathbb{U}},\delta:\Delta\vdash\mathsf{mer}\,u\,a:{\between}(u:{\mathbb{U}}).A\\\
\mathrm{where}\,\,\mathsf{mer}\,u\,(\mathsf{unmer}(v.t[v/u,\delta|_{u=v}/\delta]))=t\end{array}\hfill}\text{}$

Figure 1. Selection of typing rules for a naïve transpension type.

###  2.1. Typing rules

To do this, we first present, in fig. 1, typing rules for the transpension
type in a very simple setting: a type system with affine shape variables
$u:{\mathbb{U}}$. Variables to the left of $u$ are understood to be fresh for
$u$; variables introduced after $u$ may be substituted with terms depending on
$u$. In particular, we have no contraction
$(w/u,w/v):(w:{\mathbb{U}})\to(u,v:{\mathbb{U}})$, while exchange
$(x:A,u:{\mathbb{U}})\to(u:{\mathbb{U}},x:A)$ only works in one direction.
This is enforced by the special substitution rules for shape variables.

The rule for $f\,u$ requires that the function $f$ be fresh for $u$, i.e. that
$f$ depend only on variables to the left of $u$ [BCM15, Mou16].

Additionally, the system contains a transpension type ${\between}\,u.A$ over
${\mathbb{U}}$, with more unusual rules. When checking the type
${\between}(u:{\mathbb{U}}).A$ in context $(\Gamma,u:{\mathbb{U}},y:B)$, the
part $A$ will be checked in a modified context [BV17, ND19], were $y:B$ (which
potentially depends on $u$) will change type, becoming a function
$y|_{u={\llcorner\lrcorner}}:\forall\,u.B$ that can be applied to
$v:{\mathbb{U}}$ yielding $y|_{u=v}:B[v/u]$. In other words, we get hold of
the dependency of $y$ on $u$. The _meridian_ constructor $\mathsf{mer}\,u\,a$
is checked in a similar way, and is modelled by transposition for the
adjunction $\forall\,u\dashv{\between}\,u$. We remark that both
${\between}\,u.A$ and $\mathsf{mer}\,u\,a$ depend on $u$, whereas $A$ and $a$
do not, so in a way the transpension lifts data to a higher dimension, turning
points into ${\mathbb{U}}$-cells. The elimination rule takes data again to a
lower dimension: it turns a dependent ${\mathbb{U}}$-cell in the transpension
into a point in $A$. This is the co-unit of the adjunction. The $\beta$\- and
$\eta$-rules internalize the adjunction laws.

These typing rules are sound in certain presheaf categories (those where
${\mathbb{U}}$ is cancellative and affine, see definition 4.1), but are
unsatisfactory in several respects. First, we have no story for substitutions
which exist in cubical type systems such as
$(0/i):\Gamma\to(\Gamma,i:{\mathbb{I}})$ [BCM15, BCH14, CCHM17] or $(j\wedge
k/i):(\Gamma,j,k:{\mathbb{I}})\to(\Gamma,i:{\mathbb{I}})$ [CCHM17], as there
is no formation rule for ${\between}\,0.A$ or ${\between}\,(j\wedge k).A$.
Secondly, in non-affine generalizations, the transpension is not stable under
substitution of the shape variables preceding $u$ (cf. the commutation
properties for transpension and substitution in [Nuy20b]). In order to obtain
a better behaved type system, in the rest of the paper we will rely on MTT,
which we briefly summarize in section 3.

###  2.2. Poles

We can still try to get a grasp on ${\between}\,0.A$, however. In general we
have $T[0/i]\cong(\forall\,i.(i=0)\to T)$. For $T={\between}\,i.A$, the latter
type is inhabited by $\lambda i.\lambda
e.\mathsf{mer}\,i\,(\lightning\,(e|_{i=1}))$, since $e|_{i=1}$ proves $1=0$.
Moreover, using the $\eta$-rule, we can show that this is the only element.

Thus we see that the transpension type essentially consists of meridians
$(i:{\mathbb{I}})\to{\between}\,i.T$ for all $t:T$ which are all equal when
$i=0$ or $i=1$. This makes the transpension type quite reminiscent of a
dependent version of the suspension type from HoTT [Uni13], although the
quantification of the context is obviously a distinction.

###  2.3. Higher-dimensional pattern matching

Given two types $A,B:\mathsf{U}$, higher-dimensional pattern matching allows
us to construct a function $\Gamma\vdash f:(\forall\,u.A\uplus
B)\to(\forall\,u.A)\uplus(\forall\,u.B)$. This function expresses that any
${\mathbb{U}}$-shaped cell in the coproduct type $A\uplus B$ must be either a
cell in $A$ or a cell in $B$. In that sense, it exposes the presheaf structure
of the coproduct type $A\uplus B$ and other colimit constructions. We can
define $f$ as follows (and generalization to $A,B:\forall\,u.\mathsf{U}$ is
straightforward):

$f~{}\hat{c}=\mathsf{unmer}\mathopen{}\left(u.\mathsf{case}\,\hat{c}\,u\,\mathsf{of}\mathopen{}\left\\{\begin{array}[]{l
c l}\mathsf{inl}\,a&\mapsto&\mathsf{mer}\,u\,(\mathsf{inl}\,(\lambda
v.a|_{u=v}))\\\
\mathsf{inr}\,b&\mapsto&\mathsf{mer}\,u\,(\mathsf{inr}\,(\lambda
v.b|_{u=v}))\end{array}\right\\}\mathclose{}\right)\mathclose{}$

The argument to $\mathsf{unmer}(u.{\llcorner\lrcorner})$ should be of type
${\between}\,u.((\forall\,u.A)\uplus(\forall\,u.B))$. Interestingly, since we
have $u$ in scope, we can apply $\hat{c}:\forall\,u\ldotp(A\uplus B)$ to it,
and pattern match to decide which case we are in. Both cases are analogous; in
the first case, a variable $a:A$ is brought in scope, so we are in context
$(\Gamma,\hat{c}:\forall\,u.A\uplus B,u:{\mathbb{U}},a:A)$. We then use the
constructor $\mathsf{mer}\,u\,{\llcorner\lrcorner}$, which again removes $u$
from scope and turns $a:A$ into a function
$a|_{u={\llcorner\lrcorner}}:\forall\,u.A$. Then we trivially finish the proof
by writing $\mathsf{inl}\,(\lambda v.a|_{u=v})$, where we have $\eta$-expanded
$a|_{u={\llcorner\lrcorner}}$ mainly for facilitating further narrative. In
summary, between $\mathsf{unmer}$ and $\mathsf{mer}$, we had temporary access
to a variable $u:{\mathbb{U}}$ which allowed us to pattern-match on
$\hat{c}\,u$. More conceptually, we can say that the transpension allows us to
temporarily work with $\hat{c}$ as if it were a lower-dimensional value of
type $A\uplus B$. We will see in section 8 how similar ideas can be used to
implement other internalization operators. Interestingly, this construction of
$f$ using the transpension also comes with suitable computational behaviour.
When we evaluate $f\,(\lambda u.\mathsf{inl}(\hat{a}\,u))$, then $\hat{a}\,u$
is substituted for $a$. Next, $(\hat{a}\,u)|_{u=v}$ simplifies to
$\hat{a}\,v$, so we can $\eta$-contract $\lambda v.\hat{a}\,v$, and
$\beta$-reduce $\mathsf{unmer}$, which yields $\mathsf{inl}\,\hat{a}$ as
expected.

##  3\. Multimode Type Theory

As announced, we will rely on the extensional version of Gratzer et al.’s
multimode and multimodal dependent type system MTT [GKNB20b, GKNB20a] in order
to frame the transpension and its left adjoints as modal operators. We refer
to the original work for details, but in this section we highlight some
important aspects of MTT and introduce our notation using _ticks_.

###  3.1. The mode theory

MTT is parametrized by a _mode theory_ , which is a strict 2-category whose
objects, morphisms and 2-cells we will refer to as modes, modalities and,
well, 2-cells respectively. Semantically, every mode $p$ will correspond to an
entire model of dependent type theory $\mathopen{}\left\llbracket
p\right\rrbracket\mathclose{}$. A modality
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q$ will consist of a functor $\mathopen{}\left\llbracket\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}\right\rrbracket\mathclose{}:\mathopen{}\left\llbracket
q\right\rrbracket\mathclose{}\to\mathopen{}\left\llbracket
p\right\rrbracket\mathclose{}$ and an operation
$\mathopen{}\left\llbracket{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\right\rrbracket\mathclose{}$
that is almost a dependent right adjoint (DRA [BCM+20]) to
$\mathopen{}\left\llbracket\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}\right\rrbracket\mathclose{}$;
for all our purposes it will be an actual DRA and even one arising from a weak
CwF morphism [BCM+20, lemma 17][Nuy18a]. A 2-cell
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}$
is interpreted as a natural transformation
$\mathopen{}\left\llbracket{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}\downarrow\right\rrbracket\mathclose{}:\mathopen{}\left\llbracket\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}}\right\rrbracket\mathclose{}\to\mathopen{}\left\llbracket\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}\right\rrbracket\mathclose{}$
and hence also gives rise to an appropriate transformation
$\mathopen{}\left\llbracket{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}\right\rrbracket\mathclose{}:\mathopen{}\left\llbracket{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\right\rrbracket\mathclose{}\to\mathopen{}\left\llbracket{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}\right\rrbracket\mathclose{}$.

###  3.2. Judgement forms

The judgement forms of MTT are listed in fig. 2. All forms are annotated with
a mode $p$ which specifies in what category they are to be interpreted. Every
judgement form also has a corresponding equality judgement, which is respected
by everything as the typing rules are to be read as a specification of a
generalized algebraic theory (GAT [Car86]). The statements $p\,\mathsf{mode}$,
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q$ and
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}$
are simply requirements about the mode theory. This means we give no syntax or
equality rules for modalities and 2-cells: these are fixed by the choice of
mode theory.

Judgement forms:

$\displaystyle p\mathrel{|}\Gamma\,\mathsf{ctx}$ $\Gamma$ is a context at mode
$p$, $\displaystyle p\mathrel{|}\sigma:\Gamma\to\Delta$ $\sigma$ is a
simultaneous substitution from $\Gamma$ to $\Delta$ at mode $p$,
$\displaystyle p\mathrel{|}\Gamma\vdash T\,\mathsf{type}$ $T$ is a type in
context $\Gamma$ at mode $p$, $\displaystyle p\mathrel{|}\Gamma\vdash t:T$ $t$
has type $T$ in context $\Gamma$ at mode $p$.

Prerequisites:
Basic rules of dependent type theory (including all desired types) at each
mode $p$, e.g.:

$\dfrac{\begin{array}[]{l l}\text{\hypertarget{rule:ctx-empty}{{ctx-
empty}}}\\\ q\,\mathsf{mode}\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}\cdot\,\mathsf{ctx}\end{array}\hfill}\text{\text{}}\qquad\dfrac{\begin{array}[]{l
l}\text{\hypertarget{rule:ctx-ext}{{ctx-ext}}}\\\ q\mathrel{|}\Gamma\vdash
T\,\mathsf{type}\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}\Gamma.T\,\mathsf{ctx}\end{array}\hfill}\text{\text{}}$

$\dfrac{\begin{array}[]{l l}\text{\hypertarget{rule:uni}{{uni}}}\\\
q\mathrel{|}\Gamma\,\mathsf{ctx}\quad\ell\in{\mathbb{N}}\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}\Gamma\vdash\mathsf{U}_{\ell}^{q}\,\mathsf{type}_{\ell+1}\end{array}\hfill}\text{\text{}}\qquad\dfrac{\begin{array}[]{l
l}\text{\hypertarget{rule:uni:elim}{{uni:elim}}}\\\ q\mathrel{|}\Gamma\vdash
t:\mathsf{U}_{\ell}^{q}\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}\Gamma\vdash\mathsf{El}(t)\,\mathsf{type}_{\ell}\\\
\mathrm{where}\,\,\mathsf{El}(\ulcorner
T\urcorner)=T\end{array}\hfill}\text{\text{}}\qquad\dfrac{\begin{array}[]{l
l}\text{\hypertarget{rule:uni:intro}{{uni:intro}}}\\\ q\mathrel{|}\Gamma\vdash
T\,\mathsf{type}_{\ell}\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}\Gamma\vdash\ulcorner T\urcorner:\mathsf{U}_{\ell}^{q}\\\
\mathrm{where}\,\,\ulcorner\mathsf{El}(t)\urcorner=t\end{array}\hfill}\text{\text{}}$

Context locking:

Note:
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>is shorthand for
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}1}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>
$\dfrac{\begin{array}[]{l l}\text{\hypertarget{rule:lock}{{lock}}}\\\
q\mathrel{|}\Gamma\,\mathsf{ctx}\quad{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q\end{array}\hfill}{\begin{array}[]{l l}p\mathrel{|}\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}\,\mathsf{ctx}\\\
\mathrm{where}\,\,\Gamma=(\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}1}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\bullet}})\\\
\phantom{\mathrm{where}}\,\,(\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}},\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}})=(\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu\circ\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}\mathfrak{m}}})\end{array}\hfill}\text{\text{}}\qquad\dfrac{\begin{array}[]{l
l}\text{\hypertarget{rule:lock:fmap}{{lock:fmap}}}\\\
q\mathrel{|}\sigma:\Gamma\to\Delta\qquad{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu,\nu}:p\to
q\qquad{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}\end{array}\hfill}{\begin{array}[]{l
l}p\mathrel{|}(\sigma,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}}):(\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}})\to(\Delta,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}})\\\
\mathrm{where}\,\,\sigma=(\sigma,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\bullet}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\bullet}})\quad(\sigma,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha^{\prime}}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}^{\prime}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}^{\prime}}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}})=(\sigma,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}(\alpha^{\prime}\mathbin{\star}\alpha)}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}^{\prime}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}^{\prime}\mathfrak{n}}})\\\
\phantom{\mathrm{where}}\,\,1=(1,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}})\quad(\sigma,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}})\circ(\tau,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\beta}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{o}}})=(\sigma\circ\tau,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}(\beta\circ\alpha)}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{o}}})\end{array}\hfill}\text{\text{}}$

Modal context extension:

We consider the non-modal rule LABEL:rule:ctx-ext and its introduction,
elimination and computation rules as a special case of LABEL:rule:ctx-modext
for $p=q$ and $\mu=1$.

$\dfrac{\begin{array}[]{l l}\text{\hypertarget{rule:ctx-modext}{{ctx-
modext}}}\\\
q\mathrel{|}\Gamma\,\mathsf{ctx}\quad{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q\\\ p\mathrel{|}\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>T\,\mathsf{type}\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}\Gamma,{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}T\,\mathsf{ctx}\end{array}\hfill}\text{\text{}}\qquad\dfrac{\begin{array}[]{l
l}\text{\hypertarget{rule:ctx-modext:intro}{{ctx-modext:intro}}}\\\
q\mathrel{|}\sigma:\Gamma\to\Delta\qquad{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q\\\ p\mathrel{|}\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>t:T[\sigma]\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}(\sigma,t/x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}):\Gamma\to(\Delta,{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}T)\\\
\mathrm{where}\,\,\tau=((x/\oslash)\circ\tau,(x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}})[\tau]/x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}})\\\
\phantom{\mathrm{where}}\,\,(\sigma,t/x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}})\circ\rho=(\sigma\circ\rho,t[\rho,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}1}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}]/x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}})\end{array}\hfill}\text{\text{}}$

$\quad\dfrac{\begin{array}[]{l l}\text{\hypertarget{rule:ctx-modext:wkn}{{ctx-
modext:wkn}}}\\\
q\mathrel{|}\Gamma\,\mathsf{ctx}\qquad{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q\\\ p\mathrel{|}\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>T\,\mathsf{type}\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}(x/\oslash):(\Gamma,{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}T)\to\Gamma\\\
\mathrm{where}\,\,(x/\oslash)\circ(\sigma,t/x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}})=\sigma\end{array}\hfill}\text{\text{}}\qquad\dfrac{\begin{array}[]{l
l}\text{\hypertarget{rule:ctx-modext:var}{{ctx-modext:var}}}\\\
q\mathrel{|}\Gamma\,\mathsf{ctx}&{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q\\\ p\mathrel{|}\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>T\,\mathsf{type}&{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mathsf{locks}(\Delta)}\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}\Gamma,{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}T,\Delta\vdash
x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathsf{ticks}(\Delta)}}:T[{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathsf{ticks}(\Delta)}}]\\\
\mathrm{where}\,\,x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathsf{ticks}(\Delta)}}[{\mathrm{id}}_{\Gamma},t/x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}},{\mathrm{id}}_{\Delta}]=t[{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathsf{ticks}(\Delta)}}]\\\
\phantom{\mathrm{where}}\,\,x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathsf{ticks}(\Delta)}}[{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\beta}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathsf{ticks}(\Delta)}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathsf{ticks}(\Theta)}}]=x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}(\beta\circ\alpha)}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathsf{ticks}(\Theta)}}\end{array}\hfill}\text{\text{}}$

Locks in a telescope:

$\begin{array}[]{l l
l}\mathsf{locks}(\cdot)=1&\mathsf{locks}(\Delta,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}})=\mathsf{locks}(\Delta)\circ\mu&\mathsf{locks}(\Delta,{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}T)=\mathsf{locks}(\Delta)\\\
\mathsf{ticks}(\cdot)=\bullet&\mathsf{ticks}(\Delta,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}})=\mathsf{ticks}(\Delta)\mathfrak{m}&\mathsf{ticks}(\Delta,{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}T)=\mathsf{ticks}(\Delta)\end{array}$

Figure 2. Judgement forms and structural rules of MTT [GKNB20b][Nuy20a, fig.
5.5]. $\begin{array}[]{l}\dfrac{\begin{array}[]{l
l}\text{\hypertarget{rule:wdra}{{wdra}}}\\\
{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q\\\ p\mathrel{|}\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>A\,\mathsf{type}_{\ell}\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}\Gamma\vdash\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}{A}\right\rangle\mathclose{}\,\mathsf{type}_{\ell}\end{array}\hfill}\text{\text{}}\\\
\rule{0.0pt}{51.6665pt}\dfrac{\begin{array}[]{l
l}\text{\hypertarget{rule:wdra:intro}{{wdra:intro}}}\\\
{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q\\\ p\mathrel{|}\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>a:A\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}\Gamma\vdash\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}\,a:\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>l}\text{\hypertarget{rule:wdra:elim}{{wdra:elim}}}\\\
{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q\quad{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}:q\to
r\\\ q\mathrel{|}\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}}\vdash\hat{a}:\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>r\mathrel{|}\Gamma,{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}\shortmid\hat{x}:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}}\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>C\,\mathsf{type}\\\
r\mathrel{|}\Gamma,{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu\circ\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>c:C[\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}\,x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}\mathfrak{m}}}/\hat{x}\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>l}r\mathrel{|}\Gamma\vdash\mathsf{let}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}}\,(\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}\,x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}\mathfrak{m}}}=\hat{a})\,\mathsf{in}\,c:C[\hat{a}/\hat{x}\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>\mathrm{where}\,\,\mathsf{let}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}}\,(\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}\,x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}\mathfrak{m}}}=\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}\,a)\,\mathsf{in}\,c=c[a/x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>Figure 3. Typing rules for MTT’s modal types (weak DRAs) [GKNB20b][Nuy20a,
fig. 5.6].

$\dfrac{\begin{array}[]{l l}\text{\hypertarget{rule:modpi}{{modpi}}}\\\
p\mathrel{|}\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>A\,\mathsf{type}_{\ell}\quad{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q\\\
q\mathrel{|}\Gamma,{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>B\,\mathsf{type}_{\ell}\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}\Gamma\vdash({\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}A)\to
B\,\mathsf{type}_{\ell}\end{array}\hfill}\text{\text{}}$

$\dfrac{\begin{array}[]{l
l}\text{\hypertarget{rule:modpi:intro}{{modpi:intro}}}\\\
{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q\\\
q\mathrel{|}\Gamma,{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>b:B\end{array}\hfill}{\begin{array}[]{l
l}q\mathrel{|}\Gamma\vdash\lambda({\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x).b:({\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}A)\to
B\\\
\mathrm{where}\,\,\lambda({\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x).(f\cdot^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}})=f\end{array}\hfill}\text{\text{}}\qquad\dfrac{\begin{array}[]{l
l}\text{\hypertarget{rule:modpi:elim}{{modpi:elim}}}\\\
q\mathrel{|}\Gamma\vdash
f:({\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}A)\to
B\\\ p\mathrel{|}\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>a:A\quad{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:p\to
q\end{array}\hfill}{\begin{array}[]{l l}q\mathrel{|}\Gamma\vdash
f\cdot^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}a:B[a/x]\\\
\mathrm{where}\,\,(\lambda({\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x).b)\cdot^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}a=b[a/x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>
Figure 4. Typing rules for MTT’s modal $\Pi$-types [GKNB20b][Nuy20a, fig. 5.7]
(of which non-modal $\Pi$-types are a special case for $p=q$ and $\mu=1$).

###  3.3. Typing rules

The typing rules are listed in Figures 2, 3 and 4. We will discuss these in
turn. As every mode corresponds to a model of all of dependent type theory
(DTT), we can import all the usual typing rules of DTT and apply them at any
given fixed mode. We assume that DTT has a universe à la Coquand with mutually
inverse encoding and decoding operations (which we will henceforth suppress),
and we ignore cumulativity-related hassle, referring to Gratzer et al.
[GKNB20b] for details.

The formation and introduction rules of modal types
$\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}A\right\rangle\mathclose{}$
in fig. 3 (which should help to understand the more basic rules) work by
transposition: we apply the left adjoint (in the form of a lock) to the
context of their argument. As such, they behave like DRAs, but their
elimination rule is weaker, so we call them weak DRAs.

In order to disambiguate in certain situations, we choose to enrich the
original MTT syntax [GKNB20b, GKNB20a] by annotating locks with a name, which
we call ticks [Nuy20a, §5.3] after Bahr et al. [BGM17]. So
$\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>and
$\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}\,a$
will both bind a tick
${\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>
Going back to fig. 2, context formation starts with the empty context which
exists at any mode, and proceeds by adding locks and variables.

Adding locks is strictly functorial: it preserves identity and composition of
modalities (and we take the liberty to use strings like
$\mathfrak{n}\mathfrak{m}$ and $\bullet$ as ticks). In fact, it is strictly
2-functorial: it also has an action on 2-cells (producing substitutions
between locked contexts) that preserves identity and composition of 2-cells.
It is also strictly bifunctorial: we can combine a substitution and a 2-cell
to a substitution between locked contexts. If the 2-cell is the identity and
we are just renaming locks, then we write
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>for
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}1_{\mu}}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>as a variable is a placeholder for another program to be _pre_ composed, a
tick is a placeholder for another 2-cell to be _post_ composed. Thus, it may
seem silly that our notation cleanly separates ticks from 2-cells, and we
could write
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}\circ\alpha}/{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>instead of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>While mathematically more elegant, we found this to be completely unreadable.

A modal variable
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>is essentially the same as a non-modal variable
$\hat{x}:\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>(which in turn is shorthand for
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}1}\shortmid\hat{x}:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\bullet}}\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}{T}\right\rangle\mathclose{}$),
but the judgemental modal annotation allows direct access to a term of type
$A$ through the variable rule. Hence, the type $T$ is checked the same way as
it would be in
$\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>Terms substituted for a modal variable $x$ are also checked in the locked
context, and therefore term substitution binds a tick. The basic variable rule
would be
$\Gamma,{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\shortmid
x:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}T,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}:T$.
A 2-cell
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}$
takes the variable to a context with $\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>instead of $\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>By functoriality of locks, $\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>may be split into multiple locks, and by weakening we may insert types in
between. Building in these substitutions, we get the general variable rule
which features an arbitrary telescope $\Delta$ with
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mathsf{locks}(\Delta)}$.

Modal elimination (fig. 3) uses a let-syntax to turn the modal type into a
judgemental annotation on a variable. Modal function type formation and
introduction (fig. 4) are by simple abstraction. Modal function application
binds a tick.

###  3.4. Results

We highlight some results about MTT that are relevant in the current paper.

######  Proposition 3.1.

We have
$\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}1}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>A$ and
$\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu\circ\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}\mathfrak{m}}}{A}\right\rangle\mathclose{}\cong\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}}{\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>
######  Proposition 3.2.

For any 2-cell
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}$,
we have
$\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}{A}\right\rangle\mathclose{}\to\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{n}}}{A[{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>
######  Proposition 3.3.

If $\kappa\dashv\mu$ internal to the mode theory, there is a function
$\mathsf{prmod}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}:({\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\kappa}\shortmid^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{k}}}{\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}{A}\right\rangle\mathclose{}})\to
A[{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\varepsilon}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{k}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>satisfying a $\beta$\- and (thanks to extensionality) an $\eta$-law. Combined
with these rules,
$\mathsf{prmod}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}$
is equally expressive as the $\mathsf{let}$-eliminator for
$\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}{\llcorner\lrcorner}\right\rangle\mathclose{}$.

######  Proposition 3.4.

If $\kappa\dashv\mu$ internal to the mode theory, there is an isomorphism of
contexts
$\sigma=(x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\eta}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}\mathfrak{k}}}/y\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{k}}}):(\Gamma,x:A,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}})\cong(\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}},{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\kappa}\shortmid
y:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{k}}}A[{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\eta}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\bullet}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}\mathfrak{k}}}])$
with inverse
$\sigma^{-1}=({\mathrm{id}}_{\Gamma},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\eta}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\bullet}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}\mathfrak{k}}},y\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{k}}}/x\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\bullet}},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}^{\prime}}})\circ({\mathrm{id}}_{(\Gamma,\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}},y)},{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\varepsilon}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{k}\mathfrak{m}^{\prime}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\bullet}})$.
Correspondingly, given $B$ in the latter context, there is an isomorphism of
types
$\mathopen{}\left((x:A)\to\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}{B[\sigma]}\right\rangle\mathclose{}\right)\mathclose{}\cong\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}}}{({\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\kappa}\shortmid
y:^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{k}}}A[{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\eta}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\bullet}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{m}\mathfrak{k}}}])\to
B}\right\rangle\mathclose{}$.

##  4\. A Mode Theory for Shape (Co)quantification

For space reasons, we assume that there are no prior modalities, i.e. that the
type system to which we wish to add a transpension type is non-modal in the
sense that it has a single mode and only the identity modality. Prior
modalities are considered in the technical report [Nuy20b]. We assume that
this single prior mode is modelled by the presheaf category
$\mathrm{Psh}({\mathcal{W}})$.

###  4.1. Shape Contexts

A first complication is that the modalities
$\Omega\,u\dashv\Pi\,u\dashv{\between}\,u$ all bind or depend on a variable, a
phenomenon which is not supported by MTT. However, the following trick solves
this problem. Assume we have in the prior system a context $\Xi$ modelled by a
presheaf over ${\mathcal{W}}$. Then the presheaves
$\mathrm{Psh}({\mathcal{W}}/\Xi)$ over the category of elements
${\mathcal{W}}/\Xi$ of the presheaf $\Xi$ are also a model of dependent type
theory. Denoting the judgements of the latter system with a prefix
$\Xi\mathrel{|}$, it happens to be the case that judgements
$\Xi\mathrel{|}\Gamma\vdash J$ (i.e. $\Gamma\vdash J$ in
$\mathrm{Psh}({\mathcal{W}}/\Xi)$) have precisely the same meaning as
judgements $\Xi.\Gamma\vdash J$ in $\mathrm{Psh}({\mathcal{W}})$ (for a
suitable but straightforward translation of $J$). Thus, we will group together
all shape variables (variables for which we want a transpension type) in a
shape context $\Xi$ in front of the typing context. Our judgements will then
take the form $\Xi\mathrel{|}\Gamma\vdash J$. This allows us to frame $\Xi$ as
the _mode_ of the judgement.

###  4.2. Mode Theory

For simplicity, we take a highly general mode theory and will then only be
able to say interesting things about specific modes, modalities and 2-cells.
In practice, and especially in implementations, one will want to select a more
syntactic subtheory right away.

As modes, we take the set of all small presheaves over ${\mathcal{W}}$, which
we think of as shape contexts. The mode $\Xi$ is modelled in
$\mathrm{Psh}({\mathcal{W}}/\Xi)$. As modalities
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}:\Xi_{1}\to\Xi_{2}$,
we take all functors $\mathopen{}\left\llbracket\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}\right\rrbracket\mathclose{}:\mathrm{Psh}({\mathcal{W}}/\Xi_{2})\to\mathrm{Psh}({\mathcal{W}}/\Xi_{1})$
which have a right adjoint $\mu$ that is then automatically a weak CwF
morphism [Nuy20b][Nuy20a, thm. 6.4.1] and gives rise to a DRA [BCM+20, lemma
17][Nuy18a]. As 2-cells
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\nu}$,
we take all natural transformations.

###  4.3. Shapes and Multipliers

We now proceed by highlighting some interesting modes, modalities, and
2-cells. To begin with, we fix a collection of shapes. We associate to each
shape ${\mathbb{U}}$ a functor ${\llcorner\lrcorner}\ltimes
U:{\mathcal{W}}\to{\mathcal{W}}$ which extends to a functor
${\llcorner\lrcorner}\ltimes\mathbf{y}U:\mathrm{Psh}({\mathcal{W}})\to\mathrm{Psh}({\mathcal{W}})$.444Both
${\llcorner\lrcorner}\ltimes U$ and ${\llcorner\lrcorner}\ltimes\mathbf{y}U$
are to be regarded as single-character symbols, i.e. $\ltimes$ in itself is
meaningless. Internally, we will use shape variables to increase human
readability and to reduce the heaviness of notation for shape substitutions,
writing $(\Xi,u:{\mathbb{U}})$ for the shape context $\Xi\ltimes\mathbf{y}U$.
However, in a fully elaborate syntax these variables would be redundant.

Of course, if we model shape context extension with $u:{\mathbb{U}}$ by an
_arbitrary_ functor, then we will not be able to prove many results. Depending
on the properties of the functor, the variable $u$ will behave like an affine
one or like a cartesian one (or perhaps neither) and the $\Phi$-combinator
will or will not be sound for ${\mathbb{U}}$. For this reason, we introduce
some criteria that help us classify shapes:

######  Definition 4.1.

Assume ${\mathcal{W}}$ has a terminal object $\top$. A multiplier for an
object $U$ is a functor ${\llcorner\lrcorner}\ltimes
U:{\mathcal{W}}\to{\mathcal{W}}$ such that $\top\ltimes U\cong U$.555In the
technical report [Nuy20b], we generalize beyond endofunctors. This gives us a
natural second projection $\pi_{2}:({\llcorner\lrcorner}\ltimes U)\to U$. We
define the fresh weakening functor to the slice category as
$\Finv_{U}:{\mathcal{W}}\to{\mathcal{W}}/U:W\mapsto(W\ltimes U,\pi_{2})$. We
say that a multiplier (as well as its shape) is:

  * •

Semicartesian if it is copointed, i.e. has a first projection
$\pi_{1}:({\llcorner\lrcorner}\ltimes U)\to\mathrm{Id}$,

  * •

Cartesian if it is naturally isomorphic to the cartesian product with $U$,

  * •

Cancellative if $\Finv_{U}$ is faithful,

  * •

Affine if $\Finv_{U}$ is full,

  * •

Connection-free if $\Finv_{U}$ is essentially surjective on objects $(V,\psi)$
such that $\psi$ is dimensionally split (definition 4.3),

  * •

Quantifiable if $\Finv_{U}$ has a left adjoint
$\exists_{U}:{\mathcal{W}}/U\to{\mathcal{W}}$.

Variables of shape ${\mathbb{U}}$ admit weakening if and only if the
multiplier is semicartesian, and exchange and contraction if (but not only if)
it is cartesian. Weakening, exchange and contraction are all shape
substitutions, which will be internalized as modalities.

A non-trivial multiplier cannot be both affine and cartesian:

######  Proposition 4.2.

If a multiplier is affine and cartesian, then it is the identity functor.
[Nuy20b]

######  Definition 4.3.

A morphism $\psi:V\to U$ is called dimensionally split (w.r.t.
${\llcorner\lrcorner}\ltimes U$) if there is some $W$ such that
$\pi_{2}:W\ltimes U\to U$ factors over $\psi$. We define the boundary
$\partial U$ as the subpresheaf of the Yoneda-embedding $\mathbf{y}U$
consisting of those morphisms that are _not_ dimensionally split, and we
define ${\llcorner\lrcorner}\ltimes\partial U$ by pullback.666I.e.
$\Xi\ltimes\partial U$ is the pullback of
$\Xi\ltimes\mathbf{y}U\to\mathbf{y}U\supseteq\partial U$. It is the
subpresheaf of $\Xi\ltimes\partial U$ of all cells $\psi$ such that
$\pi_{2}\circ\psi$ is _not_ dimensionally split. We also write
$(\Xi,u:\partial{\mathbb{U}})$ for $\Xi\ltimes\partial U$.

In most popular base categories, all morphisms to $\top$ are split epi. Being
dimensionally split is then equivalent to being split epi. We call a category
spooky if some morphism to $\top$ is not split epi. The notion of
dimensionally split morphisms lets us consider the boundary and connection-
freedom (a requirement for modelling $\Phi$) also in spooky base categories,
where the output of $\Finv_{U}$ may not be split epi.

####  4.3.1. Examples

Let us look at some examples of multipliers. Their properties are listed in
fig. 5. Most properties are easy to verify, so we omit the proofs.

######  Example 4.4 (Identity).

The identity functor on an arbitrary category ${\mathcal{W}}$ is an
endomultiplier for $\top$. It is quantifiable, with
$\exists_{\top}:{\mathcal{W}}/\top\to{\mathcal{W}}:(W,())\mapsto W$.

######  Example 4.5 (Cartesian product).

Let ${\mathcal{W}}$ be a category with finite products and
$U\in{\mathcal{W}}$. Then ${\llcorner\lrcorner}\times U$ is an endomultiplier
for $U$, which is affine if and only if it is the identity (i.e. $U$ is
terminal, cf. propositions 4.2 and 4.4). It is quantifiable with
$\exists_{U}:{\mathcal{W}}/U\to{\mathcal{W}}:(W,\psi)\mapsto W$. Hence, we
have $\exists_{U}\Finv_{U}={\llcorner\lrcorner}\times U$.

######  Definition 4.6.

Let ${\mathsf{RG}}$ be the category generated by the following diagram and
equations:

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.75pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{\mathbb{N}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
13.39722pt\raise 4.50694pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{{\mathbf{s}}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 30.75pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}}}\ignorespaces{\hbox{}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
13.41666pt\raise-5.15277pt\hbox{{}\hbox{\kern 0.0pt\raise
0.0pt\hbox{\hbox{\kern 3.0pt\hbox{\hbox{\kern
0.0pt\raise-2.15279pt\hbox{$\scriptstyle{{\mathbf{t}}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 30.75pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}}}\ignorespaces{\hbox{}}{\hbox{\kern
30.75pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise
0.0pt\hbox{$\textstyle{{\mathbb{I}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
16.40695pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{{\mathbf{r}}}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
6.75002pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces}}}}\ignorespaces\qquad\begin{array}[]{r
c l}{\mathbf{r}}\circ{\mathbf{s}}&=&1_{{\mathbb{N}}},\\\
{\mathbf{r}}\circ{\mathbf{t}}&=&1_{{\mathbb{N}}}.\end{array}$

A presheaf over ${\mathsf{RG}}$ is a reflexive graph. More generally, let
${}^{k}{{\mathsf{RG}}}$ be the category generated by the following:

$\lx@xy@svg{\hbox{\raise 0.0pt\hbox{\kern
6.75pt\hbox{\ignorespaces\ignorespaces\ignorespaces\hbox{\vtop{\kern
0.0pt\offinterlineskip\halign{\entry@#!@&&\entry<EMAIL_ADDRESS>0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{\mathbb{N}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{}}\ignorespaces\ignorespaces\ignorespaces{\hbox{\kern
18.32639pt\raise 6.15pt\hbox{{}\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\hbox{\hbox{\kern
0.0pt\raise-1.75pt\hbox{$\scriptstyle{{\mathbf{e}}_{0},\ldots,{\mathbf{e}}_{k-1}}$}}}\kern
3.0pt}}}}}}\ignorespaces{\hbox{\kern 60.75pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}}}\ignorespaces{\hbox{}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{}}\ignorespaces{\hbox{\kern
60.75pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}}}\ignorespaces{\hbox{}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{}}\ignorespaces{\hbox{\kern
60.75pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}}}\ignorespaces{\hbox{}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}\ignorespaces\ignorespaces{\hbox{}}\ignorespaces{\hbox{\kern
60.75pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}\ignorespaces\ignorespaces{\hbox{\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}\lx@xy<EMAIL_ADDRESS>0.0pt\raise-3.41666pt\crvi}}}}}\ignorespaces{\hbox{}}{\hbox{\kern
30.75pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern
3.0pt\raise 0.0pt\hbox{$\textstyle{}$}}}}}}}{\hbox{\kern 60.75pt\raise
0.0pt\hbox{\hbox{\kern 0.0pt\raise 0.0pt\hbox{\hbox{\kern 3.0pt\raise
0.0pt\hbox{$\textstyle{{\mathbb{I}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$}}}}}}}\ignorespaces\ignorespaces\ignorespaces\ignorespaces{}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
31.40695pt\raise 0.0pt\hbox{\hbox{\kern
0.0pt\raise-1.50694pt\hbox{$\scriptstyle{{\mathbf{r}}}$}}}}}{\hbox{\lx@xy@droprule}}\ignorespaces{\hbox{\kern
6.75002pt\raise 0.0pt\hbox{\hbox{\kern 0.0pt\raise
0.0pt\hbox{\lx@xy@tip{1}\lx@xy@tip{-1}}}}}}{\hbox{\lx@xy@droprule}}{\hbox{\lx@xy@droprule}}\ignorespaces}}}}\ignorespaces\qquad\begin{array}[]{r
c l}{\mathbf{r}}\circ{\mathbf{e}}_{i}&=&1_{{\mathbb{N}}}.\end{array}$

######  Example 4.7 (Cartesian cubes).

Let ${}^{a}{{\mathsf{Cube}}}$ be the category of cartesian $a$-ary cubes. It
is the free cartesian monoidal category with same terminal object over
${}^{a}{{\mathsf{RG}}}$. Concretely:

  * •

Its objects take the form $(i_{1}:{\mathbb{I}},\ldots,i_{n}:{\mathbb{I}})$
(the names are desugared to de Bruijn indices, i.e. the objects are really
just natural numbers),

  * •

Its morphisms
$(i_{1}:{\mathbb{I}},\ldots,i_{n}:{\mathbb{I}})\to(j_{1}:{\mathbb{I}},\ldots,j_{m}:{\mathbb{I}})$
are arbitrary functions

$\varphi:\mathopen{}\left\\{j_{1},\ldots,j_{m}\right\\}\mathclose{}\to\mathopen{}\left\\{i_{1},\ldots,i_{n}\right\\}\mathclose{}\cup\mathopen{}\left\\{0,\ldots,a-1\right\\}\mathclose{}:j\mapsto
j\langle\varphi\rangle.$

We also write
$\varphi=(j_{1}\langle\varphi\rangle/j_{1},\ldots,j_{m}\langle\varphi\rangle/j_{m})$.
If a variable $i$ is not used, we may write $i/\oslash$ to emphasize this.

This category is spooky if and only if $a=0$. On this category, we consider
the multiplier ${\llcorner\lrcorner}\times(i:{\mathbb{I}})$, which is an
instance of example 4.5.

######  Example 4.8 (Affine cubes).

Let ${}^{a}{{\mathsf{Cube}}}_{\Box}$ be the category of affine $a$-ary cubes
as used in [BCH14] (binary) or [BCM15] (unary). It is the free monoidal
category with (same) terminal unit over ${}^{a}{{\mathsf{RG}}}$. Concretely:

  * •

Objects are as in ${}^{a}{{\mathsf{Cube}}}$,

  * •

Morphisms are as in ${}^{a}{{\mathsf{Cube}}}$ such that if
$j\langle\varphi\rangle=k\langle\varphi\rangle\not\in\mathopen{}\left\\{0,\ldots,a-1\right\\}\mathclose{}$,
then $j=k$. This rules out diagonal maps.

This category is spooky if and only if $a=0$. On this category, we the functor
${\llcorner\lrcorner}*(i:{\mathbb{I}}):W\mapsto(W,i:{\mathbb{I}})$, which is a
multiplier for $(i:{\mathbb{I}})$. This functor is quantifiable with
$\exists_{(i:{\mathbb{I}})}((W,j:{\mathbb{I}}),(j/i))=W$ and
$\exists_{(i:{\mathbb{I}})}(W,(\varepsilon/i))=W$ for each of the $a$
endpoints $\varepsilon$.

In the nullary case, ${}^{0}{{\mathsf{Cube}}}_{\Box}$ is the base category of
the Schanuel topos, which is equivalent to the category of nominal sets
[Pit13]. In that case, $\exists_{(i:{\mathbb{I}})}$ is not just left adjoint
to $\Finv_{(i:{\mathbb{I}})}$, but in fact an inverse and hence also right
adjoint. This is in line with the fact that in nominal type theory [PMD15],
there is a single name quantifier which can be read as either existential or
universal quantification.

Example |  Base category |  Multiplier |  Spooky category |  | Weakening/
---
Semicartesian

Exchange |  Contraction |  Cartesian |  Cancellative |  Affine |  Connection-free |  Quantifiable
4.4 | ${\mathcal{W}}$ | $\mathrm{Id}$ | ? |  |  |  |  |  |  |  |
4.5 | ${\mathcal{W}}$ | $({\llcorner\lrcorner}\times U)\not\cong\mathrm{Id}$ | ? |  |  |  |  | ? |  | ? |
4.7 | ${}^{a}{{\mathsf{Cube}}}$ | ${\llcorner\lrcorner}\times(i:{\mathbb{I}})$ | $a=0$ |  |  |  |  |  |  |  |
4.8 | ${}^{a}{{\mathsf{Cube}}}_{\Box}$ | ${\llcorner\lrcorner}*(i:{\mathbb{I}})$ | $a=0$ |  |  |  |  |  |  |  |
4.9 | ${\mathsf{CCHM}}$ | ${\llcorner\lrcorner}\times(i:{\mathbb{I}})$ |  |  |  |  |  |  |  |  |
4.10 | ${\mathsf{DCube}_{d}}$ | ${\llcorner\lrcorner}\times(i:{\llparenthesis k\rrparenthesis})$ |  |  |  |  |  |  |  |  |
4.11 | ${\mathsf{Clock}}$ | ${\llcorner\lrcorner}\times(i:{\text{\clock}}_{k})$ |  |  |  |  |  |  |  |  |
4.12 | ${\mathsf{TwCube}}$ | ${\llcorner\lrcorner}\ltimes{\mathbb{I}}$ |  |  |  |  |  |  |  |  |
4.13 | $n$ | $\min({\llcorner\lrcorner},i)$ |  |  |  |  |  |  |  |  |
4.14 | ${\mathsf{Simplex}}$ | ${\llcorner\lrcorner}\uplus_{<}\mathopen{}\left[0\right]\mathclose{}$ |  |  |  |  |  |  |  |  |
4.15 | ${}^{2}{{\mathsf{Cube}}}_{\bot}$ | ${\llcorner\lrcorner}\times\bot$ |  |  |  |  |  |  |  |  |
Figure 5. Some interesting multipliers and their properties.

######  Example 4.9 (CCHM cubes).

Let ${\mathsf{CCHM}}$ be the category of CCHM cubes [CCHM17]. Its objects are
as in ${}^{2}{{\mathsf{Cube}}}$ and its morphisms are functions from
$\mathopen{}\left\\{j_{1},\ldots,j_{m}\right\\}\mathclose{}$ to the free de
Morgan algebra over
$\mathopen{}\left\\{i_{1},\ldots,i_{n}\right\\}\mathclose{}$. We again
consider ${\llcorner\lrcorner}\times(i:{\mathbb{I}})$, another instance of
example 4.5. Connection-freedom is now violated by $(j\vee k/i),(j\wedge
k/i):(j:{\mathbb{I}},k:{\mathbb{I}})\to(i:{\mathbb{I}})$.

######  Example 4.10 (Depth $d$ cubes).

Let ${\mathsf{DCube}_{d}}$ with $d\geq-1$ be the category of depth $d$ cubes,
used as a base category in degrees of relatedness [ND18a, Nuy18a]. This is a
generalization of the category of binary cartesian cubes ${\mathsf{Cube}}$,
where instead of typing every dimension with _the_ interval ${\mathbb{I}}$, we
type them with the $k$-interval ${\llparenthesis k\rrparenthesis}$, where
$k\in\mathopen{}\left\\{0,\ldots,d\right\\}\mathclose{}$ is called the degree
of relatedness of the edge. Its objects take the form $(i_{1}:{\llparenthesis
k_{1}\rrparenthesis},\ldots,i_{n}:{\llparenthesis k_{n}\rrparenthesis})$.
Conceptually, we have a map ${\llparenthesis
k\rrparenthesis}\to{\llparenthesis\ell\rrparenthesis}$ if $k\geq\ell$. Thus,
morphisms $\varphi:(i_{1}:{\llparenthesis
k_{1}\rrparenthesis},\ldots,i_{n}:{\llparenthesis
k_{n}\rrparenthesis})\to(j_{1}:{\llparenthesis\ell_{1}\rrparenthesis},\ldots,j_{m}:{\llparenthesis\ell_{m}\rrparenthesis})$
send every variable $j:{\llparenthesis\ell\rrparenthesis}$ of the codomain to
$j\langle\varphi\rangle$, which is either 0, 1 or a variable
$i:{\llparenthesis k\rrparenthesis}$ of the domain such that $k\geq\ell$.

  * •

If $d=-1$, then there is only one object $()$ and only the identity morphism,
i.e. we have the point category.

  * •

If $d=0$, we just get ${\mathsf{Cube}}$.

  * •

If $d=1$, we obtain the category of bridge/path cubes
${\mathsf{BPCube}}:={\mathsf{DCube}_{1}}$. We write ${\mathbb{P}}$ for
${\llparenthesis 0\rrparenthesis}$ (the path interval) and ${\mathbb{B}}$ for
${\llparenthesis 1\rrparenthesis}$ (the bridge interval). Bridge/path cubical
sets are used as a model for parametric quantifiers [NVD17, Nuy18a].

On this category, we consider ${\llcorner\lrcorner}\times(i:{\llparenthesis
k\rrparenthesis})$, which is another instance of example 4.5.

######  Example 4.11 (Clocks).

Let ${\mathsf{Clock}}$ be the category of clocks, used as a base category in
guarded type theory [BM18]. It is the free cartesian category over $\omega$.
Concretely:

  * •

Its objects take the form
$(i_{1}:{\text{\clock}}_{k_{1}},\ldots,i_{n}:{\text{\clock}}_{k_{n}})$ where
all $k_{j}\geq 0$. We can think of a variable of type ${\text{\clock}}_{k}$ as
representing a clock (i.e. a time dimension) paired up with a certificate that
we do not care what happens after the time on this clock exceeds $k$.

  * •

Correspondingly, we should have a map
${\text{\clock}}_{k}\to{\text{\clock}}_{\ell}$ if $k\leq\ell$. So the
morphisms
$\varphi:(i_{1}:{\text{\clock}}_{k_{1}},\ldots,i_{n}:{\text{\clock}}_{k_{n}})\to(j_{1}:{\text{\clock}}_{\ell_{1}},\ldots,j_{m}:{\text{\clock}}_{\ell_{m}})$
are functions that send (de Bruijn) variables $j:{\text{\clock}}_{\ell}$ of
the codomain to a variable $j\langle\varphi\rangle:{\text{\clock}}_{k}$ of the
domain such that $k\leq\ell$.

This category is spooky. On this category we consider
${\llcorner\lrcorner}\times(i:{\text{\clock}}_{k})$, which is another instance
of example 4.5.

######  Example 4.12 (Twisted cubes).

Pinyo and Kraus’s category of twisted cubes ${\mathsf{TwCube}}$ [PK19] can be
described as a subcategory of the category of non-empty finite linear orders
(or, if you want, of its skeletalization: the category of simplices
${\mathsf{Simplex}}$). On these categories, we can define a functor
${\llcorner\lrcorner}\ltimes{\mathbb{I}}$ such that
$W\ltimes{\mathbb{I}}=W^{\mathsf{op}}\uplus_{<}W$, where we consider elements
from the left smaller than those from the right. Now ${\mathsf{TwCube}}$ is
the subcategory of ${\mathsf{Simplex}}$ whose objects are generated by $\top$
and ${\llcorner\lrcorner}\ltimes{\mathbb{I}}$ (note that every object then
also has an opposite since $\top^{\mathsf{op}}=\top$ and
$(V\ltimes{\mathbb{I}})^{\mathsf{op}}\cong V\ltimes{\mathbb{I}}$), and whose
morphisms are given by

  * •

$(\varphi,0):\mathrm{Hom}_{\mathsf{TwCube}}(V,W\ltimes{\mathbb{I}})$ for all
$\varphi:\mathrm{Hom}_{\mathsf{TwCube}}(V,W^{\mathsf{op}})$,

  * •

$(\varphi,1):\mathrm{Hom}_{\mathsf{TwCube}}(V,W\ltimes{\mathbb{I}})$ for all
$\varphi:\mathrm{Hom}_{\mathsf{TwCube}}(V,W)$,

  * •

$\varphi\ltimes{\mathbb{I}}:\mathrm{Hom}_{\mathsf{TwCube}}(V\ltimes{\mathbb{I}},W\ltimes{\mathbb{I}})$
for all $\varphi:\mathrm{Hom}_{\mathsf{TwCube}}(V,W)$,

  * •

$():\mathrm{Hom}_{\mathsf{TwCube}}(V,\top)$.

Note that this collection automatically contains all identities, composites,
and opposites. Isomorphism to Pinyo and Kraus’s category of twisted cubes can
be seen from their ternary representation [PK19, def. 34]. We now consider the
multiplier
${\llcorner\lrcorner}\ltimes{\mathbb{I}}:{\mathsf{TwCube}}\to{\mathsf{TwCube}}$,
which Pinyo and Kraus call the twisted prism functor. It is quantifiable with

$\exists_{{\mathbb{I}}}:\left\\{\begin{array}[]{l c
l}(W,((),0))&\mapsto&W^{\mathsf{op}}\\\ (W,((),1))&\mapsto&W\\\
(W\ltimes{\mathbb{I}},()\ltimes{\mathbb{I}})&\mapsto&W,\end{array}\right.$ (1)

with the obvious action on morphisms.

######  Example 4.13 (Finite ordinals).

In the base category $\omega$ of the topos of trees, used in guarded type
theory [BMSS12], a cartesian product is given by $i\times j=\min(i,j)$.
However, this category lacks a terminal object. Instead, on the subcategory
$n$, which is endowed with the same cartesian product, we consider the
multiplier ${\llcorner\lrcorner}\times i$, which is again an instance of
example 4.5.

######  Example 4.14 (Simplices).

In the category of simplices ${\mathsf{Simplex}}$, we consider the functor
${\llcorner\lrcorner}\ltimes\mathopen{}\left[1\right]\mathclose{}:={\llcorner\lrcorner}\uplus_{<}\mathopen{}\left[0\right]\mathclose{}$,
which adds a maximal element to a linear order. This is a multiplier for
$\mathopen{}\left[1\right]\mathclose{}$ and is quantifiable with
$\exists_{\mathopen{}\left[1\right]\mathclose{}}(W,\psi)=\psi^{-1}(0)$.

######  Example 4.15 (Non-cancellativity).

Let ${}^{2}{{\mathsf{Cube}}}_{\bot}$ be the category of binary cubes extended
with an initial object. We consider the cartesian product
${\llcorner\lrcorner}\times\bot$ which sends everything to $\bot$.

###  4.4. Modalities for Substitution

A substitution $\sigma:\Xi_{1}\to\Xi_{2}$ gives rise to a functor
$\Sigma^{/\sigma}:{\mathcal{W}}/\Xi_{1}\to{\mathcal{W}}/\Xi_{2}$ and hence
[Sta19] to a triple of adjoint functors
$\Sigma\,{\sigma}\dashv\Omega\,{\sigma}\dashv\Pi\,{\sigma}$ between the
presheaf categories, where $\Omega\,{\sigma}$ has the exact same semantics as
ordinary substitution. By consequence, if $\sigma$ is a weakening
substitution, then $\Sigma\,\sigma$ and $\Pi\,\sigma$ have semantics
isomorphic to those of ordinary $\Sigma$\- and $\Pi$-types.

The two functors $\Omega\,{\sigma}$ and $\Pi\,{\sigma}$ give rise to DRAs and
can be internalized as MTT modalities. We denote these as777By the second
notation, we mean that we declare new variables (with their type if there is
space) and write $u=t$ when we substitute $t$ for $u$.
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}$
or
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(\xi_{1}:\Xi_{1},\xi_{2}=\xi_{2}[\sigma])}:(\xi_{2}:\Xi_{2})\to(\xi_{1}:\Xi_{1})$
and as
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi\,\sigma}$
or
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi(\xi_{1}:\Xi_{1},\xi_{2}=\xi_{2}[\sigma])}:(\xi_{1}:\Xi_{1})\to(\xi_{2}:\Xi_{2})$.
For example, in cubical type theory, we get
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(i=0)}:(\Xi,i:{\mathbb{I}})\to\Xi$
with right adjoint
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi(i=0)}$,
and for semicartesian ${\mathbb{U}}$, we get
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(u:{\mathbb{U}})}:\Xi\to(\Xi,u:{\mathbb{U}})$
with right adjoint
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi(u:{\mathbb{U}})}$.

The $\Pi$-modality is strictly functorial, whereas the $\Omega$-modality is
pseudofunctorial: we need explicit 2-cells witnessing
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\tau\circ\Omega\,\sigma}\cong{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(\tau\circ\sigma)}$.888This
is because we defined the modality $\mu$ via
$\mathopen{}\left\llbracket\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\mu}}\right\rrbracket\mathclose{}$
and $\mathopen{}\left\llbracket\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi\,{\llcorner\lrcorner}}}\right\rrbracket\mathclose{}=\Omega\,{\llcorner\lrcorner}$
is strictly functorial in the model while
$\mathopen{}\left\llbracket\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,{\llcorner\lrcorner}}}\right\rrbracket\mathclose{}=\Sigma\,{\llcorner\lrcorner}$
is merely pseudofunctorial. However, Gratzer et al. [GKNB20a] have a
strictification theorem for models of MTT which can strictify the isomorphism.
These modalities are adjoint internally by virtue of the 2-cells for the unit
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{const}_{\sigma}}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}1}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi\,\sigma\circ\Omega\,\sigma}$
and co-unit
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{app}_{\sigma}}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma\circ\Pi\,\sigma}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}1}$.
If $\sigma$ introduces variables, then the codomain of the co-unit may be a
variable renaming that is semantically the identity, e.g.
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{app}_{(v/u:{\mathbb{U}})}}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(v:{\mathbb{U}})\circ\Pi(u:{\mathbb{U}})}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(v:{\mathbb{U}},u=v)}$.

######  Example 4.16.

If ${\mathbb{U}}$ is cartesian, then there is a diagonal substitution
$(w/u,w/v):(\Xi,w:{\mathbb{U}})\to(\Xi,u,v:{\mathbb{U}})$. Writing

$\displaystyle{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}={\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}1_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi\,u}}\mathbin{\star}1_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi\,v}}\mathbin{\star}\mathsf{const}_{(w,u=w,v=w)}}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi\,u\circ\Pi\,v}\Rightarrow$
$\displaystyle\qquad{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi\,u\circ\Pi\,v\circ\Pi(w,u=w,v=w)\circ\Omega(w,u=w,v=w)}={\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi\,w\circ\Omega(w,u=w,v=w)},$

this allows us to type the naïvely typed function $\lambda f.\lambda
w.f\,w\,w:(\Pi\,u.\Pi\,v.A)\to\Pi\,w.A[w/u,w/v]$ as

$\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi(u:{\mathbb{U}})}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{p}_{u}}}{\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi(v:{\mathbb{U}})}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{p}_{v}}}{A}\right\rangle\mathclose{}}\right\rangle\mathclose{}\to\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi(w:{\mathbb{U}})}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{p}_{w}}}{\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(w:{\mathbb{U}},u=w,v=w)}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{o}}}{A[{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\alpha}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{p}_{u}\mathfrak{p}_{v}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>
######  Remark 4.17.

The reframing of shape substitutions as a modality, has the annoying
consequence that substitution no longer reduces. However, both
$\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}\mathrel{|}{\llcorner\lrcorner}\right\rangle\mathclose{}$
and
$\mathsf{mod}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}}$
are semantically an ordinary substitution.999Not along
$\sigma:\Xi_{1}\to\Xi_{2}$, but along
$\sigma.\eta_{\Sigma\,\sigma\dashv\Omega\,\sigma}:\Xi_{1}.\Gamma\cong\Xi_{2}.\Sigma\,\sigma\,\Gamma$,
which happens to be an isomorphism. Thus, we could add computation rules such
as:

$\begin{array}[]{r c l r c
l}\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>B}\right\rangle\mathclose{}&=&\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{o}}}{A}\right\rangle\mathclose{}\times\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{o}}}{B}\right\rangle\mathclose{},&{}\quad\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{o}}}{\mathsf{U}}\right\rangle\mathclose{}&=&\mathsf{U},\\\
\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{o}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}}\,(a,b)&=&(\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{o}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}}\,a,\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{o}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}}\,b),&\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{o}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}}\,A&=&\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>
This is fine in an extensional type system, but would not play well with the
$\beta$-rule for modal types in an intensional system. Indeed,
$\beta$-reduction for
$\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>requires a solution to the following problem: when
$\hat{a}=\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{o}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,\sigma}}\,a$
definitionally, then we need to be able to infer $a$ up to definitional
equality from $\hat{a}$.

###  4.5. Modalities for (Co)quantification

The fresh weakening functor $\Finv_{U}:{\mathcal{W}}\to{\mathcal{W}}/U$
generalizes to a functor
$\Finv_{U}^{/\Xi}:{\mathcal{W}}/\Xi\to{\mathcal{W}}/(\Xi\ltimes\mathbf{y}U)$
between categories of elements. Assuming that the multiplier is
quantifiable,101010We have not encountered any interesting examples where this
is not the case. there is a left adjoint
$\exists_{U}^{/\Xi}\dashv\Finv_{U}^{/\Xi}$ [Nuy20b]. These two give rise to
four adjoint functors
$\exists(u:{\mathbb{U}})\dashv\Finv(u:{\mathbb{U}})\dashv\forall(u:{\mathbb{U}})\dashv{\between}(u:{\mathbb{U}})$
between the presheaf categories. The latter three give rise to DRAs and can be
internalized as MTT modalities.

Here, $\exists(u:{\mathbb{U}})$, $\Finv(u:{\mathbb{U}})$ and
$\forall(u:{\mathbb{U}})$ are the substructural counterparts to the cartesian
(co)quantifiers $\Sigma(u:{\mathbb{U}})$, $\Omega(u:{\mathbb{U}})$ and
$\Pi(u:{\mathbb{U}})$; and ${\between}(u:{\mathbb{U}})$ is the transpension
coquantifier. Reusing symbols for the cartesian counterparts, we denote the
units and co-units of these adjunctions as

$\begin{array}[]{r
r}{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{const}_{(u:{\mathbb{U}})}}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}1}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall(u:{\mathbb{U}})\circ\Finv(u:{\mathbb{U}})}&{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{app}_{(u:{\mathbb{U}})}}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Finv(u:{\mathbb{U}})\circ\forall(u:{\mathbb{U}})}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}1}\\\
{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{reidx}_{(u:{\mathbb{U}})}}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}1}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}{\between}(u:{\mathbb{U}})\circ\forall(u:{\mathbb{U}})}&{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{unmer}_{(u:{\mathbb{U}})}}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall(u:{\mathbb{U}})\circ{\between}(u:{\mathbb{U}})}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}1}\end{array}$

Again, we also write
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{app}_{(v/u:{\mathbb{U}})}}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Finv(v:{\mathbb{U}})\circ\forall(u:{\mathbb{U}})}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(v:{\mathbb{U}},u=v)}$
and
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{reidx}_{(v/u:{\mathbb{U}})}}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(v:{\mathbb{U}},u=v)}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}{\between}(v:{\mathbb{U}})\circ\forall(u:{\mathbb{U}})}$
to handle shape variable renamings that are semantically the identity.

######  Theorem 4.18 (Quantification).

[Nuy20b] If the multiplier is

  * •

cancellative and affine, then the substructural
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{const}_{(u:{\mathbb{U}})}}$
and
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{unmer}_{(u:{\mathbb{U}})}}$
are natural isomorphisms,

  * •

semi-cartesian (so that
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(u:{\mathbb{U}})}$
and
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi(u:{\mathbb{U}})}$
exist), then we have
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{spoil}_{(u:{\mathbb{U}})}}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Finv(u:{\mathbb{U}})}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(u:{\mathbb{U}})}$
and
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{cospoil}_{(u:{\mathbb{U}})}}:{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi(u:{\mathbb{U}})}\Rightarrow{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall(u:{\mathbb{U}})}$,

  * •

cartesian, then we can soundly identify
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Finv(u:{\mathbb{U}})}={\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(u:{\mathbb{U}})}$
and
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall(u:{\mathbb{U}})}={\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi(u:{\mathbb{U}})}$.

To understand the difference between
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Finv(u:{\mathbb{U}})}$
and
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(u:{\mathbb{U}})}$,
we can compare to the naïve system (section 2) or Moulin et al.’s system
[BCM15, Mou16]. There, shape variables $u:{\mathbb{U}}$ are part of the
context, and variables to the left of $u$ are fresh for $u$. Here, shape
variables are all in the shape context, but we use
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Finv\,u}$
and
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega\,u}$
(as well as the semantically identical $\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall\,u}}$
and $\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi\,u}}$)
to keep track of whether or not other variables should be fresh for $u$. Thus,
in terms of the naïve system,
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall(u:{\mathbb{U}})}$
introduces $u$ at the end of $\Gamma$ (marking all variables fresh with
$\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall\,u}}$),
and
${\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi(u:{\mathbb{U}})}$
introduces $u$ in front of $\Gamma$ (marking them non-fresh with
$\text{{{\char
181\relax}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Pi\,u}}$).
The naïve system allows exchanging shape and other variables in one direction
only, which is represented here by the generally non-invertible 2-cells
$\mathsf{spoil}$ and $\mathsf{cospoil}$. We emphasize that the word ‘fresh’
needs to be taken with a grain of salt: only for cancellative and affine
${\mathbb{U}}$ does invertibility of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{const}_{u}}$
guarantee that something fresh for $u$ does not depend on $u$.

######  Example 4.19.

As an instance of proposition 3.3, we obtain
$\mathsf{prmod}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall(v/u:{\mathbb{U}})}}:({\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Finv(v:{\mathbb{U}})}\shortmid^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{f}}}{\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall(u:{\mathbb{U}})}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{a}}}{A}\right\rangle\mathclose{}})\to\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\Omega(v:{\mathbb{U}},u=v)}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\bullet}}{A[{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{app}_{v/u}}{\downarrow}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{f}\mathfrak{a}}}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>which says that a non-cartesian function $g$ with naïve type $g:\forall\,u.A$
can be applied to $v:{\mathbb{U}}$ provided that $g$ is fresh for $v$.

######  Example 4.20 (Higher-dimensional pattern matching).

As in section 2, we create a function
$f:\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall(u:{\mathbb{U}})}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>B}\right\rangle\mathclose{}\to\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall(u:{\mathbb{U}})}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{a}}}{A}\right\rangle\mathclose{}\uplus\mathopen{}\left\langle{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall(u:{\mathbb{U}})}\mathrel{|}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color<EMAIL_ADDRESS>namely:

$f\,\hat{c}=\mathsf{prmod}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}{\between}\,u}}\cdot^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{a}}}\mathsf{case}\,(\mathsf{prmod}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall\,u}}\cdot^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{o}}}(\hat{c}\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{const}_{u}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{a}\mathfrak{o}}}))\,\mathsf{of}\mathopen{}\left\\{\begin{array}[]{l
c
l}\mathsf{inl}\,a\mapsto\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{t}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}{\between}\,u}}\,(\mathsf{inl}\,(\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{a}^{\prime}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall\,u}}\,(a\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{reidx}_{u}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{t}\mathfrak{a}^{\prime}}})))\\\
\mathsf{inr}\,b\mapsto\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{t}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}{\between}\,u}}\,(\mathsf{inr}\,(\mathsf{mod}^{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{a}^{\prime}}}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall\,u}}\,(b\,{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{reidx}_{u}}{\downarrow}_{{\color[rgb]{0.7,0.7,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0.7,0.7,0.7}\pgfsys@color@gray@stroke{0.7}\pgfsys@color@gray@fill{0.7}\mathfrak{t}\mathfrak{a}^{\prime}}})))\end{array}\right\\}\mathclose{}.$

We see that
$\mathsf{mod}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall\,u}}$
and
$\mathsf{prmod}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}\forall\,u}}$
correspond to shape abstraction and application in the naïve system,
$\mathsf{prmod}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}{\between}\,u}}$
to $\mathsf{unmer}$, and
$\mathsf{mod}_{{\color[rgb]{0.6,0.3,0}\definecolor[named]{pgfstrokecolor}{rgb}{0.6,0.3,0}{\between}\,u}}$
to $\mathsf{mer}$. The annotation
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\mathsf{const}_{u}}$
is an explicit weakening over $u:{\mathbb{U}}$, whereas