Layered Modal Type Theories

Jason Z. S. Hu
Brigitte Pientka

School of Computer Science
McGill University
McConnell Engineering Bldg. , 3480 University St.
H3A 0E9

We introduce layers to modal type theories, which subsequently enables type theories
for pattern matching on code in meta-programming and clean and straightforward

§ INTRODUCTION

Under Curry-Howard correspondence, <cit.> discovered that the modal
logic $S4$ corresponds to staged or meta-programming.
In their settings, what fundamentally characterizes meta-programming in $S4$ is the
reading of $\square A$ as the code of type $A$ and the following two axioms:

\begin{align*}
T &: \square A \to A \\
4 &: \square A \to \square \square A
\end{align*}

In these two axioms, $T$ means that we can extract a term of $A$ from its
In other words, $T$ runs a meta-program and generates a program which evaluates to a
value of $A$.
The Axiom $4$, on the other hand, allows the use of a macro inside of a macro of a
macro of a macro ... until an arbitrary depth.
Though <cit.> have made a convincing argument that $S4$ does
provide a logical foundation for meta-programming, compared to practice, the facility
provided by $S4$ is hardly enough.
In particular, tactics in proof assistants frequently refer to the current goal,
analyze the structure of the goal and apply various strategies to fill it in.
However, $S4$ in itself only allows composition of meta-programs. It does not
provide a clear direction of how one should add support for case analyses of code
structures as we would usually expect from a reasonable tactic language in a proof
The most recent breakthrough in this direction is due to <cit.>.
They propose Moebius, which extend System F with modal types so that it supports the
analysis or pattern matching on code.
The crucial ideas of their work are:

* contextual types due to <cit.>, which generalize
<cit.> and support representation of an open piece of code
relative to a certain local context, and

* levels, which ultimately are a technicality forced by the fact that pattern
matching on code must be able to pattern match on the code that again does pattern

Though this work has provided ideas and shed light on how we should support pattern
matching on code, there are also problems:

* Moebius, despite having preservation, does not have progress.
The crucial issue here is that Moebius does not provide guarantees on the covering
of pattern matching on code.
It is possible for a pattern matching to find no matching case for a piece of code,
in which case the evaluation gets stuck.

* Moebius does not have a normalization proof.
It is hard to say whether any well-typed program in Moebius terminates or not even
if there is a fix for the covering problem.

These shortcomings are usually not a big deal if Moebius is used as a programming language.
However, in type theory, we have to be more cautious, as our system must be
foundationally consistent.
In this technical report, we develop another group of modal type theories based on one
simple idea of layers.
In this idea, a modal type theory is stratified into layers (primarily into two but
possibly more) but terms share one common syntax.
The modalities are then responsible for distinguishing terms from different layers.
It turns out that having layers is one powerful idea that not only enables a simpler
way to do pattern matching on code, but also finds a clear correspondence in the
semantics, which seems to work around the limitations found by

In this technical report, we start with the simplest layered modal type theory that
can only be used to meta-program closed code.
Then we work our way up to support open code, and next pattern matching.
We are also interested in scaling the whole setup to dependent types, but we leave the
work in another technical report due to the size of the development.

§ LAYERED DUAL-CONTEXT FORMULATION

In this section, we develop the layered modal type theory $S4$ in the dual-context
style with simple types.
We first introduce the original formulation of $S4$
by <cit.> and compare it with our layered
It turns out that the original dual-context $S4$ is just a limit of our layered
As we will see, when we restrict the type theory to two layers, we obtain very clean
and intuitive semantics for the type theory.

§.§ Original Dual-context Formulation

The original dual-context formulation of $S4$ is pioneered
by <cit.>, which not only gives an
intuitionistic formulation of the modal logic $S4$, but also shows that $S4$
corresponds to meta-programming under Curry-Howard correspondence.
The core idea of the dual-context formulation is simple: there are two kinds of facts
in the system that are tracked by two different contexts.
One kind stands for truth or local facts.
The other kind is global facts.
Effectively, that $\square A$ is true is equivalent to that $A$ is globally true.
The type theory has the following syntax:

S, T    :=       □T S T

x, y            Local variables

u            Global variables

s, t    :=       x u Terms, $\Exp$

natural numbers

t u s t

λx. t s t functions

Γ, Δ   :=        ·Γ, x : T
Local contexts

Φ, Ψ   :=        ·Φ, u : T
Global contexts

We use natural numbers as our base type.
We could have introduced a recursor for $\Nat$ but omit it to avoid clutter.
Since there are two kinds of facts, we have two kinds of contexts and variables.
$\boxit t$ introduces a $\square$ type while $\letbox u s t$ eliminates one.
Their typing rules are:

[Ψ][·]t T

[Ψ, u : T]tT'
u s t T'

According tho the introduction rule, $\boxit t$ can only depends on global facts, so
we can be sure that it is also a global fact.
In the elimination rule, an additional global assumption of $T$ is added to the global
context when typing the body $t$.
We can easily see that these two rules are coherent in the sense of local soundness:

[Ψ][·]s T
[Ψ, u : T]tT'
u s t T

t[s/u] T

The right hand side holds due to a theorem of global substitutions.

§.§ Adding Layers

In this section, we add layers to the previous modal type theory.
The ultimate motivation for adding layers comes from the desire of drawing more
distinctions to code and computation.
In the original dual-context formulation, a judgment $\dtyping t T$ does not provide
information about whether we are treating $t$ as a piece of code or not.
This distinction is made in programmers' mind, when they place $t$ inside or outside
of $\tbox$.
However, this existing distinction is not made in the judgment, and we perceive that
this lack of information is the critical reason of why supporting pattern matching on
code is so difficult and cumbersome.
By adding layers, we add a subscript $i \in [0, n]$ for a fixed natural number $n$
to the typing judgment so that the nested layers of $\square$ are accounted for.

[Ψ][·] i t T
1 + it□T

i s□T
[Ψ, u : T] i tT'
i u s t T'

It is immediate to see that to recover the original $S4$, we simply take $n$ to
$\omega$ so that arbitrarily nested $\square$s are allowed.
In this sense, the original formulation becomes a special case of the layered
In this technical report, we focus on the case of $n = 1$, in which typing of code and
computation is naturally distinguished, and subsequently we find that supporting
pattern matching on code becomes natural and the semantics of the type theory is
amazingly intuitive.
Under Curry-Howard correspondence, we intend to make layer $0$ the layer for code, and
layer $1$ the one for computation.

When we take $n = 1$, the introduction rule is only possible when $i = 0$, namely

[Ψ][·] 0 t T

Since $\boxit t$ can only live at layer $1$, it is not possible to construct a
$\square T$ at layer $0$ without using the global assumptions.
To actual ban $\square$ entirely at layer $0$, we must maintain an invariant:

S T

$\iscore T$ holds whenever $T$ contains no $\square$.
We require that all types from a valid global context satisfy this judgment by
generalizing this judgment to $\iscore \Psi$.
Semantically, $\iscore T$ describes the types that belong to some core type theory
(simply typed $\lambda$-calculus in this case) where programming occurs, while
$\square$ is an add-on to extend this core type theory with
Similarly, we require that all types from a valid local context at layer $1$ must have
at max one layer of $\square$.
This is checked by the following judgment:

S T

This judgment ensures that a meta-program never describes another meta-program,
i.e. meta-meta-programs don't exist.
This might appear as a restriction at the first glance, but, lo and behold, most
widely used meta-programming systems have the same limitation and they have the
additional disadvantage of having a different meta-programming language[These
systems include macro systems of practical languages like C and Rust, and tactic
languages like Ltac, Ltac2 of Coq, and Eisbach of Isabelle].
Not to mention some of these systems are not even typed.
Yet, they are still widely used and are pretty practical.
We perceive this limitation as a blessing: practicality comes from simplicity, not
Clearly, $\istype T$ subsumes $\iscore T$.

If $\iscore T$, then $\istype T$.

The following theorem is part of the syntactic validity of the typing judgment:
If $\ltyping i t T$, then $\iscore \Psi$ and

* if $i = 0$, then $\iscore \Gamma$;

* if $i = 1$, then $\istype \Gamma$.

Moreover, the layers are associated with the validity of types:
thm:st:typ-wf $ $

* If $\ltyping 0 t T$, then $\iscore T$.

* If $\ltyping 1 t T$, then $\istype T$.

With these two intended theorems in mind, the rules become:

[Ψ][·] 0 t T

1 s□T
[Ψ, u : T] 1 tT'
1 u s t T'

<Ref> checks out in these two rules by seeing that the
induction hypotheses directly apply.
Notice that the elimination rule can only occur at layer $1$.
This is forced by the fact that $\square T$ is only possible at layer $1$.
Eliminating a $\square$ at layer $0$ is automatically vacuous, so we immediately
exclude that from our rules.
We finish the typing rules for other terms for completeness:

u : T ∈Ψ

u : T ∈Ψ

x : T ∈Γ

x : T ∈Γ

[Ψ][Γ, x : S]itT
iλx. tS T

itS T
it sT

<Ref> are checked by doing induction on the typing
At last, layer $0$ is subsumed by layer $1$:

If $\ltyping 0 t T$, then $\ltyping 1 t T$.

Induction. For the case of local variables, apply subsumption.

§.§ Programming in Layered Formulation

Before discussing more about the layered $S4$, let us see some programs written in
this system.
It is possible to implement Axioms $K$ and $T$:

[Ψ, u : A B, u' : A][Γ, f : □(A B), x :
□A] 0 uA B

[Ψ, u : A B, u' : A][Γ, f : □(A B), x : □A] 0 u'A
[Ψ, u : A B, u' : A][Γ, f : □(A B), x : □A] 0 u u'B
[Ψ, u : A B, u' : A][Γ, f : □(A B), x : □A] 1 (u u')□B
[Ψ][Γ, f : □(A B), x : □A] 1 u f u' x (u u')□B
1 λf x. u f u' x (u u')□(A B) □A □B

[Ψ, u : A][Γ, x : □A] 1 uA
[Ψ][Γ, x : □A] 1 u x uA
1 λx. u x u□A A

We omit the validity checking of contexts and types without loss of generality.

Nevertheless, though we claim this system is a layered $S4$, it does not admit the
Axiom $4$:

\begin{align*}
\square A \func \square \square A
\end{align*}

In fact, the type is not even valid.
$\istype{\square \square A}$ requires $\iscore{\square A}$, which is not possible.
This is intended because our goal is to exclude meta-meta-programs.
If we let $n > 1$, then it is possible to express this axiom.
Nevertheless, it is still possible to write reasonable meta-programs.
The following composes two pieces of code of type $\Nat$ with addition (if we assume
the system supports it):

\begin{align*}
\ltyping 1 {\lambda x\ y. \letbox u x {\letbox{u'}y{\boxit{(u + u')}}}}{\square \Nat
\func \square \Nat \func \square \Nat}
\end{align*}

Let this function be $f$. Then we can have:

\begin{align*}
\ltyping 1 {f\ (\boxit{(3 + 2)})\ (\boxit{(1 + 4)})}{\square \Nat}
\end{align*}

Executing this program generates the code $\boxit{((3 + 2) + (1 + 4))}$.
We will see soon that this execution has already reached a normal form because code is
distinguished by its syntactic structure, so this code is different from $\boxit{10}$,
for example.

§.§ Equivalence of Layered Formulation

In this section, we consider the equivalence of our layered formulation.
The equivalence relation is also layered.
In principle, the $\beta$ and $\eta$ equivalence rules only apply for layer $1$,
i.e. the computation layer.
Other rules like the PER rules and the congruence rules apply for both layers.

The PER rules:

i s t T
i t s T

i s t T
i t u T
i s u T

Congruence rules:

u : T ∈Ψ

u : T ∈Ψ

x : T ∈Γ
0 x x T

x : T ∈Γ
1 x x T

[Ψ][Γ, x : S]itt'T
iλx. tλx. t'S T

itt'S T
it st' s'T

1 ss'□T
[Ψ, u : T] 1 tt'T'
1 u s tus't' T'

$\beta$ equivalence:

[Ψ][Γ, x : S] 1 t T
1 s S
1(λx. t) st[s/x]T

[Ψ][·] 0 s T
[Ψ, u : T] 1 tT'
1 u s tt[s/u]T

$\eta$ equivalence:

1 tS T
1 t λx. (t x)S T

Due to lack of dynamics at layer $0$, equivalence in fact is just syntactic equality:

If $\ltyequiv 0 t s T$, then $t = s$.

Induction, and notice that $\beta$ and $\eta$ equivalences are excluded from layer

This lemma ensures that terms at layer $0$ are indeed treated as code, as they are
distinguished by their syntactic structures.

The $\beta$ equivalence rules depend on the folklore substitution lemma:
$ $

* If $\ltyping[\Psi][\Gamma, x : S, \Gamma'] 1 t T$ and $\ltyping 1 s S$, then
$\ltyping[\Psi][\Gamma, \Gamma']1{t[s/x]}T$.

* If $\ltyping[\Psi, u : S, \Psi'] i t T$ and $\ltyping[\Psi][\cdot] 0 s S$, then
$\ltyping[\Psi, \Psi'] i {t[s/u]}T$.

Notice that the case for local substitutions only occurs at layer $1$ while the case
for global substitutions occurs at both layers.
This is because local substitutions do not propagate under $\tbox$ so the $\beta$ rule
for function will never affect layer $0$.
Contrarily, global substitutions do go under $\tbox$, so we must consider all

Induction. In the case of global substitutions, notice layer $0$ is subsumed by
layer $1$.

Presupposition then is a consequence of substitution lemma:
If $\ltyequiv i{t}{t'}T$, then $\ltyping i t T$ and $\ltyping i {t'}T$.

Induction on $\ltyequiv i{t}{t'}T$.

§.§ Simultaneous Substitutions

In preparation for the semantic development, we first develop the theory of
simultaneous substitutions for the dual-context formulation.
Though this section directly targets our layered formulation, nothing here cannot be
generalized to the original formulation.
The development in this section will directly contribute to a deepened understanding
of the presheaf model developed later in this technical report.

Since there are two contexts in the dual-context style, we need two different kinds of
substitutions to handle those between global contexts and those between local
First, we consider the substitutions between global contexts.
They are very similar to the substitutions in simply typed $\lambda$-calculus:

\begin{align*}
\sigma := \cdot \sep \sigma, t/u \tag{Global substitutions}
\end{align*}

[Ψ][·] 0 tT
[Ψ]σ, t/uΦ, u : T

Notice that in the step case, the term $t$ is typed at layer $0$.
This is because a global substitution is meant to store a list of codes of right
The equivalence between global substitutions is simply the congruence rules:

[Ψ][·] 0 tt'T
[Ψ]σ, t/uσ', t'/uΦ, u : T

The step case is equivalent to say $t = t'$ and that $t$ is well-typed.

The local substitutions are similar.
We quickly list out the definitions for completeness:

\begin{align*}
\delta := \cdot \sep \delta, t/x \tag{Local substitutions}
\end{align*}

1 tT
δ, t/xΔ, x : T

Notice that in the step case, the term $t$ is typed at layer $1$.

1 tt'T
δ, t/xδ', t'/xΔ, x : T

Since the term equivalence in the step case is at layer $1$, it is possible to have
$\beta$ and $\eta$ equivalence occurring in a local substitution.
A simultaneous substitution between dual-contexts is simply a pair of global and local

σ; δΦ; Δ

σ; δσ', δ'Φ; Δ

To develop a substitution calculus, we first define the application of a global

\begin{align*}
x[\sigma] &:= x \\
u[\sigma] &:= \sigma(u) \tag{lookup $u$ in $\sigma$} \\
\ze[\sigma] &:= \ze \\
\su t [\sigma] &:= \su{(t[\sigma])} \\
\boxit t [\sigma] &:= \boxit{(t[\sigma])} \\
\letbox u s t [\sigma] &:= \letbox u {s[\sigma]} {(t[\sigma, u/u])} \\
\lambda x. t [\sigma] &:= \lambda x. (t[\sigma]) \\
t\ s [\sigma] &:= (t[\sigma]) \ (s[\sigma])
\end{align*}

The following substitution lemma holds:

If $\ltyping[\Phi] i t T$ and $\typing[\Psi] \sigma \Phi$, then $\ltyping i{t[\sigma]} T$.

We do induction on $\ltyping[\Phi] i t T$ and only consider some important cases:

* $t = u$

u : T ∈Φ

\begin{align*}
& \ltyping[\Psi][\cdot] 0 {\sigma(u)} T \tag{due to $u : T \in \Phi$} \\
& \ltyping i {\sigma(u)} T \tag{weakening and subsumption}
\end{align*}

* $t = \boxit t'$

[Φ][·] 0t' T

\begin{align*}
& \ltyping[\Psi][\cdot] 0{t'[\sigma]} T
\byIH \\
& \ltyping{1}{\boxit t'[\sigma]}{\square T}
\end{align*}

* $t = \letbox u s t'$

[Φ] 1 s□T'
[Φ, u : T'] 1 t'T
[Φ] 1 u s t' T

\begin{align*}
& \ltyping 1 {s[\sigma]}{\square T'}
\byIH \\
& \ltyping[\Psi, u : T'] 1 {t'[\sigma, u/u]}{T}
\tag{by IH and weakening} \\
& \ltyping{1}{\letbox u s t'[\sigma]}{T}
\end{align*}

Applying a local substitution follows the same principle:

\begin{align*}
x[\delta] &:= \delta(x) \tag{lookup $x$ in $\delta$} \\
u[\delta] &:= u  \\
\ze[\delta] &:= \ze \\
\su t [\delta] &:= \su{(t[\delta])} \\
\boxit t [\delta] &:= \boxit t \\
\letbox u s t [\delta] &:= \letbox u {s[\delta]} {(t[\delta])} \\
\lambda x. t [\delta] &:= \lambda x. (t[\delta, x/x]) \\
t\ s [\delta] &:= (t[\delta]) \ (s[\delta])
\end{align*}

The local substitution lemma is only concerned about layer $1$:

If $\ltyping[\Psi][\Delta] 1 t T$ and $\dtyping \delta \Delta$, then $\ltyping 1{t[\delta]} T$.

We do induction on $\ltyping[\Psi][\Delta] 1 t T$.
The fact that we only operate at layer $1$ has eliminated several cases.
We only work on a few selected cases.

* $t = x$

x : T ∈Δ

\begin{align*}
& \ltyping 1 {\delta(x)} T \tag{due to $x : T \in \Delta$}
\end{align*}

* $t = \boxit t'$

[Ψ][·] 0t' T

\begin{align*}
& \istype \Gamma \tag{by $\dtyping \delta \Delta$} \\
& \ltyping{1}{\boxit t'}{\square T}
\end{align*}

* $t = \letbox u s t'$

[Ψ][Δ] 1 s□T'
[Ψ, u : T'][Δ] 1 t'T
[Ψ][Δ] 1 u s t' T

\begin{align*}
& \ltyping 1 {s[\delta]}{\square T'}
\byIH \\
& \ltyping[\Psi, u : T'] 1 {t'[\delta]}{T}
\tag{by weakening of $\delta$ and IH} \\
& \ltyping{1}{\letbox u s t'[\delta]}{T}
\end{align*}

Then the application of a simultaneous substitution is just a chain of applying two
substitutions one after the other:

\begin{align*}
t [\sigma; \delta] := t[\sigma][\delta]
\end{align*}

If $\ltyping[\Phi][\Delta] 1 t T$ and $\dtyping{\sigma;\delta}{\Phi;\Delta}$, then
$\ltyping 1 {t[\sigma;\delta]} T$.

Simultaneous substitutions are only applicable at layer $1$.
At layer $0$, only we are only concerned about global substitutions.

Use the global substitution lemma and then the local one.

We can then generalize the application of global substitutions to local substitutions:

If $\dtyping[\Phi] \delta \Delta$ and $\typing[\Psi] \sigma \Phi$, then
$\dtyping{\delta[\sigma]} \Delta$.

This generalization is necessary to define the composition of two simultaneous substitutions:

\begin{align*}
(\sigma'; \delta') \circ (\sigma; \delta) := \sigma' \circ \sigma; \delta' [\sigma]
\circ \delta
\end{align*}

where the composition of global and local substitutions is just defined naturally.

If $\dtyping[\Psi'][\Gamma']{\sigma'; \delta'}{\Psi''; \Gamma''}$
and $\dtyping{\sigma; \delta}{\Psi'; \Gamma'}$, then
$\dtyping{(\sigma'; \delta') \circ (\sigma; \delta)}{\Psi''; \Gamma''}$

By inversion, we have the following

First it is clear that $\typing[\Psi]{\sigma' \circ \sigma'}{\Psi''}$ holds.
By the generalized global substitution lemma, we also have
$\dtyping[\Psi][\Gamma']{\delta'[\sigma]}{\Gamma''}$ and hence
$\dtyping{\delta'[\sigma] \circ \delta}{\Gamma''}$.
That justifies our definition.

With the easy definition of identity, we see that there are two categories to organize
for the dual-context formulation.
First we have the category of global contexts and global substitutions.
In this category, terms in global substitutions are identified by their syntactic
The second category is the category of dual-contexts and simultaneous substitutions.
Local substitutions in simultaneous substitutions do admit dynamics and it is similar
to typical type theories like the simply typed $\lambda$-calculus.
In our presheaf model, we take their special subcategories of weakenings as bases and
use $\square$ to travel between two bases.
Terms in the first category is interpret to programs in the second, so that dynamics
of syntactic structures are recovered.

§ A PRESHEAF MODEL AND NORMALIZATION BY EVALUATION

In this section, we follow the ideas we built at the end of the last section and build
a presheaf model for our 2-layered dual-context modal type theory.
From this presheaf model, we extract a normalization by
evaluation <cit.>
algorithm that is sound and complete w.r.t. the typing and equivalence judgments.
Normalization by evaluation (or NbE for short) is a technique to establish the
normalization property of a type theory.
An NbE proof usually is composed of two steps: first, we evaluate the terms of a type
theory in some mathematical domain which has a notion of computation; second, we
extract from the values in this mathematical domain normal forms in the original type
Compared to the more traditional approach of reducibility candidates, An NbE proof has
the advantage of not having to establish the confluence property of certain reduction
The confluence property of the type theory is ultimately piggybacked on the confluence
property of that chosen domain.

An NbE proof using a presheaf model has become a standard technique in the community
to quickly and robustly establish the normalization property.
A presheaf category maps from some chosen base category to the category of sets.
By carefully choosing this base category, a straightforward interpretation from terms
to the presheaf category corresponds to a normalization algorithm.
In this section, this base category is the category of weakenings.
The presheaf model showed in this section is a moderate extension of the classic
presheaf model of simply typed $\lambda$-calculus <cit.>.

§.§ Weakenings

As previously mentioned, we will use the category of weakenings as the base
Similar to substitutions, we need to have two different kinds of weakenings.
In spite of that, weakenings are actually much simpler than substitutions, because we
only need to handle shifting of positions of variables in the contexts.
First, we define the weakenings of global contexts:

\begin{align*}
\gamma := \varepsilon \sep q(\gamma) \sep p(\gamma)
\tag{Global weakenings}
\end{align*}

ε: ·_g ·

γ: Ψ_g Φ
q(γ) : Ψ, u : T _g Φ, u : T

γ: Ψ_g Φ
p(γ) : Ψ, u : T _g Φ

This definition is identical to the one for simply typed $\lambda$-calculus.
We let $\id_\Psi : \Psi \To_g \Psi$ be the identity global weakening.
We omit the subscript whenever it is clear from the context.
In fact, local substitutions are defined in the same way:

\begin{align*}
\tau := \varepsilon \sep q(\tau) \sep p(\tau)
\tag{Local weakenings}
\end{align*}

ε: Ψ;·_l ·

τ: Ψ; Γ_l Δ
q(τ) : Ψ; Γ, x : T _l Δ, x : T

τ: Ψ; Γ_l Δ
p(τ) : Ψ; Γ, x : T _l Δ

We overload $\id_{\Psi; \Gamma} : \Psi; \Gamma \To_l \Gamma$ be the identity local
Again, we omit the subscript when it can be inferred from the context.
Both global and local weakenings have composition and form categories.
Then the weakenings of dual-contexts are defined as pairs of global and local

γ: Ψ_g Φ
τ: Ψ; Γ_l Δ
γ;τ: Ψ; ΓΦ; Δ

Composition of weakenings is simply defined as composition of global and local
substitutions, due to the following lemma:

If $\tau : \Psi; \Gamma \To_l \Delta$ and $\iscore \Phi$, then $\tau : \Phi; \Gamma \To_l \Delta$.

Our base category is set to be the category of dual-contexts and weakenings:

Dual-contexts and weakenings form a category.

We call this category .

§.§ Presheaf Model

In this section, we construct the presheaf model.
Since the presheaf model effectively constructs a normalization algorithm, we first
define what it means to be normal and neutral:

t^c    :=       x u t^c λx. t^c t^c t^c'
Core terms ($\CExp$)

w    :=        v w t^c λx. w
Normal form ($\Nf$)

v    :=        x u v w u v w Neutral form

In order to completely capture all normal forms by using grammar only, we introduce
core terms which effectively remove $\tbox$ and $\tletbox$ from the terms.
In other words, $t^c$ only represents programs that live at layer $0$.
Moreover, our definition of normal forms indicates that we are not concerned about
extensional equivalence of $\square$, including commuting conversions.
For example, the following is a well possible normal form:

\begin{align*}
\lambda x. (\letbox u v {\lambda y. u\ y}) x
\end{align*}

even though in principle it can be further simplified to:

\begin{align*}
\lambda x. \letbox u v {u\ x}
\end{align*}

This longer normal form is due to the lack of following commuting conversions:

\begin{align*}
\letbox u s {\lambda x. t} \approx \lambda x. \letbox u s t
\end{align*}

Namely in our system, $\tletbox$ and $\lambda$ do not commute.
In general, such commuting conversions can be introduced for sum types, i.e. those
types that use pattern matching instead of projections for elimination.
We can replace $\tletbox$ for an  expression for example to obtain a
possible commuting conversion for booleans.
In this report, we are not concerned about this because eventually our system will be
scaled to dependent types, where extensional equivalence is usually not considered
at all.

Furthermore, we let

\begin{align*}
\Nf^T_{\;\Psi; \Gamma} &:= \{ w \sep \ltyping 1 w T \} \\
\Ne^T_{\;\Psi; \Gamma} &:= \{ v \sep \ltyping 1 v T \}
\end{align*}

Notice that the sets only capture judgments at layer $1$, because at layer $0$, terms
do not compute so all well-typed terms are automatically normal.
$\Nf^T$ and $\Ne^T$ are the mapping from dual-contexts to the sets of normal and
neutral forms, respectively.
Evidently $\Nf^T$ and $\Ne^T$ are presheaves from the category of weakenings because
both normal and neutral forms respects weakenings.

To give the interpretation of types, we need exponential objects in the presheaf
Given two presheaves $F$ and $G$, we form a presheaf exponential $F \hfunc G$ by

\begin{align*}
F \hfunc G &: \WC^{op} \To \SetC \\
(F \hfunc G)_{\;\Psi;\Gamma} &:= \forall\ \Phi;\Delta \To \Psi;\Gamma. F_{\;\Phi;\Delta} \to G_{\;\Phi;\Delta}
\end{align*}

We interpret types as follows:

\begin{align*}
\intp{\_} &: \Typ \to \WC^{op} \To \SetC \\
\intp{\Nat} &:= \Nf^\Nat \\
\intp{\square T} &:= \Nf^{\square T} \\
\intp{S \func T} &:= \intp{S} \hfunc \intp{T}
\end{align*}

Notice that the interpretation of $\square T$ is not even recursive.
We directly interpret it as the presheaf of normal forms.
According to the definition of $\Nf^{\square T}$, there are two possibilities:

* either the term is already neutral, which there is nothing more we can learn, or

* it is of the form $\boxit t^c$.

In the latter case, we know that $t^c$ must be well-typed at layer $0$ as a closed
term, which gives us a ticket to its raw syntactic structure.
This is more obvious when we interpret the terms to natural transformations.
This interpretation does return a presheaf because all subcases return presheaves:
$ $

* If $\iscore T$, then $\intp{T}$ is a functor.

* If $\istype T$, then $\intp{T}$ is a functor.

If $a \in \intp{T}_{\;\Phi; \Delta}$ and $\gamma; \tau : \Psi; \Gamma \To \Phi; \Delta$,
we write $a[\gamma;\tau]$ for the functorial action of $\gamma;\tau$ on $a$.

Next we give semantics for dual-contexts.
The interpretation proceeds in two steps.
In the first step, we interpret global contexts in the category of global contexts and
global weakenings:

\begin{align*}
\intp{\Phi}^0_\Psi &:= \{ \gamma \sep \gamma : \Psi \To_g \Phi \} \\
\intp{\Phi}^1_\Psi &:= \{ \sigma \sep \typing[\Psi]{\sigma}{\Phi}\}
\end{align*}

The interpretation of global contexts is layered because in the interpretation of
terms, we need to interpret global contexts differently at different layers to ensure
the interpretation of terms does form a natural transformation.
This treatment will become clear when we consider terms.
At layer $0$, $\Phi$ is mapped to its Hom set, while at layer $1$, $\Phi$ is
interpreted as a presheaf of global substitutions.
We also use $\sigma$ to range over $\intp{\Phi}^i_{\Psi}$ when $i$ is unknown.
Then we interpret the local contexts:

\begin{align*}
\intp{\cdot}_{\;\Psi;\Gamma} &:= \{ * \} \\
\intp{\Delta, x : T}_{\;\Psi;\Gamma} &:= \intp{\Delta}_{\;\Psi;\Gamma}
\times \intp{T}_{\;\Psi;\Gamma}
\end{align*}

where $\{ * \}$ denotes a fixed singleton set.
We let $\rho$ to range over $\intp{\Delta}_{\;\Psi;\Gamma}$.
The interpretation of local contexts is not layered because computation only occurs at
layer $1$.
The interpretation of dual-contexts is also layered due to the layered interpretation
of global contexts:

\begin{align*}
\intp{\Phi;\Delta}^i_{\;\Psi;\Gamma} &:= \intp{\Phi}^i_\Psi \times
\intp{\Delta}_{\;\Psi;\Gamma}
\end{align*}

Functoriality of previous two interpretations are immediate:

If $\iscore \Phi$, then $\intp{\Phi}^i$ is a functor for both $i$.

If $\istype \Delta$, then $\intp{\Delta}$ is a functor.

If $\iscore \Phi$ and $\istype \Delta$, then $\intp{\Phi;\Delta}^i$ is a functor.

The functorial action is defined as follows: given $\gamma; \tau : \Psi'; \Gamma'
\To \Psi ; \Gamma$, we have

\begin{align*}
(\gamma'; \rho  : \intp{\Phi; \Delta}^0_{\;\Psi;\Gamma})[\gamma;\tau]
&:= \gamma' \circ \gamma; \rho [\gamma; \tau] \\
(\sigma; \rho  : \intp{\Phi; \Delta}^1_{\;\Psi;\Gamma})[\gamma;\tau]
&:= \sigma[\gamma]; \rho [\gamma; \tau]
\end{align*}

Notice that regardless of which layer, the local weakening does not have effect on
the interpretation of the global context.

Last we interpret terms to natural transformations between presheaves.
We need two auxiliary natural transformations which map $\Ne^T$ to $\intp{T}$ and
$\intp{T}$ to $\Nf^T$, respectively:

\begin{align*}
\downarrow^T &: \intp{T} \To \Nf^T \\
\downarrow^\Nat_{\;\Psi;\Gamma}(a) &:= a \\
\downarrow^{\square T}_{\;\Psi;\Gamma}(a)
&:= a \\
\downarrow^{S \func T}_{\;\Psi;\Gamma}(a)
&:= \lambda x. \downarrow^T_{\;\Psi;\Gamma, x : S}(a~(\id; p(\id)~,~{\uparrow^S_{\;\Psi;\Gamma, x : S}\!(x)}))
\tag{where $\id; p(\id) : \Psi; \Gamma, x{:} S \To \Psi; \Gamma$}\\[5pt]
\uparrow^T &: \Ne\ T \To \intp{T} \\
\uparrow^B_{\;\Psi;\Gamma}(v) &:= v \\
\uparrow^{\square T}_{\;\Psi;\Gamma}(v)
&:= v \\
\uparrow^{S \func T}_{\;\Psi; \Gamma}(v)
&:= (\gamma;\tau : \Phi;\Delta \To \Psi;\Gamma)(a)
\mapsto \uparrow^T_{\;\Phi;\Delta}(v[\gamma;\tau]\ \downarrow^S_{\;\Phi;\Delta}(a))
\end{align*}

In the following, we interpret terms as natural transformations:

\begin{align*}
\intp{\_}
&: \forall i \to \ltyping[\Phi][\Delta] i t T \to \intp{\Phi;\Delta}^i \To \intp{T} \\
\intp{t}^i_{\;\Psi;\Gamma}
&: \intp{\Phi;\Delta}_{\;\Psi;\Gamma} \to \intp{T}_{\;\Psi;\Gamma}
\tag{expanded form}\\
\intp{\ze}^i_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \ze \\
\intp{\su t}^i_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \su (\intp{t}^i_{\;\Psi;\Gamma}(\sigma; \rho)) \\
\intp{u}^0_{\;\Psi;\Gamma}(\gamma; \rho)
&:= \uparrow^{T}_{\;\Psi; \Gamma}(u[\gamma]) \\
\intp{u}^1_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \intp{\sigma(u)}^0_{\;\Psi; \Gamma}(\id; *) \\
\intp{x}^i_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \rho(x) \tag{lookup $x$ in $\rho$} \\
\intp{\boxit t}^1_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \boxit {(t[\sigma])} \\
\intp{\letbox u s t}^1_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \intp{t}^1_{\;\Psi;\Gamma}(\sigma, t^c/u; \rho)
\tag{if $\intp{s}^1_{\;\Psi;\Gamma}(\sigma; \rho) = \boxit {t^c}$} \\
\intp{\letbox u s t}^1_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \uparrow^{T}_{\;\Psi;\Gamma}(\letbox u v {\downarrow^T_{\;\Psi, u: S;\Gamma}(\intp{t}^1_{\;\Psi, u:
S;\Gamma}(\sigma', u/u; \rho'))})
\tag{if $\intp{s}^1_{\;\Psi;\Gamma}(\sigma; \rho) = v : \square S$ and $p(\id);
\id : \Psi, u: S;\Gamma \To \Psi;\Gamma$ and $(\sigma'; \rho') := (\sigma; \rho)[p(\id); \id]$} \\
\intp{\lambda x : S. t}^i_{\;\Psi;\Gamma}(\sigma;\rho)
&:= (\gamma;\tau : \Phi;\Delta \To \Psi;\Gamma)(a :
\intp{S}_{\;\Phi;\Delta}) \mapsto
\intp{t}^i_{\;\Phi;\Delta} (\sigma'; (\rho', a))
\tag{where $(\sigma'; \rho') := \sigma;\rho[\gamma; \tau]$}  \\
\intp{t\ s}^i_{\;\Psi;\Gamma}(\sigma;\rho) &:= \intp{t}^i_{\;\Psi;\Gamma} (\sigma;\rho, \id_{\;\Psi;\Gamma}~,~
\intp{s}^i_{\;\Psi;\Gamma}(\sigma;\rho))
\end{align*}

This interpretation extends the interpretation of simply typed $\lambda$-calculus.
The interpretation is also layered because the type theory itself is layered.
All cases that are not modal are identical to the simply typed $\lambda$-calculus
regardless of layers.
For example, in the variable case, we use the variable $x$ to look up the current
local environment $\rho$ to find a $\intp{T}_{\;\Psi;\Gamma}$.
What are more interesting are the modal cases.
The $\boxit t$ case is only available at layer $1$, because $\tbox$ is only well-typed
at this layer.
Since a $\tbox$'ed term should be identified with its syntactic structure, we directly
apply the global substitution $\typing[\Psi]\sigma\Phi$ and obtain a closed term
In the $\tletbox$ case, we must first evaluate $s$.
$\intp{s}^1_{\;\Psi;\Gamma} \in \intp{\square S}^1_{\;\Psi;\Gamma} =
\Nf^{\square S}_{\;\Psi;\Gamma}$, there are two possible outcomes of this evaluation: it is either a
$\boxit{t^c}$, or a neutral form.
In the first case, we have obtained a piece of code, so we can just extend $t^c$ for $u$
to the global substitution.
In this case, we can employ other interpretations.
For example, it is possible to inspect the syntactic structure of $t^c$.
If we have the following form in our syntax:

\begin{align*}
\isapp s t t'
\end{align*}

which inspects the structure of $s$.
If $s$ is a function application, then we branch to $t$, otherwise $t'$.
In this interpretation, we can clearly interpret this code:

\begin{align*}
\intp{\isapp s t t'}^1_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \intp{t}^1_{\;\Psi;\Gamma}(\sigma; \rho)
\tag{if $\intp{s}^1_{\;\Psi;\Gamma}(\sigma; \rho) = \boxit{(s^c\ t^c)}$} \\
\intp{\isapp s t t'}^1_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \intp{t'}^1_{\;\Psi;\Gamma}(\sigma; \rho)
\tag{if $\intp{s}^1_{\;\Psi;\Gamma}(\sigma; \rho) = \boxit{t^c}$ but $t^c$ is not
an application}
\end{align*}

The elimination form of a $\square$ can be more complex, e.g. case analysis on the code
However, though the semantic side is ready for a more complex interpretation, the
syntactic side is not rich enough to express the same level of complexity.
We will need a more powerful core theory, which exactly leads us to an adaptation to
dependent type theory.
We will develop this theory once we finish the development of simple types.

In the second case of $\tletbox$, on the other hand, we are blocked by some neutral
term, so we can only continue the evaluation of $t$ with $u$ as is, i.e. by applying
the $p(\id)$ weakening to the global substitution and then append the result with $u/u$.
We need the overall term to be some $\intp{T}_{\;\Psi;\Gamma}$, so we first reify the
evaluation of $t$ into a normal form, and then reflect the neutral back to the
abstract data in $\intp{T}_{\;\Psi;\Gamma}$.

Finally, we consider the interpretation of $u$.
This case is the most interesting one and is the essence of this layered
It is possible to refer to $u$ at both layers.
When we refer to $u$ at layer $1$, this means that we are actually bringing a term at
layer $0$ to layer $1$, so we must bring the dynamics of that term back alive.
This is why we interpret the lookup of $u$ in $\sigma$ at layer $0$.
The layer goes from $1$ to $0$ ensures the well-foundedness of the interpretation
regardless of what $\sigma(u)$ is.
The evaluation environment of the recursive interpretation is independent of the input
If we refer to $u$ at layer $0$, that means $u$ remains neutral even after the
evaluation in the core type theory.
In this case, we want to eventually return something representing a neutral term by
calling reflection.
In addition, we must ensure the naturality of the interpretation.
Combining both requirements, we come to the conclusion of using global weakenings only
for the interpretation of global contexts at layer $0$.
$u[\gamma]$ still returns a global variable.
This interpretation maintains monotonocity, which eventually
leads to naturality.

Next, we define the identity environment $\intp{\Gamma}_{\;\Psi;\Gamma}$ as

\begin{align*}
\uparrow^{\Gamma} &:  \intp{\Gamma}^1_{\;\Psi;\Gamma} \\
\uparrow^{\cdot} &:= * \\
\uparrow^{\Gamma, x : T} &:= (\uparrow^{\Psi; \Gamma} [\id; p(\id)], \uparrow^{T}_{\Psi; \Gamma, x : T}\!\!(x))
\end{align*}

Then we let

\begin{align*}
\uparrow^{\Psi; \Gamma} &:  \intp{\Psi; \Gamma}^1_{\;\Psi;\Gamma} \\
\uparrow^{\Psi; \Gamma} &:= \id; \uparrow^\Gamma
\end{align*}

This allows us to finally write down the normalization algorithm:

A normalization by evaluation algorithm given $\ltyping 1 t T$ is

\begin{align*}
\nbe^T_{\;\Psi;\Gamma}(t) &:= \downarrow^T_{\;\Psi;\Gamma} (\intp{t}^1_{\;\Psi;\Gamma}(\uparrow^{\Psi;\Gamma}))
\end{align*}

$\nbe^T_{\;\Psi;\Gamma}(t)$ returns a $\Nf^T_{\;\Psi;\Gamma}$.
The correctness of this algorithm is formulated by the following two target theorems:
If $\ltyequiv 1 t {t'} T$, then $\nbe^T_{\;\Psi;\Gamma}(t) = \nbe^T_{\;\Psi;\Gamma}(t')$.

If $\ltyping 1 t T$, then $\ltyequiv 1 t {\nbe^T_{\;\Psi;\Gamma}(t)} T$.

The completeness theorem states that if two terms are equivalent, then they have equal
normal forms.
The soundness theorem states that a well-typed term is equivalent to its normal
These two theorems are only concerned about layer $1$, because, again, this is the
only layer where computation actually occurs.
Starting the next section, we will develop properties of the interpretations and
establish the target theorems.

§.§ Properties of Interpretations

To establish the completeness and soundness theorems, we need the following important
If $\ltyping[\Phi][\Delta] i t T$, $\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma$ and
$\sigma;\rho \in \intp{\Phi;\Delta}^i_{\;\Psi;\Gamma}$, then
$\intp{t}^i_{\;\Psi;\Gamma}(\sigma;\rho)[\gamma;\tau] = \intp{t}^i_{\;\Psi';\Gamma'}((\sigma;\rho)[\gamma;\tau])$.

That is, the order of applying a weakening does not change the result.

We also need two lemmas that describe how the interpretation of terms interacts with
global and local substitutions:
$\intp{t}^i_{\;\Psi;\Gamma}(\sigma \circ \sigma';\rho) = \intp{t[\sigma]}^i_{\;\Psi;\Gamma}(\sigma';\rho)$

Assume $x$ is the topmost local variable,

$\intp{t[s/x]}^i_{\;\Psi;\Gamma}(\sigma;\rho) =
\intp{t}^i_{\;\Psi;\Gamma}(\sigma;(\rho, \intp{s}^i_{\;\Psi;\Gamma}(\sigma;\rho)))$

Let us first tackle the naturality of the interpretation.
The naturality of the interpretation relies on the naturality of both reification and

Both $\uparrow^T$ and $\downarrow^T$ are natural.

We perform induction on $T$.
We only need to check the function case because the other two cases are identity.
Let $T = S \func T'$.
First assume $\gamma;\tau : \Phi; \Delta \To \Psi; \Gamma$ and $a \in \intp{S \func
T'}_{\Psi; \Gamma}$, then we need to prove

\begin{align*}
\downarrow^{S \func T'}_{\;\Psi;\Gamma}(a)[\gamma;\tau]
= \downarrow^{S \func T'}_{\;\Phi;\Delta}(a[\gamma;\tau])
\end{align*}

We compute the left hand side:

\begin{align*}
\downarrow^{S \func T'}_{\;\Psi;\Gamma}(a)[\gamma;\tau]
&= (\lambda x. \downarrow^{T'}_{\;\Psi;\Gamma, x : S}(a(\id;
p(\id)~,~{\uparrow^S_{\;\Psi;\Gamma, x : S}\!(x)})))[\gamma; \tau] \\
&= \lambda x. \downarrow^{T'}_{\;\Psi;\Gamma, x : S}(a(\id;
p(\id)~,~{\uparrow^S_{\;\Psi;\Gamma, x : S}\!(x)}))[\gamma; q(\tau)] \\
&= \lambda x. \downarrow^{T'}_{\;\Psi;\Gamma, x : S}(a(\id;
p(\id)~,~{\uparrow^S_{\;\Psi;\Gamma, x : S}\!(x)})[\gamma; q(\tau)])
\byIH \\
&= \lambda x. \downarrow^{T'}_{\;\Phi;\Delta, x : S}(a(\gamma;
p(\tau)~,~{\uparrow^S_{\;\Phi;\Delta, x : S}\!(x)}))
\tag{Notice by IH $\uparrow^S_{\;\Psi;\Gamma, x : S}\!(x)[\gamma; q(\tau)] =
\uparrow^S_{\;\Psi;\Gamma, x : S}\!(x[\gamma; q(\tau)]) =
\uparrow^S_{\;\Phi;\Delta, x : S}\!(x)$} \\
&= \lambda x. \downarrow^{T'}_{\;\Phi;\Delta, x : S}(a((\gamma; \tau) \circ (\id;
p(\id))~,~{\uparrow^S_{\;\Phi;\Delta, x : S}\!(x)}))
\tag{$\gamma; p(\tau) = (\gamma \circ \id); (\tau \circ p(\id)) = (\gamma; \tau)
\circ (\id; p(\id))$} \\
&= \lambda x. \downarrow^{T'}_{\;\Phi;\Delta, x : S}(a[\gamma; \tau](\id;
p(\id)~,~{\uparrow^S_{\;\Phi;\Delta, x : S}\!(x)}))
\tag{functoriality of $\intp{S \func T'}$} \\
&= \downarrow^{S \func T'}_{\;\Phi;\Delta}(a[\gamma;\tau])
\end{align*}

Now we check reflection.
Assume $v \in \Ne^{S \func T'}_{\;\Psi;\Gamma}$, then we compute

\begin{align*}
\uparrow^{S \func T'}_{\;\Psi;\Gamma}(v)[\gamma;\tau]
&= (\gamma';\tau' : \Phi';\Delta' \To \Phi;\Delta)(a)
\mapsto \uparrow^{T'}_{\;\Phi';\Delta'}(v[\gamma;\tau \circ
\gamma';\tau']\ \downarrow^S_{\;\Phi';\Delta'}(a)) \\
&= (\gamma';\tau' : \Phi';\Delta' \To \Phi;\Delta)(a)
\mapsto \uparrow^{T'}_{\;\Phi';\Delta'}(v[\gamma;\tau][\gamma';\tau']\
\downarrow^S_{\;\Phi';\Delta'}(a))
\tag{by composition} \\
&= \uparrow^{S \func T'}_{\;\Phi;\Delta}(v[\gamma;\tau])
\end{align*}

Next we show that at layer $0$, the component of global weakenings itself is natural.
If $\ltyping[\Phi][\Delta] 0 t T$, $\gamma' : \Psi' \To_g \Psi$, $\gamma : \Psi \To_g \Phi$ and
$\rho \in \intp{\Delta}_{\;\Psi';\Gamma}$, then
$\intp{t}^0_{\;\Psi';\Gamma}(\gamma \circ \gamma';\rho) = \intp{t[\gamma]}^0_{\;\Psi';\Gamma}(\gamma';\rho)$.

Since we are only concerned about the global weakenings and we are at layer $0$, so
the only relevant case is the global variable case.
The other cases are immediate by IH.
Let $t = u$.

\begin{align*}
\intp{u}^0_{\;\Psi';\Gamma}(\gamma \circ \gamma';\rho)
&= \uparrow_{\;\Psi';\Gamma}(u[\gamma \circ \gamma']) \\
&= \uparrow_{\;\Psi';\Gamma}(u[\gamma][\gamma']) \\
&= \intp{u[\gamma]}^0_{\;\Psi';\Gamma}(\gamma';\rho)
\end{align*}

If $\ltyping[\Phi][\Delta] 0 t T$, $\gamma : \Psi \To_g \Phi$ and
$\rho \in \intp{\Delta}_{\;\Psi;\Gamma}$, then
$\intp{t}^0_{\;\Psi;\Gamma}(\gamma;\rho) = \intp{t[\gamma]}^0_{\;\Psi;\Gamma}(\id;\rho)$.

This is because $\gamma \circ \id = \gamma$.

This corollary allows us to always set the global weakening to $\id$ by pushing the
non-$\id$ one eagerly into the term.

Now we show that $\intp{t}^i$ is also natural.

We do induction on $\ltyping[\Phi][\Delta] i t T$.
We only focus on the modal cases:

* $i = 0$ and $t = u$. In this case,

\begin{align*}
\intp{u}^0_{\;\Psi;\Gamma}(\gamma';\rho)[\gamma;\tau]
&= \uparrow_{\;\Psi;\Gamma}(u[\gamma'])[\gamma;\tau] \\
&= \uparrow_{\;\Psi';\Gamma'}(u[\gamma'][\gamma;\tau])
\tag{naturality of reflection} \\
&= \uparrow_{\;\Psi';\Gamma'}(u[\gamma'][\gamma]) \\
&= \uparrow_{\;\Psi';\Gamma'}(u[\gamma' \circ \gamma]) \\
&= \intp{u}^0_{\;\Psi';\Gamma'}(\gamma' \circ \gamma;\rho[\gamma;\tau]) \\
&= \intp{u}^0_{\;\Psi';\Gamma'}((\gamma';\rho)[\gamma;\tau])
\end{align*}

* $i = 1$ and $t = u$. In this case,

\begin{align*}
\intp{u}^1_{\;\Psi;\Gamma}(\sigma;\rho)[\gamma;\tau]
&= \intp{\sigma(u)}^0_{\;\Psi;\Gamma}(\id; *)[\gamma;\tau] \\
&= \intp{\sigma(u)}^0_{\;\Psi';\Gamma'}((\id; *)[\gamma;\tau])
\byIH \\
&= \intp{\sigma(u)}^0_{\;\Psi';\Gamma'}(\gamma; *) \\
&= \intp{\sigma(u)[\gamma]}^0_{\;\Psi';\Gamma'}(\id; *)
\tag{by \Cref{lem:st:gsubst-nat}} \\
&= \intp{\sigma[\gamma](u)}^0_{\;\Psi';\Gamma'}(\id; *) \\
&= \intp{u}^1_{\;\Psi';\Gamma'}((\sigma;\rho)[\gamma;\tau])
\end{align*}

* $i = 1$ and $t = \boxit t'$.

\begin{align*}
\intp{\boxit t'}^1_{\;\Psi;\Gamma}(\sigma;\rho)[\gamma;\tau]
&= \boxit {(t'[\sigma])}[\gamma;\tau] \\
&= \boxit {(t'[\sigma][\gamma])} \\
&= \boxit {(t'[\sigma[\gamma]])} \\
&= \intp{\boxit t'}^1_{\;\Psi';\Gamma'}(\sigma[\gamma]; \rho[\gamma;\tau]) \\
&= \intp{\boxit t'}^1_{\;\Psi';\Gamma'}((\sigma;\rho)[\gamma;\tau])
\end{align*}

* $i = 1$ and $t = \letbox u s t'$ and $\intp{s}^1_{\;\Psi;\Gamma}(\sigma; \rho) =
\boxit {t^c}$.
Then we have

\begin{align*}
\intp{s}^1_{\;\Psi;\Gamma}(\sigma; \rho)[\gamma;\tau]
= \intp{s}^1_{\;\Psi';\Gamma'}((\sigma; \rho)[\gamma;\tau])
= \boxit {(t^c[\gamma])}
\byIH
\end{align*}

\begin{align*}
\intp{\letbox u s t'}^1_{\;\Psi;\Gamma}(\sigma;\rho)[\gamma;\tau]
&= \intp{t'}^1_{\;\Psi;\Gamma}(\sigma,t^c/u;\rho)[\gamma;\tau] \\
&= \intp{t'}^1_{\;\Psi';\Gamma'}((\sigma,t^c/u;\rho)[\gamma;\tau])
\byIH \\
&= \intp{t'}^1_{\;\Psi';\Gamma'}(\sigma[\gamma],t^c[\gamma]/u;\rho[\gamma;\tau])
\\
&= \intp{\letbox u s t'}^1_{\;\Psi;\Gamma}((\sigma;\rho)[\gamma;\tau])
\end{align*}

* $i = 1$ and $t = \letbox u s t'$ and $\intp{s}^1_{\;\Psi;\Gamma}(\sigma; \rho) = v$.
Then we have

\begin{align*}
\intp{s}^1_{\;\Psi;\Gamma}(\sigma; \rho)[\gamma;\tau]
= \intp{s}^1_{\;\Psi';\Gamma'}((\sigma; \rho)[\gamma;\tau])
= v[\gamma;\tau]
\byIH
\end{align*}

And $(\sigma'; \rho') := (\sigma; \rho)[p(\id); \id]$:

\begin{align*}
& \intp{\letbox u s t'}^1_{\;\Psi;\Gamma}(\sigma;\rho)[\gamma;\tau] \\
=~& \uparrow^{T}_{\;\Psi;\Gamma}(\letbox u v {\downarrow^T_{\;\Psi, u: S;\Gamma}(\intp{t'}^1_{\;\Psi, u:
S;\Gamma}(\sigma', u/u; \rho'))})[\gamma;\tau] \\
=~& \uparrow^{T}_{\;\Psi';\Gamma'}(\letbox u v {\downarrow^T_{\;\Psi, u: S;\Gamma}(\intp{t'}^1_{\;\Psi, u:
S;\Gamma}(\sigma', u/u; \rho'))}[\gamma;\tau])
\tag{naturality of reflection} \\
=~& \uparrow^{T}_{\;\Psi';\Gamma'}(\letbox u {v[\gamma;\tau]} {\downarrow^T_{\;\Psi, u: S;\Gamma}(\intp{t'}^1_{\;\Psi, u:
S;\Gamma}(\sigma', u/u; \rho'))[q(\gamma);\tau]}) \\
=~& \uparrow^{T}_{\;\Psi';\Gamma'}(\letbox u {v[\gamma;\tau]}
{\downarrow^T_{\;\Psi', u: S;\Gamma'}(\intp{t'}^1_{\;\Psi, u:
S;\Gamma}(\sigma', u/u; \rho')[q(\gamma);\tau])})
\tag{naturality of reification} \\
=~& \uparrow^{T}_{\;\Psi';\Gamma'}(\letbox u {v[\gamma;\tau]}
{\downarrow^T_{\;\Psi', u: S;\Gamma'}(\intp{t'}^1_{\;\Psi', u:
S;\Gamma'}((\sigma', u/u; \rho')[q(\gamma);\tau]))})
\byIH \\
=~& \uparrow^{T}_{\;\Psi';\Gamma'}(\letbox u {v[\gamma;\tau]}
{\downarrow^T_{\;\Psi', u: S;\Gamma'}(\intp{t'}^1_{\;\Psi', u:
S;\Gamma'}((\sigma[p(\gamma)], u/u; \rho[p(\gamma);\tau])))}) \\
=~& \uparrow^{T}_{\;\Psi';\Gamma'}(\letbox u {v[\gamma;\tau]}
{\downarrow^T_{\;\Psi', u: S;\Gamma'}(\intp{t'}^1_{\;\Psi', u:
S;\Gamma'}((\sigma[\gamma \circ p(\id)], u/u; \rho[\gamma \circ p(\id);\tau
\circ \id])))}) \\
=~& \uparrow^{T}_{\;\Psi';\Gamma'}(\letbox u {v[\gamma;\tau]}
{\downarrow^T_{\;\Psi', u: S;\Gamma'}(\intp{t'}^1_{\;\Psi', u:
S;\Gamma'}((\sigma[\gamma][p(\id)], u/u; \rho[\gamma; \tau][p(\id);\id])))}) \\
=~& \intp{\letbox u s t'}^1_{\;\Psi';\Gamma'}((\sigma;\rho)[\gamma;\tau])
\end{align*}

We have established the naturality of interpretation.
Next we establish <Ref>.
<Ref> has shown the case where $i = 0$, so we are only
concerned about the case where $i = 1$.
We first work on the following lemma which bridges the interpretation at both layers:
If $\ltyping[\Phi][\Delta] 0 t T$, $\typing[\Psi]\sigma\Phi$, $\gamma : \Psi' \To_g \Psi$ and $\rho \in
\intp{\Delta}_{\;\Psi';\Gamma}$, then
$\intp{t[\sigma]}^0_{\;\Psi';\Gamma}(\gamma; \rho) = \intp{t}^1_{\;\Psi';\Gamma}(\sigma[\gamma]; \rho)$.

We proceed by induction on $\ltyping[\Phi][\Delta] 0 t T$.
We only consider significant cases:

* $t = u$, then

\begin{align*}
\intp{u[\sigma]}^0_{\;\Psi';\Gamma}(\gamma; \rho)
&= \intp{\sigma(u)}^0_{\;\Psi';\Gamma}(\gamma; \rho) \\
&= \intp{\sigma(u)[\gamma]}^0_{\;\Psi';\Gamma}(\id; \rho)
\tag{by \Cref{lem:st:gsubst-nat}} \\
&= \intp{\sigma(u)[\gamma]}^0_{\;\Psi';\Gamma}(\id; *)
\tag{we know $\sigma(u)[\gamma]$ is a closed term} \\
&= \intp{u}^1_{\;\Psi';\Gamma}(\sigma[\gamma]; \rho)
\end{align*}

* $t = x$, then it is immediate because they both look up the same $\rho$.

* $t = \lambda x. t'$, then

\begin{align*}
& \intp{\lambda x. t'[\sigma]}^0_{\;\Psi';\Gamma}(\gamma;\rho) \\
=~& (\gamma';\tau : \Psi'';\Gamma'' \To \Psi';\Gamma)(a) \mapsto
\intp{t'[\sigma]}^0_{\;\Psi'';\Gamma''} (\gamma \circ \gamma';
(\rho[\gamma'; \tau], a)) \\
=~& (\gamma';\tau : \Psi'';\Gamma'' \To \Psi';\Gamma)(a) \mapsto
\intp{t'}^1_{\;\Psi'';\Gamma''} (\sigma[\gamma \circ \gamma'];
(\rho[\gamma'; \tau], a))
\byIH \\
=~& (\gamma';\tau : \Psi'';\Gamma'' \To \Psi';\Gamma)(a) \mapsto
\intp{t'}^1_{\;\Psi'';\Gamma''} (\sigma[\gamma][\gamma'];
(\rho[\gamma'; \tau], a)) \\
=~& \intp{\lambda x. t'}^1_{\;\Psi';\Gamma}(\sigma[\gamma];\rho)
\end{align*}

* $t = t'\ s$, immediate by IH.

If $\ltyping[\Phi][\Delta] 1 t T$, $\typing[\Psi']{\sigma'}\Psi$, $\typing[\Psi]{\sigma}\Phi$ and
$\rho \in \intp{\Delta}_{\;\Psi';\Gamma}$, then
$\intp{t}^1_{\;\Psi';\Gamma}(\sigma \circ \sigma';\rho) = \intp{t[\sigma]}^1_{\;\Psi';\Gamma}(\sigma';\rho)$.

We proceed by induction on $\ltyping[\Phi][\Delta] 1 t T$.
We only consider the cases that are not immediate.

* $t = u$, we compute

\begin{align*}
\intp{u}^1_{\;\Psi';\Gamma}(\sigma \circ \sigma';\rho)
&= \intp{(\sigma \circ \sigma')(u)}^0_{\;\Psi';\Gamma}(\id; *) \\
&= \intp{\sigma(u)[\sigma']}^0_{\;\Psi';\Gamma}(\id; *) \\
&= \intp{\sigma(u)}^1_{\;\Psi';\Gamma}(\sigma';\rho)
\tag{by \Cref{lem:st:intp-0-1}}
\end{align*}

* $t = \boxit t'$, we also compute

\begin{align*}
\intp{\boxit t'}^1_{\;\Psi';\Gamma}(\sigma \circ \sigma';\rho)
&= \boxit {(t'[\sigma \circ \sigma'])} \\
&= \boxit {(t'[\sigma][\sigma'])} \\
&= \intp{\boxit t'[\sigma]}^1_{\;\Psi';\Gamma}(\sigma';\rho)
\end{align*}

* $t = \letbox u s t'$ and assume
$\intp{s}^1_{\;\Psi';\Gamma}(\sigma \circ \sigma'; \rho) = \boxit {t^c}$.
By IH, we have

\begin{align*}
\intp{s}^1_{\;\Psi';\Gamma}(\sigma \circ \sigma'; \rho) = \intp{s[\sigma]}^1_{\;\Psi';\Gamma}(\sigma'; \rho) = \boxit {t^c}
\end{align*}

Then we compute

\begin{align*}
\intp{\letbox u s t'}^1_{\;\Psi';\Gamma}(\sigma \circ \sigma';\rho)
&= \intp{t'}^1_{\;\Psi';\Gamma}((\sigma \circ \sigma'), t^c/u;\rho) \\
&= \intp{t'}^1_{\;\Psi';\Gamma}((\sigma[p(\id)], u/u) \circ (\sigma', t^c/u);\rho) \\
&= \intp{t'[\sigma[p(\id)], u/u]}^1_{\;\Psi';\Gamma}(\sigma', t^c/u;\rho)
\byIH \\
&= \intp{\letbox u s t'[\sigma]}^1_{\;\Psi';\Gamma}(\sigma';\rho)
\end{align*}

We notice that

\begin{align*}
\letbox u s t'[\sigma]
= \letbox u {s[\sigma]} {(t'[\sigma[p(\id)], u/u])}
\end{align*}

* $t = \letbox u s t'$ and assume
$\intp{s}^1_{\;\Psi';\Gamma}(\sigma \circ \sigma'; \rho) = v : \square S$.
By IH, we have

\begin{align*}
\intp{s}^1_{\;\Psi';\Gamma}(\sigma \circ \sigma'; \rho) = \intp{s[\sigma]}^1_{\;\Psi';\Gamma}(\sigma'; \rho) = v : \square S
\end{align*}

Then we compute

\begin{align*}
& \intp{\letbox u s t'}^1_{\;\Psi';\Gamma}(\sigma \circ \sigma';\rho) \\
=~& \uparrow^{T}_{\;\Psi';\Gamma}(\letbox u v {\downarrow^T_{\;\Psi', u: S;\Gamma}(\intp{t}^1_{\;\Psi', u:
S;\Gamma}((\sigma \circ \sigma')[p(\id)], u/u; \rho[p(\id); \id]))}) \\
=~& \uparrow^{T}_{\;\Psi';\Gamma}(\letbox u v {\downarrow^T_{\;\Psi', u: S;\Gamma}(\intp{t}^1_{\;\Psi', u:
S;\Gamma}(\sigma \circ (\sigma'[p(\id)]), u/u; \rho[p(\id); \id]))}) \\
=~& \uparrow^{T}_{\;\Psi';\Gamma}(\letbox u v {\downarrow^T_{\;\Psi', u: S;\Gamma}(\intp{t}^1_{\;\Psi', u:
S;\Gamma}((\sigma, u/u) \circ (\sigma'[p(\id)], u/u); \rho[p(\id); \id]))}) \\
=~& \uparrow^{T}_{\;\Psi';\Gamma}(\letbox u v {\downarrow^T_{\;\Psi', u: S;\Gamma}(\intp{t[\sigma, u/u]}^1_{\;\Psi', u:
S;\Gamma}(\sigma'[p(\id)], u/u; \rho[p(\id); \id]))})
\byIH \\
=~& \intp{\letbox u s t'[\sigma]}^1_{\;\Psi';\Gamma}(\sigma';\rho)
\end{align*}

* $t = \lambda x. t'$, we compute

\begin{align*}
& \intp{\lambda x. t'}^i_{\;\Psi';\Gamma}(\sigma \circ \sigma';\rho) \\
=~& (\gamma;\tau : \Psi'';\Gamma'' \To \Psi';\Gamma)(a) \mapsto
\intp{t'}^i_{\;\Psi'';\Gamma''} ((\sigma \circ \sigma')[\gamma];
(\rho[\gamma; \tau], a)) \\
=~& (\gamma;\tau : \Psi'';\Gamma'' \To \Psi';\Gamma)(a) \mapsto
\intp{t'}^i_{\;\Psi'';\Gamma''} ((\sigma \circ \sigma'[\gamma]);
(\rho[\gamma; \tau], a))
\tag{notice $(\sigma \circ \sigma')[\gamma] = \sigma \circ \sigma'[\gamma]$} \\
=~& (\gamma;\tau : \Psi'';\Gamma'' \To \Psi';\Gamma)(a) \mapsto
\intp{t'[\sigma]}^i_{\;\Psi'';\Gamma''} (\sigma'[\gamma];
(\rho[\gamma; \tau], a))
\byIH \\
=~& \intp{\lambda x. t'[\sigma]}^i_{\;\Psi';\Gamma}(\sigma';\rho)
\end{align*}

§.§ Interactions with Local Substitutions

We have one last theorem remains, which describes the interactions between evaluation
and local substitutions.
A similar proof is done for the presheaf model
in <cit.>, so we only sketch the essence in this

Given $\rho \in \intp{\Delta, \Delta'}_{\;\Psi;\Gamma}$ and
$a \in \intp{T}_{\;\Psi;\Gamma}$, then
$\inser(\rho, \Delta', x, a) \in \intp{\Delta, x : T, \Delta'}_{\;\Psi;\Gamma}$ is defined as

\begin{align*}
\inser(\rho, \cdot, x, a) &:= \rho, a \\
\inser((\rho, b), (\Delta'', y : S), x, a) &:= \inser(\rho, \Delta'', x, a), b
\end{align*}

The $\inser$ function is monotonic w.r.t. weakenings.

$\inser(\rho, \Delta', x, a)[\gamma; \tau] = \inser(\rho[\gamma; \tau], \Delta', x,
a[\gamma; \tau])$

Induction on $\Delta'$.

* $\Delta' = \cdot$, immediate.

* $\Delta' = \Delta'', y : S$,

\begin{align*}
\inser((\rho, b), (\Delta'', y : S), x, a)[\gamma;\tau]
&= (\inser(\rho, \Delta'', x, a), b)[\gamma;\tau] \\
&= \inser(\rho, \Delta'', x, a)[\gamma;\tau], b[\gamma;\tau] \\
&= \inser(\rho[\gamma;\tau], \Delta'', x, a[\gamma;\tau]), b[\gamma;\tau]
\byIH \\
&= \inser(\rho[\gamma;\tau], (\Delta'', y : S), x, a[\gamma;\tau])
\end{align*}

If $\ltyping[\Phi][\Delta, x : S, \Delta'] i t T$ and $\ltyping[\Phi][\Delta,
\Delta'] i s S$, then
$\intp{t[s/x]}^i_{\;\Psi;\Gamma}(\sigma; \rho) = \intp{t}^i_{\;\Psi;\Gamma}(\sigma; \inser(\rho, \Delta', x,
\intp{s}^i_{\;\Psi;\Gamma}(\sigma; \rho)))$

We proceed by induction on $\ltyping[\Phi][\Delta, x : S, \Delta'] i t T$.

* $t = x$, immediate.

* $t = y$ and $x \neq y$, immediate.

* $t = \lambda y : S'. t'$, then

\begin{align*}
& \intp{\lambda y. t'[s/x]}^i_{\;\Psi';\Gamma}(\sigma;\rho) \\
=~& (\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma)(a) \mapsto
\intp{t'[s/x]}^i_{\;\Psi';\Gamma'} (\sigma[\gamma];
(\rho[\gamma; \tau], a)) \\
=~& (\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma)(a) \mapsto
\intp{t'}^i_{\;\Psi';\Gamma'} (\sigma[\gamma];
\inser((\rho[\gamma; \tau], a), (\Delta', y : S'), x, \intp{s}^i_{\;\Psi';\Gamma}(\sigma[\gamma];
(\rho[\gamma; \tau], a))))
\byIH \\
=~& (\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma)(a) \mapsto
\intp{t'}^i_{\;\Psi';\Gamma'} (\sigma[\gamma];
\inser(\rho[\gamma; \tau], \Delta', x, \intp{s}^i_{\;\Psi';\Gamma}(\sigma[\gamma];
(\rho[\gamma; \tau], a))), a) \\
=~& (\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma)(a) \mapsto
\intp{t'}^i_{\;\Psi';\Gamma'} (\sigma[\gamma];
\inser(\rho[\gamma; \tau], \Delta', x, \intp{s}^i_{\;\Psi';\Gamma}((\sigma;
\rho)[\gamma; \tau])), a)
\tag{$s$ was locally weakening when inside of a $\lambda$} \\
=~& (\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma)(a) \mapsto
\intp{t'}^i_{\;\Psi';\Gamma'} (\sigma[\gamma];
\inser(\rho, \Delta', x, \intp{s}^i_{\;\Psi';\Gamma}(\sigma;
\rho))[\gamma; \tau], a)
\tag{monotonicity of $\inser$} \\
=~& \intp{\lambda y. t'}^i_{\;\Psi;\Gamma}(\sigma; \inser(\rho, \Delta', x,
\intp{s}^i(\sigma; \rho)))
\end{align*}

Now we can conclude our target lemma:

Let $\Delta'$ be empty and immediate from the previous lemma.

§.§ Semantic Judgments and Completeness

Now we have established all desired properties of the interpretations.
In this section, we establish <Ref> i.e. the completeness theorem.
In the proof of the completeness theorem, we must establish the relation between
evaluations of two equivalent terms.
Luckily, in the presheaf model, this is very easy and this relation can just be
defined as point-wise equality in the semantics as we will see very soon.
More specifically, the semantic judgments must also be layered due to the behavioral
differences between layers.

0 s T
0 t T

s = t

1 s T
1 t T

∀(σ; ρ) ∈Ψ; Γ^1_ Φ;Δ.
s^1_ Φ;Δ(σ;ρ) = t^1_ Φ;Δ(σ;ρ)

i t T

The semantic equivalence at layer $0$ is straightforward: it simply requires
the terms are syntactically equal.
This makes much sense because terms at layer $0$ are just code and they do not have
At layer $1$, due to dynamics, the semantic equivalence is more typical.
It requires two terms are equal when evaluated in the same environment.
Our target theorem is
thm:st:comp-fund $ $

* If $\ltyping i t T$, then $\lsemtyp i t T$.

* If $\ltyequiv i s t T$, then $\lsemtyeq i s t T$.

The completeness theorem is then a corollary of the fundamental theorem at layer $1$.
Notice that at layer $0$, we do not really have much to do: the layer $0$ only
requires syntactic equality, which we have shown is implied by the syntactic
equivalence judgment.
Therefore, we only focus on layer $1$.

Most PER and congruence rules are immediate because our underlying equivalence in the
semantics is equality.
We will examine a few cases.

§.§.§ Congruence Rules

Assume $(\sigma; \rho) \in \intp{\Psi; \Gamma}^1_{\;\Phi;\Delta}$,
we compute

\begin{align*}
\intp{\boxit t}^1_{\;\Phi;\Delta}(\sigma; \rho)
&= \boxit {(t[\sigma])} \\
\intp{\boxit t'}^1_{\;\Phi;\Delta}(\sigma; \rho)
&= \boxit {(t'[\sigma])}
\end{align*}

Notice $t = t'$ by $\lsemtyeq[\Psi][\cdot]{0}{t}{t'}T$.

\begin{align*}
\intp{\boxit t}^1_{\;\Phi;\Delta}(\sigma; \rho)
= \intp{\boxit t'}^1_{\;\Phi;\Delta}(\sigma; \rho)
\end{align*}

1 ss'□T
[Ψ, u : T] 1 tt'T'
1 u s tus't' T'

Assume $(\sigma; \rho) \in \intp{\Psi; \Gamma}^1_{\;\Phi;\Delta}$,
we have

\begin{align*}
\intp{s}^1_{\;\Phi;\Delta}(\sigma; \rho)
= \intp{s'}^1_{\;\Phi;\Delta}(\sigma; \rho)
\in \intp{\square T}_{\;\Phi;\Delta}
= \Nf^{\square T}_{\;\Phi;\Delta}
\end{align*}

There are two possibilities: either $s$ and $s'$ evaluate to some $\boxit{t^c}$ or
they evaluate to a neutral term $v$.

* $\intp{s}^1_{\;\Phi;\Delta}(\sigma; \rho)
= \intp{s'}^1_{\;\Phi;\Delta}(\sigma; \rho) = \boxit {t^c}$.

Moreover, we have

\begin{align*}
(\sigma, t^c/u; \rho) \in \intp{\Psi, u : T; \Gamma}^1_{\;\Phi;\Delta}
\end{align*}

due to which we have

\begin{align*}
\intp{t}^1_{\;\Phi;\Delta}(\sigma, t^c/u; \rho)
= \intp{t'}^1_{\;\Phi;\Delta}(\sigma, t^c/u; \rho)
\end{align*}

This concludes our first case.

* $\intp{s}^1_{\;\Phi;\Delta}(\sigma; \rho)
= \intp{s'}^1_{\;\Phi;\Delta}(\sigma; \rho) = v$.

\begin{align*}
(\sigma, u/u; \rho) \in \intp{\Psi, u : T; \Gamma}^1_{\;\Phi, u : T;\Delta}
\end{align*}

due to which we have

\begin{align*}
\intp{t}^1_{\;\Phi, u : T;\Delta}(\sigma, u/u; \rho)
= \intp{t'}^1_{\;\Phi, u : T;\Delta}(\sigma, u/u; \rho)
\end{align*}

By congruence, we have

\begin{align*}
\uparrow^{T'}_{\;\Phi;\Delta}(\letbox u v {\downarrow^{T'}_{\;\Phi, u: T;\Delta}(\intp{t}^1_{\;\Phi, u:
T;\Delta}(\sigma, u/u; \rho))})
= \uparrow^{T'}_{\;\Phi;\Delta}(\letbox u v {\downarrow^{T'}_{\;\Phi, u: T;\Delta}(\intp{t'}^1_{\;\Phi, u:
T;\Delta}(\sigma, u/u; \rho))})
\end{align*}

This concludes our goal.

§.§.§ $\beta$ Rules

[Ψ][Γ, x : S] 1 t T
1 s S
1(λx. t) st[s/x]T

Assume $(\sigma; \rho) \in \intp{\Psi; \Gamma}^1_{\;\Phi;\Delta}$,
we have

\begin{align*}
\intp{t}^1_{\;\Phi;\Delta}(\sigma; (\rho, \intp{s}^1_{\;\Phi;\Delta}))
= \intp{t[s/x]}^1_{\;\Phi;\Delta}(\sigma; \rho)
\end{align*}

by <Ref>.

[Ψ][·] 0 s T
[Ψ, u : T] 1 tT'
1 u s tt[s/u]T

Assume $(\sigma; \rho) \in \intp{\Psi; \Gamma}^1_{\;\Phi;\Delta}$,
we have

\begin{align*}
\intp{\letbox u {\boxit s} t}^1_{\;\Phi;\Delta}(\sigma; \rho)
&= \intp{t}^1_{\;\Phi;\Delta}(\sigma, s[\sigma]/u; \rho)
\tag{$s$'s typing suggests that it is a core term} \\
&= \intp{t}^1_{\;\Phi;\Delta}((\id, s/u) \circ \sigma; \rho) \\
&= \intp{t[s/u]}^1_{\;\Phi;\Delta}(\sigma; \rho)
\tag{by~\Cref{lem:st:glob-subst}}
\end{align*}

§.§.§ $\eta$ Rules

1 tS T
1 t λx. (t x)S T

Assume $(\sigma; \rho) \in \intp{\Psi; \Gamma}^1_{\;\Phi;\Delta}$,
we have

\begin{align*}
\intp{\lambda x. t\ x}^1_{\;\Phi;\Delta}(\sigma; \rho)
&= (\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma)(a) \mapsto
\intp{t\ x}^1_{\;\Psi';\Gamma'} (\sigma[\gamma];
(\rho[\gamma; \tau], a)) \\
&= (\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma)(a) \mapsto
\intp{t}^1_{\;\Psi';\Gamma'} (\sigma[\gamma];
(\rho[\gamma; \tau], a), \id, a) \\
&= (\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma)(a) \mapsto
\intp{t}^1_{\;\Psi';\Gamma'} ((\sigma; \rho)[\gamma; \tau], \id, a)
\tag{due to weakening in $t$} \\
&= (\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma)(a) \mapsto
\intp{t}^1_{\;\Psi';\Gamma'} (\sigma; \rho, \gamma; \tau \circ \id, a)
\tag{functoriality of $\intp{t}$} \\
&= (\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma)(a) \mapsto
\intp{t}^1_{\;\Psi';\Gamma'} (\sigma; \rho, \gamma; \tau, a) \\
&= \intp{t}^1_{\;\Phi;\Delta}(\sigma; \rho)
\end{align*}

§.§.§ Completeness

With the semantic judgments verified, we establish the fundamental theorems
This subsequently implies the completeness theorem (<Ref>) because
$\uparrow^{\Psi; \Gamma} \in \intp{\Psi; \Gamma}^1_{\;\Psi;\Gamma}$.

§.§ Soundness

In this section, we show the soundness theorem (<Ref>) of the
normalization algorithm.
In the soundness proof, we use a gluing model, which relates a syntactic term
with a natural transformation in the presheaf model.
For a gluing relation $R$, we write $a \sim b \in R$ to denote $(a, b) \in R$.

It is probably unsurprising that layers play some part in the definition of the gluing
However, it is quite surprising for us how much layers need to participate:
effectively, we have two sets of gluing models to expose the fact that this 2-layered
system effectively contains two languages.
We will see more concretely once we look into the semantic judgments.

§.§.§ Layer-$0$ Gluing Model

In this section, we define the gluing model at layer $0$.
At layer $0$, we only have access to the core types.
This fact is very important when we interpret the types.
We first define the following relation which glues terms and values of natural

1 t
t ∼∈_ Ψ;Γ

1 t t'
t' ∼w ∈_ Ψ;Γ
t ∼w ∈_ Ψ;Γ

1 t v
t ∼v ∈_ Ψ;Γ

$\Nat_{\;\Psi;\Gamma}$ relates a term with a normal form that is of type $\Nat$.
The gluing model at layer $0$ is defined as

\begin{align*}
\glu{T}^0_{\;\Psi;\Gamma} &\subseteq \Exp \times \intp{T}_{\;\Psi;\Gamma} \\
\glu{\Nat}^0_{\;\Psi;\Gamma} &:= \Nat_{\;\Psi;\Gamma} \\
\glu{S \func T}^0_{\;\Psi;\Gamma} &:= \{(t, a) \sep \forall
\gamma; \tau : \Phi; \Delta \To \Psi;\Gamma, s \sim b \in
\glu{S}^0_{\;\Phi;\Delta}. t[\gamma; \tau]\ s \sim a(\gamma; \tau, b) \in
\glu{T}^0_{\;\Phi;\Delta} \}
\end{align*}

Notice that $\glu{T}^0$ does not have a case for $\square$.
We can make sure that $\glu{T}^0$ is well-defined by assuming $\iscore T$ whenever we
refer to the layer-$0$ gluing model.

§.§.§ Properties of Gluing Model at Layer $0$

We need to examine a few properties of the gluing model before proceeding to the
semantic judgments.
Most these proofs are in fact simpler than those
in <cit.> because the $\Nat$ case is defined
through equivalence, so the only case that needs to look into is the function case.

If $t \sim a \in \glu{T}^0_{\;\Psi;\Gamma}$, given $\gamma;\tau : \Phi;\Delta \To \Psi;\Gamma$, then
$t[\gamma;\tau] \sim a[\gamma;\tau] \in \glu{T}^0_{\;\Phi;\Delta}$.

We proceed by induction on $T$.

* $T = \Nat$, immediate by nested induction.

* $T = S \func T'$, then

\begin{align*}
H_1: &\ \ltyping 1{t}{S \func T'} \tag{by assumption} \\
H_2: &\ \forall \gamma'; \tau' : \Phi';\Delta' \To \Psi;\Gamma, s \sim b \in
\glu{S}^0_{\;\Phi';\Delta'}. t[\gamma';\tau']\ s \sim a(\gamma';\tau', b) \in \glu{T'}^0_{\;\vDelta'}
\tag{by assumption} \\
&\ \text{assume }\gamma';\tau' : \Phi';\Delta' \To \Phi;\Delta, s \sim b \in
\glu{S}^0_{\;\Phi';\Delta'} \\
H_3: &\ t[(\gamma;\tau) \circ (\gamma';\tau')]\ s \sim a((\gamma;\tau) \circ (\gamma';\tau'), b) \in
\glu{T'}^0_{\;\Phi';\Delta'}
\tag{by $H_2$} \\
&\ t[\gamma;\tau][\gamma';\tau']\ s \sim a[\gamma;\tau](\gamma';\tau', b) \in
\glu{T'}^0_{\;\Phi';\Delta'} \\
&\ t[\gamma;\tau] \sim a[\gamma;\tau] \in \glu{S \func T'}^0_{\;\Phi;\Delta}
\tag{by abstraction}
\end{align*}

If $t \sim a \in \glu{T}^0_{\;\Psi;\Gamma}$ and
$\ltyequiv 1{t}{t'}{T}$, then $t' \sim a \in \glu{T}^0_{\;\Psi;\Gamma}$.

We prove by induction on $T$.

* $T = \Nat$, immediate by case analysis and then transitivity.

* $T = S \func T'$, then

\begin{align*}
&\ \forall \gamma;\tau : \Phi;\Delta \To \Psi;\Gamma,
s \sim b \in \glu{S}^0_{\;\Phi;\Delta}. t[\gamma;\tau]\ s \sim a(\gamma;\tau,
b) \in \glu{T'}^0_{\;\Phi;\Delta} \tag{by assumption} \\
&\ \text{assume }\gamma;\tau : \Phi;\Delta \To \Psi;\Gamma,
s \sim b \in \glu{S}^0_{\;\Phi;\Delta} \\
&\ \ltyequiv[\Phi][\Delta] 1{t[\gamma;\tau]\ s}{t'[\gamma;\tau]\ s}{T'}
\tag{by congruence} \\
&\ t'[\gamma;\tau]\ s \sim a(\gamma;\tau, b) \in \glu{T'}^0_{\;\Phi;\Delta}
\byIH \\
&\ t' \sim a \in \glu{S \func T'}^0_{\;\Psi;\Gamma}
\end{align*}

Next we show that if $t$ and $a$ are related, then $t$ is equivalent to $a$'s
This lemma needs to be proved mutually with two lemmas:
If $\ltyping 0 v T$, then $v \sim \uparrow^T_{\;\Psi;\Gamma}(v) \in
\glu{T}^0_{\;\Psi;\Gamma}$.

If $t \sim a \in \glu{T}^0_{\;\Psi;\Gamma}$, then
$\ltyequiv 1{t}{\downarrow^T_{\;\Psi;\Gamma}(a)}{T}$.

We proceed by induction on $T$.

* $T= \Nat$, immediate.

* $T = S \func T'$, then assume $\gamma;\tau : \Phi;\Delta \To \Psi;\Gamma$ and $s \sim b \in
\glu{S}^0_{\;\Phi;\Delta}$,

\begin{align*}
\uparrow^{S \func T'}_{\;\Psi;\Gamma}(v)(\gamma;\tau, b)
&= \uparrow^{T'}_{\;\Phi;\Delta}(v[\gamma;\tau]\ \downarrow^S_{\;\Phi;\Delta}(b))
\end{align*}

By IH, we have

\begin{align*}
v[\gamma;\tau]\ \downarrow^S_{\;\Phi;\Delta}(b) \sim \uparrow^{T'}_{\;\Phi;\Delta}(v[\gamma;\tau]\
\downarrow^S_{\;\Phi;\Delta}(b))
\in \glu{T'}^0_{\;\Phi;\Delta}
\end{align*}

We further obtain from <Ref> (IH)

\begin{align*}
v[\gamma;\tau]\ s \sim \uparrow^{S \func T'}_{\;\Psi;\Gamma}(v)(\gamma;\tau, b)
\in \glu{T'}^0_{\;\Phi;\Delta}
\end{align*}

Therefore $v \sim \uparrow^{S \func T'}_{\;\Psi;\Gamma}(v) \in \glu{S \func T'}^0_{\;\Psi;\Gamma}$.

We proceed by induction on $T$.

* $T = \Nat$, immediate.

* $T = S \func T'$, then

\begin{align*}
H_2: &\ \forall \gamma;\tau : \Phi;\Delta \To \Psi;\Gamma,
s \sim b \in \glu{S}^0_{\;\Phi;\Delta}. t[\gamma;\tau]\ s \sim a(\gamma;\tau,
b) \in \glu{T'}^0_{\;\Phi;\Delta} \tag{by assumption} \\
&\ x \sim \uparrow^S_{\Psi; (\Gamma, x : S)}(x) \in \intp{S}_{\Psi; (\Gamma, x : S)}
\tag{by \Cref{lem:st:ne-glue} (IH)} \\
&\ t[\id;p(\id)]\ x \sim a(\id;p(\id), \uparrow^S_{\Psi; (\Gamma, x : S)}(x)) \in
\glu{T'}^0_{\Psi; (\Gamma, x : S)}
\tag{by $H_2$ and let $\gamma;\tau$ be $\id;p(\id) : \Psi; (\Gamma, x
: S) \To \Psi; \Gamma$} \\
&\ \ltyequiv[\Psi][(\Gamma, x : S)] 1{t\ x}{\downarrow^{T'}_{\Psi;
(\Gamma, x : S)}(a(\id;p(\id), \uparrow^S_{\Psi; (\Gamma, x
: S)}(x)))}{T'}
\byIH \\
&\ \ltyequiv 1{\lambda x.t\ x}
{\lambda x.\downarrow^{T'}_{\Psi;
(\Gamma, x : S)}(a(\id;p(\id), \uparrow^S_{\Psi; (\Gamma, x
: S)}(x)))}{S \func T'}
\tag{by congruence} \\
&\ \ltyequiv 1{t}
{\lambda x.\downarrow^{T'}_{\Psi;
(\Gamma, x : S)}(a(\id;p(\id), \uparrow^S_{\Psi; (\Gamma, x
: S)}(x)))}{S \func T'}
\tag{by $\eta$ and transitivity}
\end{align*}

§.§.§ Semantic Judgments at Layer $0$

We are about to define the semantic judgments at layer $0$.
Before that, we first generalize the gluing of types to
local contexts.
Notice that this generalization is also layered and assumes $\iscore \Delta$.

\begin{align*}
\glu{\Delta}^0_{\;\Psi;\Gamma} &\subseteq (\dtyping \delta \Delta) \times \intp{\Delta}_{\;\Psi;\Gamma} \\
\glu{\cdot}^0_{\;\Psi;\Gamma} &:= \{(\cdot, *)\} \\
\glu{\Delta, x : T}^0_{\;\Psi;\Gamma} &:= \{ ((\delta, t/x), (\rho, a)) \sep \delta \sim \rho \in \glu{\Delta}^0_{\;\Psi;\Gamma}
\tand t \sim a \in \glu{T}^0_{\;\Psi;\Gamma} \}
\end{align*}

Then monotonicity also generalizes to local contexts:
If $\delta \sim \rho \in \glu{\Delta}^0_{\;\Psi;\Gamma}$, given $\gamma;\tau : \Phi;\Delta' \To
\Psi;\Gamma$,  then
$\delta[\gamma;\tau] \sim \rho[\gamma;\tau] \in \glu{\Delta}^0_{\;\Phi;\Delta'}$.

Immediate by induction on $\Delta$ and <Ref>.

Finally, we can define the judgments:

We define the semantic judgment for typing and global substitutions:

\begin{align*}
\lSemtyp 0 t T &:= \forall \gamma : \Phi \To_g \Psi \tand \delta \sim \rho \in
\glu{\Gamma}^0_{\;\Phi;\Delta}. t[\gamma][\delta] \sim
\intp{t}^0_{\;\Phi;\Delta}(\gamma;\rho) \in
\glu{T}^0_{\;\Phi;\Delta}
\end{align*}

[Ψ][·] 0 tT
[Ψ]σ, t/uΦ, u : T

We can recover the syntactic judgment for global substitutions from the semantic judgment:

If $\Semtyp[\Psi]{\sigma}{\Phi}$, then $\typing[\Psi]{\sigma}{\Phi}$.

If $\lSemtyp[\Psi] 0 {t}{T}$ and $\gamma : \Psi' \To_g \Psi$, then
$\lSemtyp[\Psi'] 0 {t[\gamma]}{T}$.

immediate by composition of global weakenings.

If $\Semtyp[\Psi]{\sigma}{\Phi}$ and $\gamma : \Psi' \To_g \Psi$, then

Induction and use monotonicity of the semantic typing at layer $0$.

The semantic typing judgment is also split into two layers.
The global substitution judgment is a generalization of the semantic judgment at layer
$0$, which will be used to define the semantic judgment at layer $1$.
However, before doing that, we must first give the layer-$1$ gluing model.

§.§.§ Layer-$1$ Gluing Model

Unlike all previous layered definitions, where we can more or less let the definition
parameterized by the layer, in this layered gluing model, we can see that this 2-layered
modal type theory effectively operates on two different languages.
Specifically our layer-$1$ model actually relies on the layer-$0$ semantic judgment,
and thus we have this incredibly long detour to arrive at the final definition.
We refer to the layer-$0$ semantic judgment when we define the semantic for $\square$:

1 tt^c□T
[Ψ][·] 0 t^c T
t ∼t^c ∈□T_ Ψ;Γ

1 t v□T
t ∼v ∈□T_ Ψ;Γ

There are two ways for $\square T$ to relate a term and a value.
The first case is the more interesting one.
When we know $t$ is related to $\boxit {t^c}$, we must be aware of the fact that it is
also a well-typed term in the semantics.
This information is necessary when we prove the semantic rule for $\tletbox$.
Now we give the gluing model at layer $1$:

\begin{align*}
\glu{T}^1_{\;\Psi;\Gamma} &\subseteq \Exp \times \intp{T}_{\;\Psi;\Gamma} \\
\glu{\Nat}^1_{\;\Psi;\Gamma} &:= \Nat_{\;\Psi;\Gamma} \\
\glu{\square T}^1_{\;\Psi;\Gamma} &:= {\square T}_{\;\Psi;\Gamma} \\
\glu{S \func T}^1_{\;\Psi;\Gamma} &:= \{(t, a) \sep \forall
\gamma; \tau : \Phi; \Delta \To \Psi;\Gamma, s \sim b \in
\glu{S}^1_{\;\Phi;\Delta}. t[\gamma; \tau]\ s \sim a(\gamma; \tau, b) \in
\glu{T}^1_{\;\Phi;\Delta} \}
\end{align*}

A few previous properties for the layer-$0$ gluing model continue to hold for the
layer-$1$ model,
e.g. <Ref>, with
layer changed from $0$ to $1$ appropriately.
In fact, $\glu{T}^0$ is subsumed by $\glu{T}^1$:
If $\iscore T$, then $\glu{T}^0_{\;\Psi;\Gamma} = \glu{T}^1_{\;\Psi;\Gamma}$.

Induction on $\iscore T$.

This lemma states that if we do not use $\square$ types, then our programs essentially
are just running in simply typed $\lambda$-calculus, so $\square$ types are the
only addition we get by operating at layer $1$.

With the gluing model, we can define the generalization of the gluing model to local
contexts and the semantic judgment:

\begin{align*}
\glu{\Delta}^1_{\;\Psi;\Gamma} &\subseteq (\dtyping \delta \Delta) \times \intp{\Delta}_{\;\Psi;\Gamma} \\
\glu{\cdot}^1_{\;\Psi;\Gamma} &:= \{(\cdot, *)\} \\
\glu{\Delta, x : T}^1_{\;\Psi;\Gamma} &:= \{ ((\delta, t/x), (\rho, a)) \sep \delta \sim \rho \in \glu{\Delta}_{\;\Psi;\Gamma}
\tand t \sim a \in \glu{T}^1_{\;\Psi;\Gamma} \}
\end{align*}

\begin{align*}
\lSemtyp 1 t T &:= \forall \Semtyp[\Phi]\sigma\Psi \tand \delta \sim \rho \in
\glu{\Gamma}^1_{\;\Phi;\Delta}. t[\sigma;\delta] \sim \intp{t}^1_{\;\Phi;\Delta}(\sigma;\rho) \in \glu{T}^1_{\;\Phi;\Delta}
\end{align*}

Notice that the semantic judgment at layer $1$ universally quantifies over a semantic
judgment of global substitutions.
This quantification informs us that terms in the substitutions are semantically
well-typed at layer $0$, hence necessary for the rule of global variables.

§.§.§ Semantic Rules

We examine all the semantic judgments:

u : T ∈Ψ

u : T ∈Ψ

We consider each rule by $i$.

* $i = 0$, then we assume $\gamma : \Phi \To_g \Psi$ and
$\delta \sim \rho \in \glu{\Gamma}^0_{\;\Phi;\Delta}$.
We should prove

\begin{align*}
u[\gamma] \sim \intp{u}^0_{\;\Phi;\Delta}(\gamma; \rho) \in \glu{T}^0_{\;\Phi;\Delta}
\end{align*}

But we know

\begin{align*}
\intp{u}^0_{\;\Phi;\Delta}(\gamma; \rho)
= \uparrow^{T}_{\;\Phi; \Delta}(u[\gamma])
\end{align*}

and thus the goal holds by <Ref>.

* $i = 1$. then we assume $\Semtyp[\Phi]\sigma\Psi$ and
$\delta \sim \rho \in \glu{\Gamma}^1_{\;\Phi;\Delta}$.
Then we should prove

\begin{align*}
\sigma(u) \sim \intp{\sigma(u)}^0_{\;\Phi;\Delta}(\id; *) \in
\glu{T}^0_{\;\Phi;\Delta} = \glu{T}^1_{\;\Phi;\Delta}
\tag{by \Cref{lem:st:glu-0-to-1}}
\end{align*}

By $\sigma(u)$'s typing judgment, we know it is closed

\begin{align*}
\sigma(u) \sim \intp{\sigma(u)}^1_{\;\Phi;\cdot}(\id; *) \in \glu{T}^0_{\;\Phi;\cdot}
\end{align*}

We get this from the semantic judgment $\lSemtyp[\Phi][\cdot] 0{\sigma(u)}{T}$.

x : T ∈Γ

x : T ∈Γ

These two rules are immediate because they simply lookup the evaluation environment
which maintains the gluing relation.

[Ψ][Γ, x : S]itT
iλx. tS T

We only consider the case where $i = 1$ because the case of $i = 0$ is the same.
Assume $\Semtyp[\Phi]\sigma\Psi$,
$\delta \sim \rho \in \glu{\Gamma}^1_{\;\Phi;\Delta}$,
$\gamma; \tau : \Phi'; \Delta' \To \Phi; \Delta$ and
$s \sim b \in \glu{S}^1_{\;\Phi';\Delta'}$
Then we should prove that

\begin{align*}
(\lambda x. (t[\sigma; (\delta[p(\id)], x/x)][\gamma; q(\tau)]))\ s \sim
\intp{t}^1_{\;\Phi';\Delta'}(\sigma[\gamma];(\rho[\gamma;\tau], b)) \in \glu{T}^1_{\;\Phi';\Delta'}
\end{align*}

We need to construct $\glu{\Gamma, x : S}^1_{\;\Phi';\Delta'}$ from what we have. We

\begin{align*}
(\delta[\gamma;\tau], s/x) \sim (\rho[\gamma;\tau], b) \in \glu{\Gamma, x : S}^1_{\;\Phi';\Delta'}
\end{align*}

because $\delta[\gamma;\tau] \sim \rho[\gamma;\tau] \in \glu{\Gamma}^1_{\;\Phi';\Delta'}$
by <Ref>. Therefore

\begin{align*}
t[\sigma; (\delta[\gamma;\tau], s/x)] \sim \intp{t}^1_{\;\Phi';\Delta'}(\sigma;
(\rho[\gamma;\tau], b)) \in \glu{T}^1_{\;\Phi';\Delta'}
\end{align*}

Comparing the goal and what we have, we use <Ref> at layer
$1$ to $\beta$ reduce the left hand side and achieve our goal.

itS T
it sT

Immediate by applying the premises.

Finally, we consider the modal components.
Recall that they only live at layer $1$.

[Ψ][·] 0 t T

Assume $\Semtyp[\Phi]\sigma\Psi$,
$\delta \sim \rho \in \glu{\Gamma}_{\;\Phi;\Delta}$.
Then we should prove

\begin{align*}
\boxit {(t[\sigma])} \sim \boxit {(t[\sigma])} \in \glu{\square T}^1_{\;\Phi;\Delta}
\end{align*}

This holds by reflexivity and the definition of the gluing model.
Notice that $\lSemtyp[\Psi][\cdot] 0 t T$ is remembered by the gluing model of
$\glu{\square T}$.

1 s□T
[Ψ, u : T] 1 tT'
1 u s t T'

Assume $\Semtyp[\Phi]\sigma\Psi$,
$\delta \sim \rho \in \glu{\Gamma}_{\;\Phi;\Delta}$.
Then we know

\begin{align*}
s[\sigma;\delta] \sim \intp{s}^1_{\;\Phi;\Delta}(\sigma;\rho) \in \glu{\square T}^1_{\;\Phi;\Delta}
\end{align*}

There are two ways that this can hold:

* $\intp{s}^1_{\;\Phi;\Delta}(\sigma;\rho) = \boxit{t^c}$ and we know $\lSemtyp[\Psi][\cdot]
0 {t^c} T$.
Then we have

\begin{align*}
& \Semtyp[\Phi]{\sigma, t^c/u}{\Psi, u : T} \\
& t[\sigma,t^c/u;\delta] \sim \intp{t}^1_{\;\Phi;\Delta}((\sigma,t^c/u);\rho)
\in \glu{T'}^1_{\;\Phi;\Delta}
\tag{from premise}
\end{align*}

We have the goal by <Ref> and perform $\beta$ reduction on
the left.

* $\intp{s}^1_{\;\Phi;\Delta}(\sigma;\rho) = v$ for some neutral $v$ and we know
$H1: \ltyequiv[\Phi][\Delta] 1{s[\sigma;\delta]}{v}{\square T}$.

\begin{align*}
& u \sim \uparrow^T_{\;\Psi;u:T;\cdot}(u) \in \glu{T}^0_{\;\Psi;u:T;\cdot}
\tag{by \Cref{lem:st:ne-glue}} \\
& \lSemtyp[\Phi, u : T][\cdot] 0 {u} T
\tag{by monotonicity} \\
& \Semtyp[\Phi, u : T]{\sigma[p(\id)], u/u}{\Psi, u : T}
\tag{by monotonicity} \\
& t[(\sigma[p(\id)], u/u); \delta[p(\id);\id]]
\sim \intp{t}^1_{\;\Phi, u : T;\Delta}((\sigma[p(\id)], u/u);
\rho[p(\id);\id])
\in \glu{T'}^1_{\;\Phi, u : T;\Delta}
\tag{by premise} \\
H2:\ & \ltyequiv[\Phi; u : T] [\Delta] 1 {t[(\sigma[p(\id)], u/u);
\delta[p(\id);\id]]}
{\downarrow^{T'}_{\;\Phi, u : T;\Delta}(\intp{t}^1_{\;\Phi, u : T;\Delta}((\sigma[p(\id)], u/u);
\rho[p(\id);\id]))}{T'}
\tag{by \Cref{lem:st:glue-nf}}
\end{align*}

We let $E := \letbox u v {\downarrow^{T'}_{\;\Phi, u : T;\Delta}(\intp{t}^1_{\;\Phi, u : T;\Delta}((\sigma[p(\id)], u/u);
\rho[p(\id);\id]))}$ and notice that $E$ is neutral and well-typed.
By <Ref>, we have

\begin{align*}
E \sim \uparrow^{T'}_{\;\Phi;\Delta}(E) \in \glu{T'}^1_{\;\Phi;\Delta}
\end{align*}

From $H1$ and $H2$, we have

\begin{align*}
\ltyequiv[\Phi][\Delta] 1 {\letbox u s t [\sigma;\delta]}{E}{T'}
\end{align*}

from which we obtain our goal via <Ref>.

Now we have finished all the semantic rules.

§.§.§ Fundamental Theorems and Soundness

$ $
If $\ltyping i t T$, then $\lSemtyp i t T$.

We would like to extract the soundness proof by setting $i = 1$.
After that we need to also make sure we can eliminate the universal quantifications.

Use the semantic rule for global variables at layer $0$.

$\id \sim \uparrow^{\Gamma} \in \glu{\Gamma}^1_{\;\Psi;\Gamma}$

Apply <Ref> for local variables.

This concludes our soundness proof.

From the fundamental theorems, we have $\lSemtyp i t T$, and then due to the
previous two lemmas
$t \sim \intp{t}^1_{\;\Psi;\Gamma}(\uparrow^{\Psi;\Gamma}) \in
\glu{T}^1_{\;\Psi;\Gamma}$.
We get the goal by <Ref>.

At this point, we have shown the completeness and soundness of the NbE algorithm.

§ LAYERED CONTEXTUAL MODAL TYPE THEORY

In the previous sections, we have developed layered modal type theory and its
normalization by evaluation proof using a presheaf model.
Though our semantics already supports certain code inspection operations, these
operations can only handle closed code.
This problem has already been addressed by contextual types proposed
by <cit.>.
Instead of clearing out all local assumptions in the $\square$ introduction rule,
contextual types allow to specify local assumptions that can be depended on.
To support full case analysis on code, we introduce contextual types to our 2-layered
modal type theory, forming layered contextual modal type theory.
In this section, we adapt our previous development to contextual types and pattern
matching, and in the next section, we adapt our previous NbE proof to show that with
contextual types, the type theory remains normalizing.

§.§ Examples

As briefly discussed in the previous section, we can support an construct,
which branches based on whether the received argument is a code of function
application or not.
This construct can be implemented by a more general pattern matching construct, which
branches into multiple cases based on a code like this:

\begin{align*}
& \matc t \\
& |\; ?u~?u' \STo \cdots \\
& |\; \su ?u \STo \cdots \\
& |\; \_ \STo \cdots
\end{align*}

A pattern variable $u$ following a question mark captures a code in a pattern.
This style might have received some influence from Ltac, the tactic language in Coq.
In this example, the first pattern matches a function application.
We use $u$ for the code of the function and $u'$ for the code of the argument.
If $t$ is a code of function application, then we fall into this case and execute the
body, which potentially uses $u$ and $u'$.
In the second branch, the pattern matches a successor and use $u$ to capture the code
of the predecessor.
At last, we use a wildcard to capture all remaining cases, which includes cases like
$\ze$ or variable $x$.

Depending on the type of $t$, we know ahead of time that certain branches are not
For example, if $t$ has type $\square \Nat$, then we know it cannot be introduced by a
$\lambda$ abstraction.
In this case, we cannot match it against a pattern of $\lambda$.
Similarly, if $t$ is a code of a function type, then both $\ze$ and $\su$ cases are
not possible and therefore these cases cannot exist.
Though it is possible to know ahead of time when an introduction is not possible,
elimination forms are always possible.
Function applications can return any type as long as it is the return type of a

To confess, in the previous discussion, we omit one detail: if we allow pattern of the form
$\lambda x. ?u$, what should be the type of $u$?
Clearly it is not closed because $u$ can at least refer to $x$.
This is when contextual types becomes useful.
If $t$ is a closed code of a function and of type $\square (S \func T)$.
Then its function body behind a $\lambda$ abstraction should have type $\cont[x :
The $x : S$ to the left of the turnstile denotes the open context the underlying term
is open with respect to.
In general, this context can be arbitrarily long.
Consider the following pattern matching, where $t$ has type $\cont{S \func T}$:

\begin{align*}
& \matc t \\
& |\; \lambda x. ?u \STo (\matc {\boxit u} \sep ?u'~?u'' \STo \cdots \sep \_ \STo \cdots) \\
& |\; \_ \STo \cdots
\end{align*}

In this pattern matching, we first test whether $t$ is a $\lambda$ abstraction.
If it is the case, we use $u$ to capture the code of the body, which has type
$\cont[\Gamma, x : S] T$.
Then we use another pattern matching to test whether $u$ is a function application or
The context in the type grows due to $\lambda$, while function applications do not
introduce new binder, so the context of $u'$ and $u''$ does not grow.

§.§ Syntax and Typing Judgments

Following the same principle as in <Ref>, we define the syntax of the type
theory as follows:

S, T    :=       T S T

Γ, Δ   :=        ·Γ, x : T
Local contexts

δ   :=       ·δ, t/x Local substitutions

s, t    :=       x u^δTerms, $\Exp$

natural numbers

t u s t t

λx. t s t functions

:=        x t t ?u t λx. ?u t
?u ?u' t

Φ, Ψ   :=        ·Φ, u : (T)
Global contexts

Instead of $\square T$, we now use $\cont T$, contextual types, to represent the type
of code.
The local context $\Gamma$ in $\cont T$ is the open variables that can be used to
construct a code of $T$.
We let $\square T := \cont[\cdot] T$ to recover the previous $\square$ type.
To introduce a contextual type, we use $\boxit t$ where $t$ is the potentially open
For elimination, in addition to $\tletbox$, we use the pattern matching construct that
we introduced in the previous example section.
There are only five possible patterns in a pattern matching, each representing one
possible syntax in the core type theory.
These five cases are exhaustive already due to the layered nature of our type theory:
it is not possible to refer to modal components at layer $0$, which is guaranteed by
our typing judgments.
In reality, the branches of a well-typed pattern matching expression must be less than
five because we forbid incompatible introduction forms according to the type
information as explained in the previous example section.
Finally, we do not support nested patterns like $\lambda x. ?u~?u'$ in our language.
Fortunately, all nested patterns can be converted into nested pattern matchings as we
did in a previous example.

Due to the introduction of local contexts in the $\square$ types, our global contexts
deviate from the previous form, having to also keep track of a local context for each
Because of this extra local context, we can no longer simply refer to a global
variable $u$.
Instead, we must specify how this local context is filled in using a local
substitution $\delta$.
When $u$ is being substituted, we also need to apply this local substitution to obtain
a well-typed term in the current context.
Before capturing the intuitions formally using typing judgments, we also need two
predicates on types as in <Ref> to classify types in the core type theory and
those in the extended type theory.
Since our core type theory remains the same, the predicate $\iscore T$ is also
When we write the generalization $\iscore \Phi$, we mean that all types occurring in
$\Phi$ including those in respective local contexts are core types.
We only need to amend the predicate $\istype T$:

S T

In the case of contextual types, we require $\iscore \Gamma$, because $\cont T$
represents an open code in the core type theory, so $\Gamma$ must not have
access to another contextual type.
$\istype \Gamma$ is the natural generalization of $\istype T$, which is used at layer
$1$ to describe the local contexts.

Next we give the typing judgments.
There are four kinds of typing judgments in the contextual system.
$\ltyping i t T$ is the usual typing judgment for terms.
$\ltyping i \delta \Delta$ is the typing judgment for local substitutions.
$\ltyping 1 \branch {\judge[\Delta] T \STo T'}$ is the typing judgment for pattern $\branch$
knowing that the type of the scrutinee is $\cont[\Delta] T$ and the return type is
Last, $\ltyping 1{\vect\branch}{\judge[\Delta] T \STo T'}$ is a generalization of
$\ltyping 1 \branch {\judge[\Delta] T \STo T'}$ and the covering judgment for all branches of a
pattern matching expression.
We only show the modal rules because they are the only changed rules:

[Ψ][Δ] 0 t T
1t[Δ] T

1 s[Δ] T
1 [Δ] T T'
1 s  T'

0 ··

1 ··

i δΔ
i tT
i δ, t/xΔ, x : T

i δΔ
u : ([Δ] T) ∈Ψ

In the rule for pattern matching, we need typing rules for all branches:

1 t T'
1 x t[Δ] T T'

1 t T'
1 t[Δ] T'

[Ψ, u : ([Δ])] 1 t T'
1 ?u t[Δ] T'

[Ψ, u : ([Δ, x : S]T)] 1 t T'
1 λx. ?u t[Δ] S T T'

∀S.  [Ψ, u : ([Δ]S T), u' : ([Δ]S)] 1 t T'
1 ?u ?u' t[Δ] T T'

At last, $\ltyping 1 {\vect \branch}{\judge[\Delta] T \STo T'}$ includes all
compatible rules from the $\ltyping 1 \branch {\judge[\Delta] T \STo T'}$ judgment
above according to $T$.
We write $\vect\branch(t)$ for the lookup of a branch.
For example, $\vect\branch(t~s)$ returns a branch $?u~?u' \STo t'$ in $\vect\branch$ because
$t~s$ is a function application.
We use the typing information to ensure this lookup is only performed legally.

Many rules just generalize their previous corresponding rules.
In the introduction rule for $\square$, $t$ is typed with $\Delta$ instead of an empty
local context.
When we refer to $u$, we need to specify a local substitution, so we must also move
the judgment for local substitutions up earlier than before.
Notice that now we also distinguish local substitutions by layers, as opposed to
before, where local substitutions only live at layer $1$.
When we refer to $u$ at layer $0$, $u$ effectively is a slot waiting to be substituted
by an open code at layer $0$.
Therefore, the local substitution $\delta$ for the open variables must only contain
code at layer $0$ as well.
When we refer to $u$ at layer $1$, we are evaluating or embedding the code represented
by $u$ in the extended type theory.
Since we are operating at layer $1$, it does no harm to let the terms in $\delta$ to
also live at layer $1$.
In this case, due to the confluence property of the system, contextual types behave no
differently from functions.
In the special case where $\delta$ is the identity local substitution, we very often
omit it for brevity, i.e. $u^\id = u$.

At last we have the elimination rule using pattern matching.
After typing the scrutinee $s$, we also need to type all branches.
What branches are possible depends on $T$.
As explained before, there are impossible cases in $\vect\branch$ based
on $T$.
The typing judgment requires $\vect\branch$ to contain all possible branches.
For each branch, we proceed as expected, and push global variables to the global
context as needed when code is captured by pattern variables.
The judgment for all branches $\ltyping 1 {\vect \branch}{\judge[\Delta] T \STo T'}$
is defined as:

∀b ∈ .  1 [Δ] T'

_= t  for some  t

_= ?u t  for some  t

_= ?u ?u' t  for some  t

∀x : ∈Δ .  b_x = x t  for some  t

is a permutation of  { _, _,

_, _x  for all  x : ∈Δ}
1[Δ] T'

∀b ∈ .  1 [Δ] S T T'

_λ= λx. ?u t  for some  t

_= ?u ?u' t  for some  t

∀x : S T ∈Δ .  b_x = x t  for some  t

is a permutation of  { _λ,

_, _x  for all  x : S T ∈Δ}
1[Δ] S T T'

There are two issues worth noting in the typing of pattern matching.
The first one is the case of function applications.
The premise is a universal quantification over all possible $\iscore S$.
This is necessary due to the lack of expressive power of our simple type system.
In a function application, the argument type is hidden and we can not learn it from
the return type.
In order to make sure the body is well-typed for all argument types, we effectively
introduce certain parametricity in the meta-theory to ensure that $t$ is oblivious to
the concrete argument type $S$ given $\iscore S$.
This treatment only exists due to simple types.
With strong type systems, e.g. System F-style type variables or dependent types, this
issue can be handled by unification or other methods, c.f. <cit.>.

The second problem is the lack of recursion on code.
Indeed, the type theory we are presenting now cannot define a recursive function on
code structure.
This is, again, because of our simple type system.
Consider a possible recursive operation which inspects a code and recurses on the
code of the function if the scrutinee is a function application.
This operation is not definable in our current type theory because the type of code
has changed.
If the original scrutinee has type $\cont[\Delta] T$, then the recursive call is on a
term of type $\cont[\Delta]{S \func T}$ for some $S$.
Nevertheless, the semantics is ready for recursion on code.
With stronger types, this feature becomes possible, and indeed we will support it when
we adapt our layered modal type theory to dependent types.

§.§ Neutral Forms and Equivalence Rules

Inheriting the previous development, our equivalence rules are also layered.
The same as before, we have PER rules, congruence rules, $\beta$ rules and $\eta$
The PER and $\eta$ rules stay the same so we omit them here.
The congruence rules are simply derived from the typing judgments above, so we also
omit most of them here.
The congruence rules for local substitutions are:

0 Ψ
i Γ
i ···

i δδ'Δ
i tt'T
i δ, t/xδ', t'/xΔ, x : T

In this rule, the equivalence relation simply propagates down recursively.
Yet, depending on $i$, this rule behaves differently.
At layer $0$, since all terms are identified by their syntactic structures,
equivalence between local substitutions also implies identical syntax.
However, at layer $1$, due to dynamics, we allow all terms inside to reduce or expand

The following are the $\beta$ rules for pattern matching on contextual types.
The rules are very intuitive, as they simply look up the branches according to
the code and perform reduction accordingly:

i δδ' Δ
u : ([Δ] T) ∈Ψ

x : T ∈Δ
1 [Δ] T T'

(x) = x t
1 x t T'

1 [Δ] T'

() = t
1  t T'

[Ψ][Δ] 0 s
1 [Δ] T'

(s) = ?u t
1 (s) t[s/u]T'

[Ψ][Δ, x : S] 0 s T
1 [Δ] S T T'
(λx. s) = λx. ?u t
1 (λx. s) t[s/u]T'

[Ψ][Δ] 0 tS T
[Ψ][Δ] 0 s S

1 [Δ] T T'

(t s) = ?u ?u' t
1 (t s) t[t/u, s/u']T'

Here we rely on global substitutions which are about to be defined, but otherwise the
$\beta$ rules should follow intuition very closely.
However, there is one tiny detail lying in this set of rules which might be difficult
to notice at the first glance: what if we match against a global variable, i.e. what
$\matc {\boxit{u^\delta}}\ \vect\branch$ should be reduced to?

This problem is raised by <cit.>, where the author points
out that one example for the $\tisapp$ function by <cit.>
seems to break confluence:

\begin{align*}
\letbox u {\boxit{(t~s)}} {\tisapp~(\boxit{u})}
\end{align*}

In our settings, we would use pattern matching to implement the $\tisapp$ function.
Then <cit.> points out two possible equivalence chains:

\begin{align*}
\letbox u {\boxit{(t~s)}} {\tisapp~(\boxit{u})}
\approx \tisapp~(\boxit{(t~s)})
\approx \tru
\end{align*}

There is another chain:

\begin{align*}
\letbox u {\boxit{(t~s)}} {\tisapp~(\boxit{u})}
\approx \letbox u {\boxit{(t~s)}}\fal
\approx \fal
\end{align*}

The first equivalence makes more sense and is expected, so let us look into why the
second case goes wrong.
It appears that in the second case, $\tisapp~(\boxit u)$ reduces to $\fal$, which
voids the later substitution of $t~s$ for $u$.
Though there could be problems in <cit.> that exhibit this
issue, in our settings, $\tisapp~(\boxit{u}) \approx \fal$ would correspond to that
global variables have their own branch in a pattern matching, which returns .
This, however, is not the case in our system.
In fact, in our system, $\matc {\boxit {u^\delta}} \ \vect\branch$ is blocked and
considered neutral.
This choice is the same as considering $\matc x \ \vect\branch$ neutral, as they are both
waiting for a substitution to supply an actual input for the computation to continue.
The only difference is that $\matc x \ \vect\branch$ is waiting for a local substitution
that could give $\tbox$ of some open code, while $\matc {\boxit {u^\delta}} \ \vect\branch$
is waiting for a global substitution that actually supplies the code for $u$.
Therefore, by adding pattern matching as an elimination form, we in
fact need to change our definition of neutral forms in a slightly surprising way:

v    :=        x u^θv w u v w v  u^δ  Neutral form

:=         x w w ?u w λx. ?u w
?u ?u' w
Normal branches

θ    :=        ·θ, w/x
Normal local substitutions

The definition of normal form stays the same as before.
This definition of neutral forms also implies that $\tletbox$ in fact cannot be
faithfully encoded by pattern matching.
If we define

\begin{align*}
\letbox u s t := \matc {s} \sep ?u \STo t
\end{align*}

namely letting bodies of all branches be $t$, this encoding will not behave the same as the
original $\tletbox$.
When $s$ is some $\boxit{u'}$, the original $\tletbox$ will reduce and substitute $u'$
for $u$, while with this encoding, the evaluation will get stuck.

Due to this difference in computational behavior, we let both elimination forms to
In our layered view of type theory, this is perfectly fine because our core theory is
Coexistence only enriches the extended type theory.
We use $\tletbox$ primarily for the execution and the composition of code and use
pattern matching for intensional analysis.
Without layers, both $\tletbox$ and pattern matching are also available inside of
$\tbox$, which makes the behavior of the overall type theory overwhelmingly difficult
to control.

§.§ Full Set of Rules for Completeness

In this section, we simply list the rest of the equivalence rules for the sake of
complete definition of the system.
We have the following PER rules:

i s t T
i t s T

i s t T
i t u T
i s u T

i δδ'Δ
i δ'δ Δ

[Ψ][Γ_0] i δδ' Γ_1
[Ψ][Γ_1] i δ'δ”Γ_2
[Ψ][Γ_0] i δδ” Γ_1

Then we have the following congruence rules:

0 Ψ
i Γ
i ···

i δδ'Δ
i tt'T
i δ, t/xδ', t'/xΔ, x : T

i δδ' Δ
u : ([Δ] T) ∈Ψ

0 Ψ
i Γ
x : T ∈Γ
i x x T

0 Ψ
i Γ

i s_0s_0' T
[Ψ][Γ, x : , y : T]is_1s_1'T

i t t'
iTs_0x y. s_1tTs_0'x y. s_1't'T

[Ψ][Γ, x : S]itt'T
iλx. tλx. t'S T

itt'S T
it st' s'T

0 Ψ

1 ss'□T
[Ψ, u : T] 1 tt'T'
1 u s tus't' T'

§.§ Reexamination of Syntactic Properties

After establishing the 2-layered contextual modal type theory, we now reexamine the
useful properties of the judgments in <Ref>.
Most of these properties pleasantly remain stable in our contextual system.
We simply enumerate them and sketch their proofs.

If $\iscore T$ ($\iscore \Gamma$, resp.), then $\istype T$ ($\istype \Gamma$, resp.).

If $\ltyping i t T$, then $\iscore \Psi$ and

* if $i = 0$, then $\iscore \Gamma$ and $\iscore T$;

* if $i = 1$, then $\istype \Gamma$ and $\istype T$.

If $\ltyping i \delta \Delta$, then $\iscore \Psi$ and

* if $i = 0$, then $\iscore \Gamma$ and $\iscore \Delta$;

* if $i = 1$, then $\istype \Gamma$ and $\istype \Delta$.

If $\ltyping 1 \branch {\judge[\Delta] T \STo T'}$, then
$\iscore \Psi$, $\istype \Gamma$, $\iscore \Delta$, $\iscore T$ and $\istype{T'}$.

Mutual induction.

The lifting of layer from $0$ to $1$ is mutually proved between terms and local substitutions.
$ $

* If $\ltyping 0 t T$, then $\ltyping 1 t T$.

* If $\ltyping 0 \delta \Delta$, then $\ltyping 1 \delta \Delta$.

Both lifting lemmas are proved by mutual induction.

Similarly, the following lemmas are also proved mutually:
$ $

* If $\ltyequiv 0 t s T$, then $t = s$.

* If $\ltyequiv 0 {\delta}{\delta'} \Delta$, then $\delta = \delta'$.

lem:ct:presup $ $

* If $\ltyequiv i{t}{t'}T$, then $\ltyping i t T$ and $\ltyping i {t'}T$.

* If $\ltyequiv i{\delta}{\delta'}\Delta$, then $\ltyping i \delta {\Delta}$ and
$\ltyping i {\delta'}\Delta$.

* If $\ltyequiv 1 {\branch}{\branch'}{\judge[\Delta] T \STo T'}$, then$\ltyping 1 \branch
{\judge[\Delta] T \STo T'}$ and $\ltyping 1{\branch'}{\judge[\Delta] T \STo T'}$.

Induction. Here we will need the substitution lemmas.

Next we define how local substitutions are applied to terms:

\begin{align*}
x[\delta] &:= \delta(x) \tag{lookup $x$ in $\delta$} \\
u^{\delta'}[\delta] &:= u^{\delta' \circ \delta}  \\
\ze[\delta] &:= \ze \\
\su t [\delta] &:= \su{(t[\delta])} \\
\boxit t [\delta] &:= \boxit t \\
\letbox u s t [\delta] &:= \letbox u{s[\delta]}{(t[\delta])}\\
\matc s \ \vect\branch [\delta] &:= \matc {s[\delta]}\ (\vect\branch[\delta]) \\
\lambda x. t [\delta] &:= \lambda x. (t[\delta, x/x]) \\
t\ s [\delta] &:= (t[\delta]) \ (s[\delta]) \\[5pt]
\cdot \circ \delta &:= \cdot \\
(\delta', t/x) \circ \delta &:= (\delta' \circ \delta) , t[\delta]/x \\[5pt]
\var x \STo t[\delta] &:= \var x \STo (t[\delta]) \\
\ze \STo t [\delta] &:= \ze \STo (t[\delta]) \\
\su{?u} \STo t [\delta] &:= \su{?u} \STo (t[\delta]) \\
\lambda x. ?u \STo t [\delta] &:= \lambda x. ?u \STo (t[\delta]) \\
?u~?u' \STo t[\delta] &:= ?u~?u' \STo (t[\delta])
\end{align*}

The local substitution lemma is a bit more cumbersome to establish than in
<Ref>, because now it is possible to apply local substitutions at layer $0$ in
the process of global substitutions (we will see how this happens in the next
Moreover, global variables store local substitutions, so the composition must also be
mutually defined at the same time.
It becomes a bit more complex at layer $1$ where we need to go under pattern matching.

Let us examine the properties layer by layer.

If $\ltyping[\Psi][\Delta] 0 t T$ and $\ltyping 0 \delta \Delta$, then $\ltyping 0{t[\delta]} T$.

If $\ltyping[\Psi][\Delta] 0 {\delta'}{\Delta''}$ and
$\ltyping[\Psi][\Delta'] 0 \delta \Delta$, then
$\ltyping[\Psi][\Delta'] 0 {\delta' \circ \delta}{\Delta''}$.

We do a mutual induction on $\ltyping[\Psi][\Delta] 0 t T$ and
$\ltyping[\Psi][\Delta] 0 {\delta'}{\Delta''}$.

It is easier to consider the local composition theorem first, where we simply invoke
local substitution for all terms.
Now we consider the cases of $t$.

* $t = x$, and we know $x : T \in \Delta$.
Then the goal is immediate.

* $t = u^{\delta'}$ and $u : (\judge[\Delta'] T) \in \Phi$,
By using the local composition theorem on $\delta'$ as the smaller argument, we

\begin{align*}
\ltyping 0{\delta' \circ \delta}{\Delta'}
\end{align*}

which concludes the goal.

* $t = \ze$ and $t = \su t'$ are immediate.

* $t = \lambda x. t'$ and $t = t'~s$ are folklore and identical to the proof in

The case for layer $1$ is slightly more complex because we need to consider pattern
Luckily, pattern matching on code only grows the global contexts so we simply
propagate the local substitutions recursively.

If $\ltyping[\Psi][\Delta] 1 t T$ and $\ltyping 1 \delta \Delta$, then $\ltyping 1{t[\delta]} T$.

If $\ltyping[\Psi][\Delta] 1 {\delta'}{\Delta''}$ and
$\ltyping[\Psi][\Delta'] 1 \delta \Delta$, then
$\ltyping[\Psi][\Delta'] 1 {\delta' \circ \delta}{\Delta''}$.

If $\ltyping[\Psi][\Delta] 1 \branch {\judge[\Delta'] T \STo T'}$ and
$\ltyping 1 \delta \Delta$, then
$\ltyping 1 {\branch[\delta]} {\judge[\Delta'] T \STo T'}$.

If $\ltyping[\Psi][\Delta] 1 {\vect\branch} {\judge[\Delta'] T \STo T'}$ and
$\ltyping 1 \delta \Delta$, then
$\ltyping 1 {\vect\branch[\delta]} {\judge[\Delta'] T \STo T'}$.

We also do mutual induction here.
For the local substitutions, the extra cases are $\tbox$ and pattern matching.
The other cases are pretty much identical to the previous theorems.
The introduction rule of $\square$ is easy because we do not even propagate the
local substitution.
The case of pattern matching is also simple because we just push the local
substitutions downward and eventually hit the cases for branches.

* $\branch = \var x \STo t$, then we know $\ltyping[\Psi][\Delta] 1 t T'$.
By IH, we have $\ltyping 1 {t[\delta]} T'$ which concludes the goal.

* $\branch = \ze \STo t$, then the same argument as above applies.

* $\branch = \su ?u \STo t$, then $\ltyping[\Psi, u :
(\judge[\Delta']\Nat)][\Delta] 1 t T'$.
Since the local context does not change, we can still apply $\delta$ directly to
$t$ by IH and obtain the goal.

* $\branch = \lambda x. ?u \STo t$ and $\branch = ?u~?u' \STo t$ are similar to the
previous case.

§.§ Global Simultaneous Substitutions

The final missing piece in our syntactic development of this type theory is global
simultaneous substitutions.
We simply adapt our previous work here and fix the differences.

\begin{align*}
\sigma := \cdot \sep \sigma, t/u \tag{Global substitutions}
\end{align*}

0 tT
[Ψ]σ, t/uΦ, u : (T)

The step case of typing rules now allow $t$ to be typed in a specified local context
according to the binding.
The equivalence follows similarly.

0 tt'T
[Ψ]σ, t/uσ', t'/uΦ, u : (T)

Next we define the application of global substitutions:

\begin{align*}
x[\sigma] &:= x \\
u^\delta[\sigma] &:= \sigma(u)[\delta[\sigma]] \tag{lookup $u$ in $\sigma$} \\
\ze[\sigma] &:= \ze \\
\su t [\sigma] &:= \su{(t[\sigma])} \\
\boxit t [\sigma] &:= \boxit{(t[\sigma])} \\
\letbox u s t[\sigma] &:= \letbox u {s[\sigma]}{(t[\sigma])} \\
\matc s \ \vect\branch [\sigma] &:= \matc {s[\sigma]} \ (\vect\branch[\sigma]) \\
\lambda x. t [\sigma] &:= \lambda x. (t[\sigma]) \\
t~s [\sigma] &:= (t[\sigma])~(s[\sigma]) \\[5pt]
\cdot[\sigma] &:= \cdot \\
(\delta', t/x) [\sigma] &:= \delta'[\sigma] , t[\sigma]/x \\[5pt]
\var x \STo t[\sigma] &:= \var x \STo (t[\sigma]) \\
\ze \STo t [\sigma] &:= \ze \STo (t[\sigma]) \\
\su{?u} \STo t [\sigma] &:= \su{?u} \STo (t[\sigma, u/u]) \\
\lambda x. ?u \STo t [\sigma] &:= \lambda x. ?u \STo (t[\sigma, u/u]) \\
?u~?u' \STo t[\sigma] &:= ?u~?u' \STo (t[\sigma, u/u, u'/u'])
\end{align*}

Most cases proceed in expected ways.
The case of global variables is probably the most interesting one.
We first lookup the global substitution and obtain an open term $\sigma(u)$.
In order to obtain a legal term in the current context, we must apply the local
substitution $\delta$.
But before that, we need to recursively apply $\sigma$ to all terms in $\delta$ so
that $\delta$ lives in the correct global context.
At last, we apply $\delta[\sigma]$ following the previous definition and obtain a term
in the right global and local contexts.
This intuition can be justified by the following theorems:
$ $

* If $\ltyping[\Phi] i t T$ and $\typing[\Psi]\sigma\Phi$, then $\ltyping
i{t[\delta]} T$.

* If $\ltyping[\Phi] i {\delta}{\Delta}$ and
$\typing[\Psi]\sigma\Phi$, then
$\ltyping i {\delta[\sigma]}{\Delta}$.

* If $\ltyping[\Phi] 1 \branch {\judge[\Delta] T \STo T'}$ and
$\typing[\Psi]\sigma\Phi$, then
$\ltyping 1 {\branch[\delta]} {\judge[\Delta] T \STo T'}$.

* If $\ltyping[\Phi] 1 {\vect\branch} {\judge[\Delta] T \STo T'}$ and
$\typing[\Psi]\sigma\Phi$, then
$\ltyping 1 {\vect\branch[\delta]} {\judge[\Delta] T \STo T'}$.

We do mutual induction.

* $t = u^\delta$

[Φ] i δΔ
u : ([Δ] T) ∈Φ

\begin{align*}
& \ltyping[\Psi][\Delta] 0 {\sigma(u)} T \tag{lookup of $\sigma$} \\
& \ltyping[\Phi] i{\delta[\sigma]} \Delta
\byIH \\
& \ltyping 0 {\sigma(u)[\delta[\sigma]]} T
\tag{by local substitution}
\end{align*}

* $t = \boxit{t'}$

[Φ][Δ] 0t'T'

\begin{align*}
& \ltyping[\Psi][\Delta] 0{t'[\sigma]}T'
\byIH \\
& \ltyping{1}{\boxit {t'[\sigma]}}{\cont[\Delta]{T'}}
\end{align*}

* $t = \matc s \ \vect\branch$, then we simply push $\sigma$ inwards by IHs.

* $\branch = \var x \STo t$,

x : T ∈Δ
[Φ] 1 t T'
[Φ] 1 x t[Δ] T T'

\begin{align*}
& \ltyping 1{t[\sigma]} T'
\byIH \\
& \ltyping 1 {\var x \STo (t[\sigma])}{\judge[\Delta] T \STo T'}
\end{align*}

* $\branch = \lambda x. ?u \STo t$,

[Φ, u : ([Δ, x : S]T)] 1 t T'
[Φ] 1 λx. ?u t[Δ] S T T'

\begin{align*}
& \typing[\Psi, u : (\judge[\Delta, x : S]T)]{\sigma,u/u}{\Phi, u :
(\judge[\Delta, x : S]T)}
\\
& \ltyping[\Psi, u : (\judge[\Delta, x : S]T)] 1{t[\sigma,u/u]}T'
\byIH \\
& \ltyping 1 {\lambda x. ?u \STo (t[\sigma,u/u])}{\judge[\Delta] S \func T \STo T'}
\end{align*}

* $\branch = ?u~?u' \STo t$,

∀S.  [Φ, u : ([Δ]S T), u' : ([Δ]S)] 1 t T'
[Φ] 1 ?u ?u' t[Δ] T T'

\begin{align*}
& \typing[\Psi, u : (\judge[\Delta]S \func T), u' :
(\judge[\Delta]S)]{\sigma,u/u,u'/u'}{\Phi, u : (\judge[\Delta]S \func T), u' :
\\
& \ltyping[\Psi, u : (\judge[\Delta]S \func T), u' : (\judge[\Delta]S)]
1{t[\sigma,u/u, u'/u']}T'
\byIH \\
& \ltyping 1 {?u~?u' \STo (t[\sigma,u/u,u'/u'])}{\judge[\Delta] T \STo T'}
\end{align*}

We could also define the substitutions between dual contexts, but they are define in
an identical way to the development in <Ref>, so we omit the details here for
In the next section, we move on to the adaptation of the presheaf model, and show that
the 2-layered contextual modal type theory is normalizing by evaluation.

§ PRESHEAF MODEL FOR CONTEXTUAL TYPES

Having developed the syntactic theory of the 2-layered contextual modal type theory,
the next step following the previous development is to show its normalization by using
a presheaf model.
The adaptation is largely moderate.
We only need to pay more attention to the interpretation of pattern matching and make
adjustments to the models in the completeness and soundness proofs.

§.§ Weakenings and Presheaves

Due to the significant changes in global contexts, our definition of global weakenings
should also be adjusted:

ε: ·_g ·

γ: Ψ_g Φ
q(γ) : Ψ, u : (T) _g Φ, u : (T)

γ: Ψ_g Φ
p(γ) : Ψ, u : (T) _g Φ

We only add the extra premises of $\iscore \Gamma$.
We still refer to the category of dual contexts and weakenings as $\WC$.

Next we move on to fix the interpretations:

\begin{align*}
\intp{\_} &: \Typ \to \WC^{op} \To \SetC \\
\intp{\Nat} &:= \Nf^\Nat \\
\intp{\cont T} &:= \Nf^{\cont T} \\
\intp{S \func T} &:= \intp{S} \hfunc \intp{T}
\end{align*}

Again the fix is moderate.
The interpretation of a contextual type is the presheaf to the set of normal forms of
that contextual type.
Since $\Nf^T$ in general is a presheaf, so all properties about this interpretation
remain true.
The interpretations of global, local and dual contexts remain the same, as well as
their properties including functoriality.
The definitions of reification and reflection only require minimal case to handle
contextual types instead:

\begin{align*}
\downarrow^T &: \intp{T} \To \Nf^T \\
\downarrow^{\cont[\Delta] T}_{\;\Psi;\Gamma}(a)
&:= a \\
\uparrow^T &: \Ne\ T \To \intp{T} \\
\uparrow^{\cont[\Delta] T}_{\;\Psi;\Gamma}(v)
&:= v
\end{align*}

Additionally, we need to a version of reification for local substitutions, because our
neutral form $u^\theta$ requires $\theta$ to be the normal local substitutions,
i.e. to only contain normal forms.

\begin{align*}
\downarrow^{\cdot}_{\;\Psi;\Gamma}(*)
&:= \cdot \\
\downarrow^{\Delta, x : T}_{\;\Psi;\Gamma}(\rho, a)
&:= \downarrow^{\Delta}_{\;\Psi;\Gamma}(\rho), \downarrow^{T}_{\;\Psi;\Gamma}(a)/x
\end{align*}

With $\rho \in \intp{\Delta}_{\;\Psi; \Gamma}$, let
$\theta := \uparrow^\Delta_{\;\Psi; \Gamma}(\rho)$.
Then we have $\ltyping 1 {\theta}\Delta$ and $\theta$ is a normal local substitution.

We do induction on $\Delta$.
Note that $\downarrow^{T}_{\;\Psi;\Gamma}(a)$ always returns normal forms.

Finally, we fix the interpretation of terms as natural transformations.

\begin{align*}
\intp{\_}
&: \forall i \to \ltyping[\Phi][\Delta] i t T \to \intp{\Phi;\Delta}^i \To \intp{T} \\
\intp{u^\delta}^0_{\;\Psi;\Gamma}(\gamma; \rho)
&:= \uparrow^{T}_{\;\Psi; \Gamma}(u[\gamma]^{\theta})
\tag{where $\ltyping[\Phi][\Delta]0\delta{\Delta'}$ and $\theta := \downarrow^{\Delta'}_{\;\Psi; \Gamma}(\intp{\delta}^0_{\;\Psi;
\Gamma}(\gamma; \rho))$}\\
\intp{u^\delta}^1_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \intp{\sigma(u)}^0_{\;\Psi; \Gamma}(\id; \intp{\delta}^1_{\;\Psi;\Gamma}(\sigma;
\rho)) \\
\intp{\boxit t}^1_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \boxit {(t[\sigma])} \\
\intp{\matc{t}\ \vect\branch}^1_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \tmatc(s, \vect\branch)_{\;\Psi; \Gamma}(\sigma; \rho)
\tag{if $\intp{t}^1_{\;\Psi;\Gamma}(\sigma; \rho) = \boxit s$} \\
\intp{\matc{t}\ \vect\branch}^1_{\;\Psi;\Gamma}(\sigma; \rho)
&:= \uparrow^{T}_{\;\Psi; \Gamma}(\matc v\ \vect\nbranch)
\tag{if $\intp{t}^1_{\;\Psi;\Gamma}(\sigma; \rho) = v : \square S$
and $\vect\nbranch :=\tnfbranch(\vect\branch)_{\;\Psi; \Gamma}(\sigma;\rho)$}
\\[5pt]
\intp{\_}
&: \forall i \to \ltyping[\Phi][\Delta] i \delta \Delta' \to \intp{\Phi;\Delta}^i
\To \intp{\Delta'} \\
\intp{\cdot}^i_{\;\Psi;\Gamma}(\_)
&:= * \\
\intp{\delta, t/x}^i_{\;\Psi;\Gamma}(\sigma;\rho)
&:= (\intp{\delta}^i_{\;\Psi;\Gamma}(\sigma;\rho), \intp{t}^i_{\;\Psi;\Gamma}(\sigma;\rho))
\\[5pt]
\tmatc
&: \ltyping[\Psi][\Delta'] 0 t T \to
\ltyping[\Phi][\Delta] 1{\vect\branch}{\judge[\Delta'] T \STo T'} \to
\intp{\Phi;\Delta}^1_{\;\Psi; \Gamma} \to \intp{T}_{\;\Psi; \Gamma} \\
\tmatc(x, \vect\branch)_{\;\Psi; \Gamma}(\sigma; \rho)
\intp{t}^1_{\;\Psi; \Gamma}(\sigma; \rho)
\tag{where $\var x \STo t := \vect\branch(x)$} \\
\tmatc(\ze, \vect\branch)_{\;\Psi; \Gamma}(\sigma; \rho)
\intp{t}^1_{\;\Psi; \Gamma}(\sigma; \rho)
\tag{where $\ze \STo t := \vect\branch(\ze)$} \\
\tmatc(\su s, \vect\branch)_{\;\Psi; \Gamma}(\sigma; \rho)
\intp{t}^1_{\;\Psi; \Gamma}(\sigma, s/u; \rho)
\tag{where $\su ?u \STo t := \vect\branch(\su s)$} \\
\tmatc(\lambda x. s, \vect\branch)_{\;\Psi; \Gamma}(\sigma; \rho)
\intp{t}^1_{\;\Psi; \Gamma}(\sigma, s/u; \rho)
\tag{where $\lambda x. ?u \STo t := \vect\branch(\lambda x. s)$} \\
\tmatc(t'~s, \vect\branch)_{\;\Psi; \Gamma}(\sigma; \rho)
\intp{t}^1_{\;\Psi; \Gamma}(\sigma, t'/u, s/u; \rho)
\tag{where $?u~?u' \STo t := \vect\branch(t'~s)$} \\
\tmatc(u^\delta, \vect\branch)_{\;\Psi; \Gamma}(\sigma; \rho)
&:= \uparrow^{T'}_{\;\Psi; \Gamma}(\matc {\boxit{u^\delta}}\ \vect\nbranch)
\tag{where $\vect\nbranch :=\tnfbranch(\vect\branch)_{\;\Psi; \Gamma}(\sigma;\rho)$} \\[5pt]
\tnfbranch &: \ltyping[\Phi][\Delta] 1{\branch}{\judge[\Delta'] T \STo T'} \to
\intp{\Phi;\Delta}^1_{\;\Psi; \Gamma} \to
\ltyping 1{\nbranch}{\judge[\Delta'] T \STo T'} \\
\tnfbranch(\var x \STo t)_{\;\Psi; \Gamma}(\sigma; \rho)
&:= \var x \STo \downarrow^{T'}_{\;\Psi; \Gamma}(\intp{t}^1_{\;\Psi; \Gamma}(\sigma; \rho)) \\
\tnfbranch(\ze \STo t)_{\;\Psi; \Gamma}(\sigma; \rho)
&:= \ze \STo \downarrow^{T'}_{\;\Psi; \Gamma}(\intp{t}^1_{\;\Psi; \Gamma}(\sigma;
\rho)) \\
\tnfbranch(\su ?u \STo t)_{\;\Psi; \Gamma}(\sigma; \rho)
&:= \su ?u \STo \downarrow^{T'}_{\;\Psi, u: (\judge[\Delta']\Nat);
\Gamma}(\intp{t}^1_{\;\Psi, u: (\judge[\Delta']\Nat); \Gamma}(\sigma', u/u;
\rho'))
\tag{where $p(\id); \id : \Psi, u: (\judge[\Delta']\Nat);\Gamma \To \Psi;\Gamma$ and $(\sigma'; \rho')
:= (\sigma; \rho)[p(\id); \id]$} \\
\tnfbranch(\lambda x. ?u \STo t)_{\;\Psi; \Gamma}(\sigma; \rho)
&:= \lambda x. ?u \STo \downarrow^{T'}_{\;\Psi, u: (\judge[\Delta', x : S]T);
\Gamma}(\intp{t}^1_{\;\Psi, u: (\judge[\Delta', x : S]T); \Gamma}(\sigma', u/u;
\rho'))
\tag{where $S$ is the type of $x$, $p(\id); \id : \Psi, u:
(\judge[\Delta', x : S]T);\Gamma \To \Psi;\Gamma$ and $(\sigma'; \rho') := (\sigma; \rho)[p(\id); \id]$} \\
\tnfbranch(?u~?u' \STo t)_{\;\Psi; \Gamma}(\sigma; \rho)
&:= ?u~?u' \STo \downarrow^{T'}_{\;\Psi, u: (\judge[\Delta']{S \func T'}), u':
(\judge[\Delta']S); \Gamma}(\intp{t}^1_{\;\Psi, u: (\judge[\Delta']{S \func T'}),
u': (\judge[\Delta']S); \Gamma}(\sigma', u/u, u'/u'; \rho'))
\tag{where $S$ is a parameterized core type, }  \\
\tag{$p(p(\id)); \id : \Psi, u: (\judge[\Delta']{S \func T'}), u': (\judge[\Delta']S);\Gamma \To \Psi;\Gamma$ and
$(\sigma'; \rho') := (\sigma; \rho)[p(p(\id)); \id]$}
\end{align*}

The interpretation of terms has grown substantially more complex than the previous
We only write down the modal cases because the other cases are folklore and remain
Let us break down what is changed after the introduction of contextual types and
pattern matching by the following lemma.
$ $

* If $\ltyping[\Phi][\Delta] i t T$ and $(\sigma;\rho) \in \intp{\Phi;\Delta}^i_{\;\Psi; \Gamma}$,
$\intp{t}^i_{\;\Psi; \Gamma}(\sigma;\rho) \in \intp{T}_{\;\Psi; \Gamma}$.

* If $\ltyping[\Phi][\Delta] i \delta \Delta'$ and
$(\sigma;\rho) \in \intp{\Phi;\Delta}^i_{\;\Psi; \Gamma}$, then
$\intp{\delta}^i_{\;\Psi; \Gamma}(\sigma;\rho) \in \intp{\Delta'}_{\;\Psi; \Gamma}$.

* $t = u^\delta$ and $i = 0$,
first, due to contextual types, all global variables must keep track of local

[Φ][Δ] 0 δΔ'
u : ([Δ'] T) ∈Φ

Since we are at layer $0$, we know $\gamma : \Psi \To_g \Phi$, hence

\begin{align*}
& \intp{\delta}^0_{\;\Psi; \Gamma}(\gamma;\rho) \in \intp{\Delta'}_{\;\Psi;
\Gamma}
\byIH \\
& \ltyping 0 {\downarrow^{\Delta'}_{\;\Psi; \Gamma}(\intp{\delta}^0_{\;\Psi;
\Gamma}(\gamma;\rho))} \Delta'
\tag{by \Cref{lem:ct:reif-lsubst}} \\
& \ltyping 0 {u[\gamma]^\theta} T
\tag{where ${u[\gamma]^\theta}$ is neutral} \\
& \uparrow^T_{\;\Psi; \Gamma}({u[\gamma]^\theta}) \in \intp{T}_{\;\Psi; \Gamma}
\end{align*}

* $t = u^\delta$ and $i = 1$,

[Φ][Δ] 1 δΔ'
u : ([Δ'] T) ∈Φ

Similar to before, we decrease the layer from $1$ to $0$ to perform further
interpretation of terms.
However, the recursive interpretation is done in a non-empty environment.

\begin{align*}
& \intp{\delta}^1_{\;\Psi; \Gamma}(\gamma;\rho) \in \intp{\Delta'}_{\;\Psi;
\Gamma}
\byIH \\
& \ltyping[\Psi][\Delta'] 0{\sigma(u)}T \\
& (\id; \intp{\delta}^1_{\;\Psi; \Gamma}(\gamma;\rho)) \in \intp{\Psi; \Delta'}^0_{\;\Psi;
\Gamma} \\
& \intp{\sigma(u)}^0_{\;\Psi; \Gamma}(\id; \intp{\delta}^1_{\;\Psi;\Gamma}(\sigma;
\rho)) \in \intp{T}_{\;\Psi; \Gamma}
\end{align*}

* $t = \boxit t'$, we do not have to check much as the global substitution
property directly applies.

* $t = \matc s \ \vect\branch$, this case is rather simple by following the types
of $\tmatc$ and $\tnfbranch$ functions.

Now we have finished the adjustments to the presheaf model.
We restate the definition of the NbE algorithm and its completeness and soundness
Next, we move on to fixing the proofs of various properties, as well as the
completeness and soundness proofs.

A normalization by evaluation algorithm given $\ltyping 1 t T$ is

\begin{align*}
\nbe^T_{\;\Psi;\Gamma}(t) &:= \downarrow^T_{\;\Psi;\Gamma} (\intp{t}^1_{\;\Psi;\Gamma}(\uparrow^{\Psi;\Gamma}))
\end{align*}

If $\ltyequiv 1 t {t'} T$, then $\nbe^T_{\;\Psi;\Gamma}(t) = \nbe^T_{\;\Psi;\Gamma}(t')$.

If $\ltyping 1 t T$, then $\ltyequiv 1 t {\nbe^T_{\;\Psi;\Gamma}(t)} T$.

§.§ Properties of Interpretations

Following the steps before, we reestablish several important properties that are
useful for later proofs.

$\uparrow^{\Delta'}$ is natural, i.e. for
$\gamma; \tau : \Phi; \Delta \To \Psi;\Gamma$, we have
$\uparrow^{\Delta'}_{\;\Psi;\Gamma}(\rho)[\gamma; \tau] =
\uparrow^{\Delta'}_{\;\Phi;\Delta}(\rho[\gamma; \tau])$.

This is a natural consequence of the naturality of $\uparrow^T$.

lem:ct:gsubst-nat-gen $ $

* If $\ltyping[\Phi][\Delta] 0 t T$, $\gamma' : \Psi' \To_g \Psi$,
$\gamma : \Psi \To_g \Phi$ and $\rho \in \intp{\Delta}_{\;\Psi';\Gamma}$, then
$\intp{t}^0_{\;\Psi';\Gamma}(\gamma \circ \gamma';\rho) =
\intp{t[\gamma]}^0_{\;\Psi';\Gamma}(\gamma';\rho)$.

* If $\ltyping[\Phi][\Delta] 0 \delta \Delta'$, $\gamma' : \Psi' \To_g \Psi$,
$\gamma : \Psi \To_g \Phi$ and $\rho \in \intp{\Delta}_{\;\Psi';\Gamma}$, then
$\intp{\delta}^0_{\;\Psi';\Gamma}(\gamma \circ \gamma';\rho) =
\intp{\delta[\gamma]}^0_{\;\Psi';\Gamma}(\gamma';\rho)$.

Only the case of global variables is worth looking into.
If $t = u^\delta$ and $\ltyping[\Phi][\Delta] 0 \delta \Delta'$.

\begin{align*}
\intp{u^\delta}^0_{\;\Psi';\Gamma}(\gamma \circ \gamma';\rho)
&= \uparrow_{\;\Psi';\Gamma}(u[\gamma \circ \gamma']^\theta)
\tag{where $\theta := \downarrow^{\Delta'}_{\;\Psi';\Gamma}(\intp{\delta}^0_{\;\Psi';\Gamma}(\gamma \circ \gamma';\rho))$} \\
&= \uparrow_{\;\Psi';\Gamma}(u[\gamma][\gamma']^\theta)
\tag{notice $\theta =
\downarrow^{\Delta'}_{\;\Psi';\Gamma}(\intp{\delta[\gamma]}^0_{\;\Psi';\Gamma}(\gamma';\rho))$
by IH} \\
&= \intp{u[\gamma]^{\delta[\gamma]}}^0_{\;\Psi';\Gamma}(\gamma';\rho) \\
&= \intp{u^\delta[\gamma]}^0_{\;\Psi';\Gamma}(\gamma';\rho)
\end{align*}

If $\ltyping[\Phi][\Delta] 0 t T$, $\gamma : \Psi \To_g \Phi$ and
$\rho \in \intp{\Delta}_{\;\Psi;\Gamma}$, then
$\intp{t}^0_{\;\Psi;\Gamma}(\gamma;\rho) = \intp{t[\gamma]}^0_{\;\Psi;\Gamma}(\id;\rho)$.

Now we reestablish the naturality of interpretations:
lem:st:t-intp-nat $ $

* If $\ltyping[\Phi][\Delta] i t T$, $\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma$ and
$\sigma;\rho \in \intp{\Phi;\Delta}^i_{\;\Psi;\Gamma}$, then
$\intp{t}^i_{\;\Psi;\Gamma}(\sigma;\rho)[\gamma;\tau] =
\intp{t}^i_{\;\Psi';\Gamma'}((\sigma;\rho)[\gamma;\tau])$.

* If $\ltyping[\Phi][\Delta] i \delta \Delta'$, $\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma$ and
$\sigma;\rho \in \intp{\Phi;\Delta}^i_{\;\Psi;\Gamma}$, then
$\intp{\delta}^i_{\;\Psi;\Gamma}(\sigma;\rho)[\gamma;\tau] =
\intp{\delta}^i_{\;\Psi';\Gamma'}((\sigma;\rho)[\gamma;\tau])$.

* If $\ltyping[\Psi][\Delta'] 0 t T$ and
$\ltyping[\Phi][\Delta] 1{\vect\branch}{\judge[\Delta'] T \STo T'}$,
$\sigma;\rho \in \intp{\Phi;\Delta}^1_{\;\Psi;\Gamma}$, and
$\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma$, then
$\tmatc(t, \vect\branch)_{\;\Psi;\Gamma}(\sigma; \rho)[\gamma; \tau]
= \tmatc(t[\gamma], \vect\branch)_{\;\Psi';\Gamma'}((\sigma; \rho)[\gamma; \tau])$.

* If $\ltyping[\Phi][\Delta] 1{\branch}{\judge[\Delta'] T \STo T'}$,
$\sigma;\rho \in \intp{\Phi;\Delta}^1_{\;\Psi;\Gamma}$, and
$\gamma;\tau : \Psi';\Gamma' \To \Psi;\Gamma$, then
$\tnfbranch(\branch)_{\;\Psi;\Gamma}(\sigma; \rho)[\gamma; \tau] =
\tnfbranch(\branch)_{\;\Psi';\Gamma'}((\sigma; \rho)[\gamma; \tau])$.

The statement of naturality is much more verbose than before because of both
contextual types and pattern matching on code.

We do mutual induction on the first statements of all four statements.

* $i = 0$ and $t = u^\delta$ and $\ltyping[\Phi][\Delta] 0 \delta \Delta'$.
In this case,

\begin{align*}
\intp{u^\delta}^0_{\;\Psi;\Gamma}(\gamma';\rho)[\gamma;\tau]
&= \uparrow_{\;\Psi;\Gamma}(u[\gamma']^\theta)[\gamma;\tau]
\tag{where $\theta := \downarrow^{\Delta'}_{\;\Psi;\Gamma}(\intp{\delta}^0_{\;\Psi;\Gamma}(\gamma';\rho))$}\\
&= \uparrow_{\;\Psi';\Gamma'}(u[\gamma']^\theta[\gamma;\tau])
\tag{naturality of reflection} \\
&= \uparrow_{\;\Psi';\Gamma'}(u[\gamma'][\gamma]^{\theta[\gamma;\tau]}) \\
&= \uparrow_{\;\Psi';\Gamma'}(u[\gamma' \circ \gamma]^{\theta'})
\tag{where $\theta' :=
\downarrow^{\Delta'}_{\;\Psi';\Gamma'}(\intp{\delta}^0_{\;\Psi;\Gamma}((\gamma';\rho)[\gamma;\tau]))
= \theta[\gamma; \tau]$ by IH} \\
&= \intp{u^\delta}^0_{\;\Psi';\Gamma'}((\gamma';\rho)[\gamma;\tau])
\end{align*}

* $i = 1$ and $t = u$ and $\ltyping[\Phi][\Delta] 0 \delta \Delta'$.
In this case,

\begin{align*}
\intp{u^\delta}^1_{\;\Psi;\Gamma}(\sigma;\rho)[\gamma;\tau]
&= \intp{\sigma(u)}^0_{\;\Psi;\Gamma}(\id; \intp{\delta}^1_{\;\Psi;\Gamma}(\sigma;\rho))[\gamma;\tau] \\
&= \intp{\sigma(u)}^0_{\;\Psi;\Gamma}((\id; \intp{\delta}^1_{\;\Psi;\Gamma}(\sigma;\rho))[\gamma;\tau]) \\
\byIH \\
&= \intp{\sigma(u)}^0_{\;\Psi;\Gamma}(\gamma; \intp{\delta}^1_{\;\Psi;\Gamma}(\sigma;\rho)[\gamma;\tau]) \\
&= \intp{\sigma(u)}^0_{\;\Psi;\Gamma}(\gamma;
\intp{\delta}^1_{\;\Psi;\Gamma}((\sigma;\rho)[\gamma;\tau]))
\tag{by IH on $\delta$} \\
&= \intp{\sigma(u)[\gamma]}^0_{\;\Psi;\Gamma}(\id;
\intp{\delta}^1_{\;\Psi;\Gamma}((\sigma;\rho)[\gamma;\tau]))
\tag{by \Cref{lem:ct:gsubst-nat}} \\
&= \intp{u^\delta}^1_{\;\Psi';\Gamma'}((\sigma;\rho)[\gamma;\tau])
\end{align*}

* $i = 1$ and $t = \boxit t'$.
This case is unchanged.

* $i = 1$ and $t = \matc {t'} \ \vect\branch$ and $\intp{t'}^1_{\;\Psi;\Gamma}(\sigma;
\rho) = v$.
Let $\vect\nbranch := \tnfbranch(\vect\branch)_{\;\Psi; \Gamma}(\sigma;\rho)$.
By IH, we have

\begin{align*}
\vect\nbranch[\gamma; \tau] &= \tnfbranch(\vect\branch)_{\;\Psi; \Gamma}(\sigma;\rho)[\gamma; \tau]
= \tnfbranch(\vect\branch)_{\;\Psi'; \Gamma'}((\sigma;\rho)[\gamma; \tau]) \\
v[\gamma; \tau] &= \intp{t'}^1_{\;\Psi;\Gamma}(\sigma;
\rho)[\gamma; \tau] = \intp{t'}^1_{\;\Psi';\Gamma'}((\sigma;
\rho)[\gamma; \tau])
\end{align*}

Therefore, due to

\begin{align*}
\uparrow^T_{\;\Phi;\Gamma}(\matc v \ \vect\nbranch)[\gamma; \tau]
&= \uparrow^T_{\;\Phi;\Gamma}(\matc {v[\gamma; \tau]} \ (\vect\nbranch[\gamma;
\tau]))
\tag{by naturality of reflection}
\end{align*}

we conclude the goal.

* $i = 1$ and $t = \matc {t'} \ \vect\branch$ and $\intp{t'}^1_{\;\Psi;\Gamma}(\sigma;
\rho) = \boxit s$.
Notice that by IH, we have

\begin{align*}
\boxit {(s[\gamma])} = \boxit s[\gamma; \tau]
= \intp{t'}^1_{\;\Psi;\Gamma}(\sigma; \rho)[\gamma; \tau]
= \intp{t'}^1_{\;\Psi';\Gamma'}((\sigma; \rho)[\gamma; \tau])
\end{align*}

We use invoke IH to conclude

\begin{align*}
\tmatc(s, \vect\branch)_{\;\Psi;\Gamma}(\sigma; \rho)[\gamma; \tau]
= \tmatc(s[\gamma], \vect\branch)_{\;\Psi;\Gamma}((\sigma; \rho)[\gamma; \tau])
\end{align*}

Effectively this requires the naturality of $\tmatc$ to be proved, which we will work on next.

For the naturality of $\tmatc$, we know that $\ltyping[\Psi][\Delta'] 0 t T$.
By doing induction, we know that there are only cases of terms in the core type
theory and the case of global variables.
Effectively we are relying on the exhaustiveness of pattern matching on code here.

* $t = x$ and $\vect\branch(x) = \var x \STo t'$,

x : T ∈Δ'

Then $x[\gamma] = x$, then the goal is effectively to prove

\begin{align*}
\intp{t'}^1_{\;\Psi;\Gamma}(\sigma; \rho)[\gamma; \tau]
= \intp{t'}^1_{\;\Psi';\Gamma'}(\sigma; \rho[\gamma; \tau])
\end{align*}

which can be discharged by IH.

* $t = \ze$ and $\vect\branch(\ze) = \ze \STo t'$,

This case is the same as above.

* $t = \su s$ and $\vect\branch(\su s) = \su ?u \STo t'$,

Then we prove

\begin{align*}
\intp{t'}^1_{\;\Psi;\Gamma}(\sigma, s/u; \rho)[\gamma; \tau]
= \intp{t'}^1_{\;\Psi';\Gamma'}(\sigma, s/u; \rho[\gamma; \tau])
\end{align*}

which can be discharged by IH.

* $t = \lambda x. s$ and $\vect\branch(\lambda x. s) = \lambda x. ?u \STo t'$,

[Ψ][Δ', x : S]0sT
[Ψ][Δ']0λx. sS T

This case is the same as above.
The extension of local context does not affect the argument.

* $t = s~s'$ and $\vect\branch(s~s') = ?u~?u' \STo t'$ and for some $\iscore S$,

[Ψ][Δ']0sS T
[Ψ][Δ']0s s'T

This case is still the same expect that there are two terms inserted to the global

* $t = u^\delta$,

[Ψ][Δ'] 0 δΔ”
u : ([Δ”] T) ∈Ψ

In this case, we do not look up $\vect\branch$ at all.
Instead, we just construct a neutral form and use reflection to convert it to a
natural transformation.
Let $\vect\nbranch := \tnfbranch(\vect\branch)_{\;\Psi; \Gamma}(\sigma;\rho)$.
By IH, we have

\begin{align*}
\vect\nbranch[\gamma; \tau] &= \tnfbranch(\vect\branch)_{\;\Psi; \Gamma}(\sigma;\rho)[\gamma; \tau]
= \tnfbranch(\vect\branch)_{\;\Psi'; \Gamma'}((\sigma;\rho)[\gamma; \tau]) \\
\boxit{u^\delta}[\gamma; \tau] &= \boxit{u[\gamma]^{\delta[\gamma]}}
\end{align*}

Therefore, the goal is concluded by the naturality of reflection and the two
equations above.

At last, we have the naturality of $\tnfbranch$ to prove.
This in fact is very similar to the neutral case in the $\tletbox$ expression in our
previous development.
Here we only pick the $\lambda$ case for demonstration.
If $\branch = \lambda x. ?u \STo t$,

[Φ, u : ([Δ', x : S]T)] 1 t T'
[Φ][Δ] 1 λx. ?u t[Δ'] S T T'

Then the goal effectively becomes

\begin{align*}
& \downarrow^{T'}_{\;\Psi, u : (\judge[\Delta', x : S]T);\Gamma}(\intp{t}^1_{\;\Psi,
u : (\judge[\Delta', x : S]T);\Gamma}(\sigma[p(\id)], u/u; \rho[p(\id);
\id]))[q(\gamma); \tau] \\
=~& \downarrow^{T'}_{\;\Psi', u : (\judge[\Delta', x :
S]T);\Gamma'}(\intp{t}^1_{\;\Psi', u : (\judge[\Delta', x :
S]T);\Gamma'}((\sigma[p(\id)], u/u; \rho[p(\id); \id])[q(\gamma); \tau]))
\end{align*}

This equation is further due to

\begin{align*}
\intp{t}^1_{\;\Psi, u : (\judge[\Delta', x : S]T);\Gamma}(\sigma[p(\id)], u/u;
\rho[p(\id); \id])[q(\gamma);\tau] = \intp{t}^1_{\;\Psi', u : (\judge[\Delta', x : S]T);\Gamma'}((\sigma[p(\id)], u/u;
\rho[p(\id); \id])[q(\gamma); \tau])
\end{align*}

This is proved by IH on $t$.

This lemma justifies the claim that the interpretations of terms and local
substitutions return natural transformations.

lem:ct:intp-lsubst-0 $ $

* If $\ltyping[\Phi][\Delta'] 0 t T$, $\ltyping[\Phi][\Delta] 0 \delta \Delta'$,
$\gamma : \Psi \To_g \Phi$ and $\rho \in \intp{\Delta}_{\;\Psi;\Gamma}$, then
$\intp{t[\delta]}^0_{\;\Psi;\Gamma}(\gamma; \rho) =
\intp{t}^0_{\;\Psi;\Gamma}(\gamma; \intp{\delta}^0_{\;\Psi;\Gamma}(\gamma;
\rho))$.

* If $\ltyping[\Phi][\Delta'] 0{\delta'}{\Delta''}$, $\ltyping[\Phi][\Delta] 0 \delta \Delta'$,
$\gamma : \Psi \To_g \Phi$ and $\rho \in \intp{\Delta}_{\;\Psi;\Gamma}$, then
$\intp{\delta' \circ \delta}^0_{\;\Psi;\Gamma}(\gamma; \rho) =
\intp{\delta'}^0_{\;\Psi;\Gamma}(\gamma; \intp{\delta}^0_{\;\Psi;\Gamma}(\gamma;
\rho))$.

We perform mutual induction.

* $t = x$, $t = \ze$, $t = \su t'$, and $t = s~s'$, immediate with possible use
of IHs.

* $t = \lambda x. s$,

[Ψ][Δ', x : S]0sT
[Ψ][Δ']0λx. sS T

We compute

\begin{align*}
\intp{\lambda x. s[\delta]}^0_{\;\Psi;\Gamma}(\gamma; \rho)
&= \intp{\lambda x. (s[\delta[\id;p(\id)], x/x])}^0_{\;\Psi;\Gamma}(\gamma; \rho)
\\
&= (\gamma'; \tau' : \Psi';\Gamma' \To \Psi; \Gamma) (a) \mapsto
\intp{s[\delta[\id;p(\id)], x/x]}^0_{\;\Psi;\Gamma}(\gamma \circ \gamma';
(\rho[\gamma'; \tau'], a)) \\
&= (\gamma'; \tau') (a) \mapsto
\intp{s}^0_{\;\Psi;\Gamma}(\gamma \circ \gamma';
\intp{\delta[\id;p(\id)], x/x}^0_{\;\Psi;\Gamma}(\gamma \circ \gamma';
(\rho[\gamma'; \tau'], a)))
\byIH \\
&= (\gamma'; \tau') (a) \mapsto
\intp{s}^0_{\;\Psi;\Gamma}(\gamma \circ \gamma';
(\intp{\delta}^0_{\;\Psi;\Gamma}(\gamma \circ \gamma';\rho[\gamma'; \tau']),
a)) \\
&= (\gamma'; \tau') (a) \mapsto
\intp{s}^0_{\;\Psi;\Gamma}(\gamma \circ \gamma';
(\intp{\delta}^0_{\;\Psi;\Gamma}(\gamma;\rho)[\gamma'; \tau'], a))
\tag{by naturality of $\intp{\delta}^0$} \\
&= \intp{\lambda x. s}^0_{\;\Psi;\Gamma}(\gamma;
\intp{\delta}^0_{\;\Psi;\Gamma}(\gamma; \rho))
\end{align*}

* $t = u^{\delta'}$,

[Ψ][Δ'] 0δ'Δ”
u : ([Δ”] T) ∈Ψ

We compute as follows

\begin{align*}
\intp{u^{\delta'}[\delta]}^0_{\;\Psi;\Gamma}(\gamma; \rho)
&= \intp{u^{\delta' \circ \delta}}^0_{\;\Psi;\Gamma}(\gamma; \rho) \\
&= \uparrow^T_{\;\Psi;\Gamma}(u[\gamma]^\theta)
\tag{where $\theta := \downarrow^{\Delta''}_{\;\Psi;\Gamma}(\intp{\delta' \circ \delta}^0_{\;\Psi;\Gamma}(\gamma; \rho))$}
\end{align*}

Notice that

\begin{align*}
\intp{\delta' \circ \delta}^0_{\;\Psi;\Gamma}(\gamma; \rho)
&= \intp{\delta'}^0_{\;\Psi;\Gamma}(\gamma;
\intp{\delta}^0_{\;\Psi;\Gamma}(\gamma; \rho))
\byIH
\end{align*}

\begin{align*}
\intp{u^{\delta'}}^0_{\;\Psi;\Gamma}(\gamma;
\intp{\delta}^0_{\;\Psi;\Gamma}(\gamma; \rho))
&= \uparrow^T_{\;\Psi;\Gamma}(u[\gamma]^{\theta'})
\tag{where $\theta' := \downarrow^{\Delta''}_{\;\Psi;\Gamma}(\intp{\delta'}^0_{\;\Psi;\Gamma}(\gamma;
\intp{\delta}^0_{\;\Psi;\Gamma}(\gamma; \rho)))$}
\end{align*}

The goal is seen by having $\theta = \theta'$.

lem:ct:intp-0-1 $ $

* If $\ltyping[\Phi][\Delta] 0 t T$, $\typing[\Psi]\sigma\Phi$, $\gamma : \Psi' \To_g \Psi$ and $\rho \in
\intp{\Delta}_{\;\Psi';\Gamma}$, then
$\intp{t[\sigma]}^0_{\;\Psi';\Gamma}(\gamma; \rho) =
\intp{t}^1_{\;\Psi';\Gamma}(\sigma[\gamma]; \rho)$.

* If $\ltyping[\Phi][\Delta] 0 \delta \Delta'$, $\typing[\Psi]\sigma\Phi$, $\gamma : \Psi' \To_g \Psi$ and $\rho \in