($t_\lambda$) with variables properly substituted.
Since $S$ is also a sub-structure, the recursive call $s_S$ invokes the recursive
principle for code of types instead, hence making the recursive principles mutually

Last, we give the case for function applications.

m Γ
p Δ
[Ψ][Δ]c S l
[Ψ][Δ, x : S  @  l] cTl'

[Ψ][Δ] c tll' x S Tl ⊔l'

[Ψ][Δ] c s S l

T_= T[s/x]

t' = (t ll' x S T s)

s_S = l_1l_2M blΔ(S)

s_T = l_1l_2M bl'(Δ, x : S  @  l)(T)

s_t = l_1l_2M b(l ⊔l')Δ(ll'xST)(t)

s_s = l_1l_2M blΔS(s)

σ= Δ/g,S/U_S,T/U_T,t/u_t,s/u_s

δ= s_S/x_S,s_T/x_T,s_t/x_t,s_s/x_s
m t_[l/ℓ,l'/ℓ',σ,δ]l_1l_2M bl'ΔT_t'M'[l'/ℓ,Δ/g,T_/U_T,t'/x_t]l_2

Similar to above, we can do recursion on all sub-structures, including $S$ and $T$,
which are handled by the recursive principles for code of types.
It is not only convenient to put $S$ and $T$ in the syntax of a function
application, but also necessary.
If we look at $s_t$ and $s_s$, the recursive calls on the function and the argument,
we see that we must supply their types, i.e. $\PI{l}{l'}xST$ and $S$, respectively.
This information, unfortunately, cannot be recovered, if we employed the more common
syntax of $t~s$.
In practice, the $\Pi$ type can be filled in by a type inference algorithm when we do
not care, so it does not truly make the type theory more difficult, but rather enables
the recursion on code of function applications.

At this point, we conclude all rules for .
Next, we shall carefully define all syntactic operations and examine the syntactic
properties of .
Then we work out the semantics by following <Ref> and
<cit.>, from which we conclude the convertibility problem of
is decidable.

§.§ A Note on Layer $v$ Rules

To summarize, only the following rules can be indexed by layer $v$:

* the typing rule for local variables and its congruence;

* the local substitution rules and their equivalence rules;

* the typing rule for global variables and its congruence;

* all conversion rules for terms and their equivalence.

In particular, we are not even obliged to include symmetry and transitivity, because
they can be derived from existing rules.

§ SYNTACTIC OPERATIONS AND PROPERTIES OF

In the previous section, we have introduced all judgments of , but we have
left out some details.
For one, we have not defined the substitution operations yet, though they are very
For the sake of completeness, we will give their definitions.
Then we examine the syntactic properties of before entering the semantic

§.§ Substitution Operations

In <Ref>, we have given the definition of substitutions for universe
levels and how to apply one to a universe level.
Applying a substitution for universe levels to types and terms simply propagate the
substitution downwards.

ll'x S T     l[ϕ]l'[ϕ]xS[ϕ](T[ϕ])

l     l[ϕ]

ℓl T

l t     l[ϕ](t[ϕ])

U^δ    U^δ[ϕ]

g l T     gl[ϕ](T[ϕ])

U ll'T     U[Γ[ϕ]]l[ϕ]l'[ϕ](T[ϕ])

l     [Γ[ϕ]]l[ϕ]

T l     [Γ[ϕ]]T[ϕ]l[ϕ]

·    ·

g     g

Γ, x : T  @  l     Γ[ϕ], x : T[ϕ]  @ l[ϕ]

·^k_g?     ·^k_g?

^k_g     ^k_g

δ, t/x     δ[ϕ], t[ϕ]/x

x     x

ll'x s t     l[ϕ]l'[ϕ]xs[ϕ](t[ϕ])

l     l[ϕ]

t     (t[ϕ])

ll'xSt     l[ϕ]l'[ϕ]xS[ϕ](t[ϕ])

tll'xST s     t[ϕ]l[ϕ]l'[ϕ]xS[ϕ]T[ϕ](s[ϕ])

l ℓt     l[ϕ,ℓ/ℓ]ℓt[ϕ,ℓ/ℓ]

t l     (t[ϕ]) $ (l[ϕ])

u^δ    u^δ[ϕ]

l g t     l[ϕ]g(t[ϕ])

t Γ    t[ϕ](Γ[ϕ])

ll' U t     l[ϕ]l'[ϕ] U(t[ϕ])

t T     t[ϕ](T[ϕ])

T     (T[ϕ])

t     (t[ϕ])

l'lΓx_T. MU.t't     l'[ϕ](l[ϕ])(Γ[ϕ])x_T. M[ϕ]U.t'[ϕ](t[ϕ])

l'lΓTx_t. Mu.t't
l'[ϕ](l[ϕ])(Γ[ϕ])(T[ϕ])x_t. M[ϕ]u.t'[ϕ](t[ϕ])

l_1l_2MblΓt     l_1[ϕ]l_2[ϕ](M[ϕ])(b[ϕ])(l[ϕ])(Γ[ϕ])(t[ϕ])

l_1l_2MblΓT t     l_1[ϕ]l_2[ϕ](M[ϕ])(b[ϕ])(l[ϕ])(Γ[ϕ])(T[ϕ])(t[ϕ])

M     (ℓ,g,x_T. M[ϕ,ℓ/ℓ]) (ℓ,g,U_T,x_t. M'[ϕ,ℓ/ℓ])

(g. t_)     (g. t_[ϕ])

(ℓ,ℓ',g, U_S,U_T,x_S,x_T. t_Π)     (ℓ,ℓ',g, U_S,U_T,x_S,x_T. t_Π[ϕ,ℓ/ℓ,ℓ'/ℓ'])

(ℓ,g. t_)     (ℓ,g. t_[ϕ,ℓ/ℓ])

(ℓ,g,u_t,x_t. t_)     (ℓ,g,u_t,x_t. t_[ϕ,ℓ/ℓ])

(ℓ,g,U_T,u_x. t_x)     (ℓ,g,U_T,u_x. t_x[ϕ,ℓ/ℓ])

(g.t'_)     (g.t'_[ϕ])

(ℓ,ℓ',g,u_s,u_t,x_s,x_t.t'_Π)     (ℓ,ℓ',g,u_s,u_t,x_s,x_t.t'_Π[ϕ,ℓ/ℓ,ℓ'/ℓ'])

(ℓ,g.t'_)     (ℓ,g.t'_[ϕ,ℓ/ℓ])

(g.t_)     (g.t_[ϕ])

(g,u_t,x_t.t_)     (g,u_t,x_t.t_[ϕ])

(ℓ,g,U_M,u_s,u_s',u_t,x_M,x_s,x_s',x_t.t_)     (ℓ,g,U_M,u_s,u_s',u_t,x_M,x_s,x_s',x_t.t_[ϕ,ℓ/ℓ])

(ℓ,ℓ',g,U_S,U_T,u_t,x_S,x_t.t_λ)     (ℓ,ℓ',g,U_S,U_T,u_t,x_S,x_t.t_λ[ϕ,ℓ/ℓ,ℓ'/ℓ'])

The composition operation and the identity substitution are defined intuitively as:
·    ·

(ϕ',l/ℓ)     (ϕ' ∘ϕ), l[ϕ]/ℓ

𝕀_·    ·

𝕀_L,ℓ     𝕀_L,ℓ/ℓ

The presentation of the identity substitution is simpler as we do not consider
weakenings for universe contexts.
We sometimes omit the subscript when it can be inferred from the textual context.
We will also need to apply a universe substitution to global context, which does not
need to be mutually defined:
·    ·

(Ψ, g : )     Ψ[ϕ], g :

(Ψ, U : i l)     Ψ[ϕ], U : [Γ[ϕ]]il[ϕ]

(Ψ, u : i T l)     Ψ[ϕ], u : [Γ[ϕ]]iT[ϕ]l[ϕ]

Then we give the the application of a local substitution.
Following <Ref>, we need two auxiliary definitions to query a local
substitution in order to define its composition.
We repeat their definitions as follows:

\begin{align*}
\widehat{\cdot_{g?}^k} &:= k \\
\widehat{\wk_{g}^k} &:= k \\
\widehat{\delta, t/x} &:= \widehat{\delta} \\
\widecheck{\cdot_{g?}^k} &:= g? \\
\widecheck{\wk_g^k} &:= g \\
\widecheck{\delta, t/x} &:= \widecheck{\delta}
\end{align*}

Then we give the application of local substitutions:

ll'x S T     ll'xS[δ](T[δ,x/x])

l     l

ℓl T

l t     l(t[δ])

U^δ'     U^δ' ∘δ

g l T     gl(T[δ])

U ll'T     U[Γ]ll'(T[δ])

l     l

T l     Tl

x     δ(x) (lookup of $x$ in $\delta$)

ll'x s t     ll'xs[δ](t[δ,x/x])

l     l

t     (t[δ])

ll'xSt     ll'xS[δ](t[δ,x/x])

tll'xST s     t[δ]ll'xS[δ]T[δ,x/x](s[δ])

l ℓt     lℓt[δ]

t l     t[δ]l

u^δ'     u^δ' ∘δ

l g t     lg(t[δ])

t Γ    t[δ]Γ

ll' U t     ll' U(t[δ])

t T     t[δ]T

T     T

t     t

l'lΓx_T. MU.t't     l'lΓx_T. M[δ,x_T/x_T]U.t'[δ](t[δ])

l'lΓTx_t. Mu.t't
l'lΓTx_t. M[δ,x_t/x_t]u.t'[δ](t[δ])

l_1l_2MblΓt     l_1l_2(M[δ])(b[δ])lΓ(t[δ])

l_1l_2MblΓT t     l_1l_2(M[δ])(b[δ])lΓT(t[δ])

M     (ℓ,g,x_T. M[δ,x_T/x_T]) (ℓ,g,U_T,x_t. M'[δ,x_t/x_t])

(g. t_)     (g. t_[δ])

(ℓ,ℓ',g, U_S,U_T,x_S,x_T. t_Π)     (ℓ,ℓ',g, U_S,U_T,x_S,x_T. t_Π[δ,x_S/x_S,x_T/x_T])

(ℓ,g. t_)     (ℓ,g. t_[δ])

(ℓ,g,u_t,x_t. t_)     (ℓ,g,u_t,x_t. t_[δ,x_t/x_t])

(ℓ,g,U_T,u_x. t_x)     (ℓ,g,U_T,u_x. t_x[δ])

(g.t'_)     (g.t'_[δ])

(ℓ,ℓ',g,u_s,u_t,x_s,x_t.t'_Π)     (ℓ,ℓ',g,u_s,u_t,x_s,x_t.t'_Π[δ,x_s/x_s,x_t/x_t])

(ℓ,g.t'_)     (ℓ,g.t'_[δ])

(g.t_)     (g.t_[δ])

(g,u_t,x_t.t_)     (g,u_t,x_t.t_[δ,x_t/x_t])

(ℓ,ℓ',g,U_S,U_T,u_t,x_S,x_t.t_λ)     (ℓ,ℓ',g,U_S,U_T,u_t,x_S,x_t.t_λ[δ,x_S/x_S,x_t/x_t])

where composition is defined in the same way as <Ref>:

\begin{align*}
\wk_g^k \circ \delta &:= \wk_g^{\widehat\delta} \\
\cdot^k \circ \delta &:= \cdot_{\widecheck{\delta}}^{\widehat\delta} \\
\cdot_{g}^k \circ \delta &:= \cdot_{g}^{\widehat\delta} \\
(\delta', t/x) \circ \delta &:= (\delta' \circ \delta), t[\delta]/x
\end{align*}

The identity local substitution is characterized as a generalization of local
weakening $\wk$.

\begin{align*}
\wk^k_{\cdot} &:=  \cdot^k \\
\wk^k_{g} &:=  \wk_g^k \\
\wk^k_{\Gamma, x : T ~@~ l} &:= \wk^{1 + k}_{\Gamma}, x/x
\end{align*}

Identity is just $\id_\Gamma := \wk^0_\Gamma$.

Then we give the global substitutions.

σ   :=       ·σ, Γ/g σ, T/U  σ, t/u
Global substitutions

Then we define the typing rules as:

[L] Ψ

p Γ
σ, Γ/gΦ, g:

[Φ] p Γ

i ∈{c, p}

[Ψ][Γ[σ]] iTl
σ, T/UΦ, u : i l

[Φ] p T l

i ∈{v, c}

[Ψ][Γ[σ]] i tT[σ]l
[Ψ]σ, t/uΦ, u : i T l

Then we consider the cases for application:

ll'x S T     ll'xS[σ](T[σ])

l     l

ℓl T

l t     l(t[σ])

U^δ     σ(U)[δ[σ]]
(lookup of $U$ in $\sigma$)

g l T     gl(T[σ,g/g])

U ll'T     U[Γ[σ]]ll'(T[σ,U^𝕀/U])

l     [Γ[σ]]l

T l     [Γ[σ]]T[σ]l

·    ·

g     σ(g)

Γ, x : T  @  l     Γ[σ], x : T[σ]  @ l

_g^k     ^k_σ(g)

2r(a local weakening extending the local context by length $m$)

·^k      ·^k

·_g^k     ·^|Γ| + m
(if $\sigma(g) = \Gamma$ and $\Gamma$ ends with a $\cdot$)

·_g^k      ·_g'^|Γ| + m
(if $\sigma(g) = \Gamma$ and $\Gamma$ ends with a $g'$)

(δ, t/x)     (δ[σ]), t[σ]/x

x     x
(no effect on local variables)

ll'x s t     ll'xs[σ](t[σ])

l     l

t     (t[σ])

ll'xSt     ll'xS[σ](t[σ])

tll'xST s     t[σ]ll'xS[σ]T[σ](s[σ])

l ℓt     lℓt[σ]

t l     t[σ]l

u^δ     σ(u)[δ[σ]]
(lookup of $u$ in $\sigma$)

l g t     lg(t[σ,g/g])

t Γ    (t[σ])(Γ[σ])

ll' U t     ll' U(t[σ,U^𝕀/U])

t T     (t[σ])(T[σ])

T     (T[σ])

t     (t[σ])

l'lΓx_T. MU.t't     l'lΓx_T. M[σ]U.t'[σ,U^𝕀/U](t[σ])

l'lΓTx_t. Mu.t't
l'lΓTx_t. M[σ]u.t'[σ,u/u](t[σ])

l_1l_2MblΓt     l_1l_2(M[σ])(b[σ])l(Γ[σ])(t[σ])

l_1l_2MblΓT t     l_1l_2(M[σ])(b[σ])l(Γ[σ])(T[σ])(t[σ])

M     (ℓ,g,x_T. M[σ,g/g]) (ℓ,g,U_T,x_t. M'[σ,g/g,U_T^𝕀/U_T])

(g. t_)     (g. t_[σ,g/g])

(ℓ,ℓ',g, U_S,U_T,x_S,x_T. t_Π)     (ℓ,ℓ',g, U_S,U_T,x_S,x_T. t_Π[σ,g/g,U_S^𝕀/U_S,U_T^𝕀/U_T])

(ℓ,g. t_)     (ℓ,g. t_[σ,g/g])

(ℓ,g,u_t,x_t. t_)     (ℓ,g,u_t,x_t. t_[σ,g/g,u_t^𝕀/u_t])

(ℓ,g,U_T,u_x. t_x)     (ℓ,g,U_T,u_x. t_x[σ,g/g,U_T^𝕀/U_T,u_x^𝕀/u_x])

(g.t'_)     (g.t'_[σ,g/g])

(ℓ,ℓ',g,u_s,u_t,x_s,x_t.t'_Π)     (ℓ,ℓ',g,u_s,u_t,x_s,x_t.t'_Π[σ,g/g,u_s^𝕀/u_s,u_t^𝕀/u_t])

(ℓ,g.t'_)     (ℓ,g.t'_[σ,g/g])

(g.t_)     (g.t_[σ,g/g])

(g,u_t,x_t.t_)     (g,u_t,x_t.t_[σ,g/g,u_t^𝕀/u_t])

(ℓ,ℓ',g,U_S,U_T,u_t,x_S,x_t.t_λ)     (ℓ,ℓ',g,U_S,U_T,u_t,x_S,x_t.t_λ[σ,g/g,U_S^𝕀/U_S,U_T^𝕀/U_T,u_t^𝕀/u_t])

Following <Ref>, we give the identity global substitution as a special case of
global weakenings, and composition.

\begin{align*}
\wk^k_{\cdot} &:=  \cdot \\
\wk^k_{\Psi, g : \Ctx} &:=  \wk_{\Psi}^{1+k}, g/g \\
\wk^k_{\Psi, U : \DTyp i l} &:= \wk^{1 + k}_{\Psi}, U^{\id_\Gamma}/U \\
\wk^k_{\Psi, u : \DTrm i T l} &:= \wk^{1 + k}_{\Psi}, u^{\id_\Gamma}/u
\end{align*}

As a special case, we have

\begin{align*}
\id_{\Psi} := \wk^0_{\Psi}
\end{align*}

Moreover, we have composition

\begin{align*}
\cdot \circ \sigma' &:= \cdot \\
(\sigma, \Gamma/g) \circ \sigma' &:= (\sigma \circ \sigma'), \Gamma[\sigma']/g \\
(\sigma, T/U) \circ \sigma' &:= (\sigma \circ \sigma'), T[\sigma']/U \\
(\sigma, t/u) \circ \sigma' &:= (\sigma \circ \sigma'), t[\sigma']/u
\end{align*}

§.§ Properties of Substitutions

In the next step, we examine the algebraic properties of all substitutions.
In the lemmas below, we always assume well-formedness or well-typedness of the
subjects in the lemmas, unless the lemmas are about typing.
For conciseness, we do not spell out the conditions as they are routine.
$ $

* $\typing[L]{\id_L}{L}$

* If $\typing[L]{\phi}{L'}$ and $\typing[L']{\phi'}{L''}$, then
$\typing[L]{\phi' \circ \phi}{L''}$.

Analyze the definition of identity and composition.

$ $

* $l[\phi][\phi'] = l[\phi \circ \phi']$ ($T$, $\Gamma$, $\delta$, $t$, $\Psi$ resp.)

* $l[\id] = l$ ($T$, $\Gamma$, $\delta$, $t$, $\Psi$ resp.)

* $\id \circ \phi = \phi$ and $\phi \circ \id = \phi$

* $(\phi_1 \circ \phi_2) \circ \phi_3 = \phi_1 \circ (\phi_2 \circ \phi_3)$

The proofs are routine; the first two statements are proved by induction on $l$
first, and then mutual induction on all applications of universe substitutions.
The last two we analyze the definition of composition.

Similar lemmas hold for local and global substitutions.
$ $

* $\ltsubst[\Psi][\Gamma,\Delta]i{\wk_{\Gamma}^{|\Delta|}}{\Gamma}$

* $\ltsubst i{\id_{\Gamma}}{\Gamma}$

Note that local substitutions permit $i = v$, so we have $\ltsubst
This intuitively makes sense, as all terms in $\id_{\Gamma}$ are just local variables.
$ $

* $T[\delta][\delta'] = T[\delta \circ \delta']$ ($t$ resp.)

* $T[\id] = T$ ($t$ resp.)

* $\id \circ \delta = \delta$ and $\delta \circ \id = \delta$

* $(\delta_1 \circ \delta_2) \circ \delta_3 = \delta_1 \circ (\delta_2 \circ \delta_3)$

The first statement is mutually proved with associativity and by mutual
induction. The second statement is mutually proved with right identity and also by
mutual induction.
When proving right identity, we realize that all extended local substitutions under
binders are identities.

Then we reason about global substitutions.
$ $

* $\ptyping[\Psi,\Phi] {\wk_{\Psi}^{|\Phi|}}{\Psi}$

* $\ptyping {\id_{\Psi}}{\Psi}$

$ $

* $T[\sigma][\sigma'] = T[\sigma \circ \sigma']$ ($\Gamma$, $\delta$, $t$ resp.)

* $T[\id] = T$ ($\Gamma$, $\delta$, $t$ resp.)

* $\id \circ \sigma = \sigma$ and $\sigma \circ \id = \sigma$

* $(\sigma_1 \circ \sigma_2) \circ \sigma_3 = \sigma_1 \circ (\sigma_2 \circ \sigma_3)$

The first two statements require mutual inductions on the applications of global
Right identity is a natural consequence of the second statement.
Left identity is proved by simply looking at the definition of the identity global
Associativity is routine.

Finally, we conclude how all these kinds of substitutions interact.
lem:dt:wkact $ $

* $\wk^k_\Gamma[\phi] = \wk^k_{\Gamma[\phi]}$

* $\wk^k_\Psi[\phi] = \wk^k_{\Psi[\phi]}$

* $\wk^k_\Gamma[\sigma] = \wk^k_{\Gamma[\sigma]}$

The first two statements are pretty straightforward as the lengths of the contexts
are not altered.
The last one requires a bit more thought.
We proceed by induction on $\Gamma$.

\begin{align*}
\wk^k_\cdot[\sigma]
&= \cdot^k[\sigma] \\
&= \cdot^k
\end{align*}

\begin{align*}
\wk^k_g[\sigma]
&= \wk^k_{\sigma(g)}
\end{align*}

which already matches the definition of $\wk^k_{g[\sigma]}$.

\begin{align*}
\wk^k_{\Gamma,x: T ~@~ l}[\sigma]
&= (\wk^{1 + m}_{\Gamma}, x/x)[\sigma] \\
&= \wk^{1 + m}_{\Gamma}[\sigma], x/x \\
&= \wk^{1 + m}_{\Gamma[\sigma]}, x/x
\byIH \\
&= \wk^{k}_{\Gamma[\sigma], x : T[\sigma] ~@~ l}
\end{align*}

$ $

* $\id_\Gamma[\phi] = \id_{\Gamma[\phi]}$

* $\id_\Psi[\phi] = \id_{\Psi[\phi]}$

* $\id_\Gamma[\sigma] = \id_{\Gamma[\sigma]}$

lem:dt:interact $ $

* $T[\delta][\phi] = T[\phi][\delta[\phi]]$ ($t$, resp.)

* $(\delta \circ \delta') [\phi] = (\delta[\phi]) \circ (\delta'[\phi])$

* $T[\sigma][\phi] = T[\phi][\sigma[\phi]]$ ($\Gamma$, $\delta$, $t$, resp.)

* $T[\delta][\sigma] = T[\sigma][\delta[\sigma]]$ ($t$, resp.)

* $(\delta \circ \delta') [\sigma] = (\delta[\sigma]) \circ (\delta'[\sigma])$

The first two statements are mutually proved. The last two statements are also
mutually proved.

Most of them can be done by simply following the IHs.
We give a few examples.

\begin{align*}
&= \LAM{l}{l'}x{S[\delta][\phi]}{(t[\delta,x/x][\phi])} \\
&= \LAM{l}{l'}x{S[\phi][\delta[\phi]]}{(t[\phi][(\delta,x/x)[\phi]])}
\byIH \\
&= \LAM{l}{l'}x{S[\phi][\delta[\phi]]}{(t[\phi][(\delta[\phi],x/x)])} \\
&= (\LAM{l}{l'}x{S}t)[\phi][\delta[\phi]]
\end{align*}

\begin{align*}
(\ell,g,x_T. M)[\delta][\phi]
&= (\ell,g,x_T. M[\delta,x_T/x_T][\phi,\ell/\ell]) \\
&= (\ell,g,x_T. M[\phi,\ell/\ell][(\delta,x_T/x_T)[\phi,\ell/\ell]])
\byIH \\
&= (\ell,g,x_T. M[\phi,\ell/\ell][(\delta[\phi],x_T/x_T)])
\tag{$\delta[\phi,\ell/\ell] = \delta[\phi]$ due to weakening of universe variables}\\
&= (\ell,g,x_T. M)[\phi][\delta[\phi]]
\end{align*}

\begin{align*}
(\ell,g,u_t,x_t. t_\tEl)[\sigma][\phi]
&= (\ell,g,u_t,x_t. t_\tEl[\sigma,g/g,u_t^\id/u_t][\phi,\ell/\ell]) \\
&= (\ell,g,u_t,x_t. t_\tEl[\phi,\ell/\ell][(\sigma,g/g,u_t^\id/u_t)[\phi,\ell/\ell]])
\byIH \\
&= (\ell,g,u_t,x_t. t_\tEl[\phi,\ell/\ell][(\sigma[\phi],g/g,u_t^\id/u_t)])
\tag{$\sigma$ is universe weakened; \Cref{lem:dt:wkact}} \\
&= (\ell,g,u_t,x_t. t_\tEl)[\phi][\sigma[\phi]]
\end{align*}

\begin{align*}
\wk^k_g[\sigma][\phi]
&= \wk^k_{\sigma(g)}[\phi] \\
&= \wk^k_{\sigma(g)[\phi]}
\tag{by \Cref{lem:dt:wkact}} \\
&= \wk^k_{g[\sigma[\phi]]}  \\
&= \wk^k_g[\phi][\sigma[\phi]]
\end{align*}

* Then we consider $\cdot^k_g$, and we case analyze $\Gamma := \sigma(g)$:

* If $\Gamma$ ends with $\cdot$.

\begin{align*}
\cdot^k_g[\sigma][\phi]
= \cdot^{|\Gamma| + m} [\phi] = \cdot^{|\Gamma| + m}
\end{align*}

* If $\Gamma$ ends with $g'$.

\begin{align*}
\cdot^k_g[\sigma][\phi]
= \cdot^{|\Gamma| + m}_{g'} [\phi] = \cdot^{|\Gamma| + m}_{g'}
\end{align*}

\begin{align*}
(\ell,g,u_t,x_t. t_\tEl)[\delta][\sigma]
&= (\ell,g,u_t,x_t. t_\tEl[\delta,x_t/x_t][\sigma,u_t^\id/u_t]) \\
&= (\ell,g,u_t,x_t. t_\tEl[\sigma,u_t^\id/u_t][(\delta,x_t/x_t)[\sigma,u_t^\id/u_t]])
\byIH \\
&= (\ell,g,u_t,x_t. t_\tEl[\sigma,u_t^\id/u_t][\delta[\sigma],x_t/x_t])
\tag{$\delta$ is globally weakened} \\
&= (\ell,g,u_t,x_t. t_\tEl)[\sigma][\delta[\sigma]]
\end{align*}

* Now we consider $\wk^k_g \circ \delta$.
This composition basically cancels out all terms from $\delta$ and leave a
weakening behind.
In this case, we know that $\delta$ must end with $\wk^{k'}_g$ for some $g$.
Moreover, in order to compose, we have that $|\delta| = m$.

\begin{align*}
(\wk^k_g \circ \delta) [\sigma]
&= \wk^{\widehat \delta}_g[\sigma] \\
&= \wk^{k'}_{\sigma(g)}
\end{align*}

\begin{align*}
(\wk^k_g[\sigma]) \circ (\delta[\sigma])
&= \wk^{|\delta|}_{\sigma(g)} \circ (\delta[\sigma]) \\
&= \wk^{k'}_{\sigma(g)}
\tag{$\wk^{|\delta|}_{\sigma(g)}$ projects away all leading terms kept by
$\delta$ so only $\wk^{k'}_{g}[\sigma]$ is left}
\end{align*}

Therefore two expressions are equal.
Similar reasoning holds for the case of $\cdot^k_g \circ \delta$.

* Then we consider $\cdot^k$ and case analyze $\widecheck \delta$.

* If $\widecheck\delta$ is not a contextual variable, then $\delta$ must end
with $\cdot^{k'}$ and also $|\delta| = m$ due to well-typedness.

\begin{align*}
(\cdot^k \circ \delta)[\sigma]
&= \cdot^{\widehat \delta}[\sigma] \\
&= \cdot^{k'} \\
&= \cdot^{k'}[\sigma] \\
&= (\cdot^k[\sigma]) \circ (\delta[\sigma])
\end{align*}

* If $\widecheck\delta$ is contextual variable $g$, then $\delta$ must end
with $\cdot^{k'}_g$ and also $|\delta| = m$ due to well-typedness.

\begin{align*}
(\cdot^k \circ \delta)[\sigma]
&= \cdot^{\widehat \delta}_g[\sigma] \\
&= \cdot^{k'}_g[\sigma]
\end{align*}

\begin{align*}
\cdot^k[\sigma] \circ (\delta[\sigma])
&= \cdot^k \circ (\delta[\sigma]) \\
&= \cdot^{\widehat{\delta[\sigma]}}_{\widecheck{\delta[\sigma]}} \\
&= \cdot^{|\sigma(g)| + k'}_{\widecheck{\delta[\sigma]}}
\end{align*}

Then we consider whether $\sigma(g)$ ends with another contextual variable or

* If $\sigma(g)$ ends with $\cdot$, then

\begin{align*}
(\cdot^k \circ \delta)[\sigma]
&= \cdot^{k'}_g[\sigma] \\
&= \cdot^{|\sigma(g)| + k'}
\end{align*}

and also $\delta[\sigma]$ must also end with no global variable.

* If $\sigma(g)$ ends with some $g'$, then

\begin{align*}
(\cdot^k \circ \delta)[\sigma]
&= \cdot^{k'}_g[\sigma] \\
&= \cdot^{|\sigma(g)| + k'}_{g'}
\end{align*}

Then $\widecheck{\delta[\sigma]}$ must also return $g'$.

$ $

* If $\judge[L']\Psi$ and $\typing[L]\phi{L'}$, then $\judge[L]{\Psi[\phi]}$.

* If $\lpjudge[\Psi][L']i\Gamma$ and $\typing[L]\phi{L'}$, then $\lpjudge[\Psi[\phi]]i{\Gamma[\phi]}$.

* If $\lpequiv[\Psi][L']i\Gamma\Delta$ and $\typing[L]\phi{L'}$, then $\lpequiv[\Psi[\phi]]i{\Gamma[\phi]}{\Delta[\phi]}$.

* If $\lttypwf[\Psi][\Gamma][L']i T l$ and $\typing[L]\phi{L'}$, then
$\lttypwf[\Psi[\phi]][\Gamma[\phi]] i{T[\phi]}{l[\phi]}$.

* If $\lttypeq[\Psi][\Gamma][L']i T{T'} l$ and $\typing[L]\phi{L'}$, then
$\lttypeq[\Psi[\phi]][\Gamma[\phi]] i{T[\phi]}{T'[\phi]} {l[\phi]}$.

* If $\lttyping[\Psi][\Gamma][L']i t T l$ and $\typing[L]\phi{L'}$, then
$\lttyping[\Psi[\phi]][\Gamma[\phi]] i{t[\phi]}{T[\phi]} {l[\phi]}$.

* If $\lttyequiv[\Psi][\Gamma][L']i t{t'} T l$ and $\typing[L]\phi{L'}$, then
$\lttyequiv[\Psi[\phi]][\Gamma[\phi]] i{t[\phi]}{t'[\phi]}{T[\phi]} {l[\phi]}$.

* If $\ltsubst[\Psi][\Gamma][L'] i{\delta}{\Gamma'}$ and $\typing[L]\phi{L'}$, then
$\ltsubst[\Psi[\phi]][\Gamma[\phi]] i{\delta[\phi]}{\Gamma'[\phi]}$.

* If $\ltsubeq[\Psi][\Gamma][L'] i{\delta}{\delta'}{\Gamma'}$ and $\typing[L]\phi{L'}$, then
$\ltsubeq[\Psi[\phi]][\Gamma[\phi]] i{\delta[\phi]}{\delta'[\phi]}{\Gamma'[\phi]}$.

Do a mutual induction. Most rules do not alter the universe context at all so they
are discharged naturally.
When encountering the only changing cases, i.e. universe-polymorphic functions and
branches of the recursive principles for code, we extend the unvierse substitutions
with sufficient new universe variables before applying the IHs.
When computation rules are encountered, we apply the composition lemma above before
applying the IHs.

We consider one complex computational rule in detail to illustrate the proof of the

m Γ
[Ψ][L'] p Δ

[Ψ][Δ][L'] c S l
[Ψ][Δ, x : S  @  l][L']cTl'

t = ll'x S T

s_S = l_1l_2M blΔ(S)

s_T = l_1l_2M bl'(Δ, x : S  @  l)(T)
[Ψ][Γ][L'] m t_Π[l/ℓ,l'/ℓ',Δ/g,S/U_S,T/U_T,s_S/x_S,
s_T/x_T]l_1l_2M b(l ⊔l')ΔtM[l⊔l'/ℓ,Δ/g,t/x_T]l_1

On the right hand side, $\phi$ simply propagates.
By IH, we can show that all premises with the universe-substituted sub-terms are
For example, we have

\[
\lttypwf[\Psi[\phi]][\Delta[\phi]]c{S[\phi]}{l[\phi]}
\]

\[
\lttypwf[\Psi[\phi]][\Delta[\phi], x : S[\phi] ~@~ {l[\phi]}]c{T[\phi]}{l'[\phi]}
\]

Now we consider the left hand side.

\begin{align*}
& t_\Pi[l/\ell,l'/\ell',\Delta/g,S/U_S,T/U_T,s_S/x_S,
s_T/x_T][\phi] \\
=~ & t_\Pi[l/\ell,l'/\ell'][\phi][\Delta[\phi]/g,S[\phi]/U_S,T[\phi]/U_T,s_S[\phi]/x_S,
\tag{by \Cref{lem:dt:interact}} \\
=~ & t_\Pi[\phi,\ell/\ell,\ell'/\ell'][l[\phi]/\ell,l'[\phi]/\ell'][\Delta[\phi]/g,S[\phi]/U_S,T[\phi]/U_T,s_S[\phi]/x_S,
\tag{by naturality of substitutions}
\end{align*}

Note that $t_\Pi[\phi,\ell/\ell,\ell'/\ell']$ is precisely how $\phi$ should be
propagated in $t_\Pi$.

Now we consider the type.
A similar reasoning applies:

\begin{align*}
M[l \sqcup l'/\ell, \Delta/g,t/x_T][\phi]
&= M[l \sqcup l'/\ell][\phi][\Delta[\phi]/g,t[\phi]/x_T]
\tag{by \Cref{lem:dt:interact}} \\
&= M[\phi,\ell/\ell][l[\phi] \sqcup l'[\phi]/\ell][\Delta[\phi]/g,t[\phi]/x_T]
\tag{by naturality of substitutions}
\end{align*}

This equality verifies the resulting type is correct.
The same rule ensures the equivalence lives in the universe level $l_1[\phi]$.

Then we consider the properties of local substitutions.
lem:dt:presup1 $ $

* If $\lpjudge i \Gamma$, then $\judge[L]\Psi$.

* If $\lpequiv i \Gamma \Delta$, then $\lpjudge i \Gamma$ and $\lpjudge i
\Delta$.

* If $\ltsubst i \delta \Delta$, then $\lpjudge i \Gamma$.

* If $\ltsubeq i{\delta}{\delta'}\Delta$, then $\ltsubst i \delta \Delta$ and
$\ltsubst i{\delta'} \Delta$.

* If $\ptyping \sigma \Phi$, then $\judge[L]\Psi$ and $\judge[L]\Phi$.

Induction on their respective premises. Note that in the second statement, the
definition of $\lpequiv i \Gamma \Delta$ is adjusted so that a simple induction
would suffice.
The third statement requires the extra premises added to the step case of the equivalence judgment.

In fact the lemma above has given full presupposition for local contexts and their
Therefore, in the forthcoming full presupposition lemma, we do not have to state these

$ $

* If $\ltsubeq i{\delta}{\delta'}\Delta$, then $\ltsubeq i{\delta'}{\delta}\Delta$.

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

By induction.

$ $

* If $\lttypwf i T l$, then $\lttypeq i T T l$.

* If $\lttyping i t T l$, then $\lttyequiv i t t T l$.

* If $\ltsubst i \delta \Delta$, then $\ltsubeq i \delta \delta \Delta$.

* If $\lpjudge i \Gamma$, then $\lpequiv i \Gamma \Gamma$.

The first two statements are proved by symmetry and then transitivity.
The third (fourth) statement is a natural consequence of the second (first, resp.) statement.

$ $

* If $\lttypwf[\Psi][\Gamma']i T l$ and $\ltsubst i{\delta}{\Gamma'}$, then
$\lttypwf i{T[\delta]} l$.

* If $\lttypeq[\Psi][\Gamma']i T{T'} l$ and $\ltsubst i{\delta}{\Gamma'}$, then
$\lttypeq i{T[\delta]}{T'[\delta]} l$.

* If $\lttyping[\Psi][\Gamma']i t T l$ and $\ltsubst i{\delta}{\Gamma'}$, then
$\lttyping i{t[\delta]}{T[\delta]} l$.

* If $\lttyequiv[\Psi][\Gamma']i t{t'} T l$ and $\ltsubst i{\delta}{\Gamma'}$, then
$\lttyequiv i{t[\delta]}{t'[\delta]}{T[\delta]} l$.

* If $\ltsubst[\Psi][\Gamma'] i{\delta'}{\Gamma''}$ and $\ltsubst i{\delta}{\Gamma'}$, then
$\ltsubst i{\delta' \circ \delta}{\Gamma''}$.

* If $\ltsubeq[\Psi][\Gamma'] i{\delta'}{\delta''}{\Gamma''}$ and $\ltsubst i{\delta}{\Gamma'}$, then
$\ltsubeq i{\delta' \circ \delta}{\delta'' \circ \delta}{\Gamma''}$.

Do a mutual induction.
Many cases go through naturally if their premises do not alter the local context.
In the base cases, we use partial presupposition above to obtain $\lpjudge i
\Gamma$ and $\judge[L]\Psi$.
The global variable cases depend on the composition of local substitutions.
The local variable case depends on the reflexivity lemma.

We consider a few cases:

[Ψ][Γ'] mtt'U[Δ] ll'T”l ⊔l'
[Ψ][Δ] pTT'l
[Ψ][Γ'] mtTt'T'T”[T/U]l'

\begin{align*}
& \lttyequiv m{t[\delta]}{t'[\delta]}{\TPI U[\Delta] l{l'}{(T''[\delta])}}{\su l
\sqcup l'}
\byIH \\
& \lttyequiv m{\TAPP{t[\delta]}{T}}{\TAPP{t'[\delta]}{T'}}{T''[\delta][T/U]}{l'}
\tag{by the same congruence rule}
\end{align*}

Notice that

\[
T''[\delta][T/U] = T''[T/U][\delta[T/U]] = T''[T/U][\delta]
\]

where the second equation holds because $\delta$ is not typed in a context with

m Γ'
p Δ

[Ψ][Δ] c S l

[Ψ][Δ, x : S  @  l] c tTl'

l_Π= l ⊔l'

T_Π= ll'xST

t' = ll'xSt

s_S = l_1l_2M blΔ(S)[δ]

s_t = l_1l_2M bl'(Δ, x : S  @  l)T(t)[δ]

δ' = s_S/x_S,s_t/x_t
[Ψ][Γ'] mt_λ[l/ℓ,l'/ℓ',Δ/g,S/U_S,T/U_T,t/u_t,δ']l_1l_2M bl_ΠΔT_Πt'M'[l_Π/ℓ,Δ/g,T_Π/U_T,t'/x_t]l_2

In this case, we first apply IHs so that $\delta$ is propagated into all premises
in $G_A$ and we must reason about the left hand side and the result type.

\begin{align*}
& t_\lambda[\delta,x_S/x_S,x_t/x_t][l/\ell,l'/\ell',\Delta/g,S/U_S,T/U_T,t/u_t,\delta'] \\
=~& t_\lambda[l/\ell,l'/\ell',\Delta/g,S/U_S,T/U_T,t/u_t][\delta[l/\ell,l'/\ell',\Delta/g,S/U_S,T/U_T,t/u_t],x_S/x_S,x_t/x_t][\delta']
\tag{by \Cref{lem:dt:interact}} \\
\tag{$\delta$ has no those variables} \\
\tag{naturality of local substitutions}
\end{align*}

On the return type, we have

\begin{align*}
& M'[\delta,x_t/x_t][l_\Pi/\ell,\Delta/g,T_\Pi/U_T,t'/x_t] \\
=~& M'[l_\Pi/\ell,\Delta/g,T_\Pi/U_T][\delta,x_t/x_t][t'/x_t]
\tag{by \Cref{lem:dt:interact} similarly} \\
=~& M'[l_\Pi/\ell,\Delta/g,T_\Pi/U_T][t'/x_t][\delta]
\tag{naturality of local substitutions}
\end{align*}

Both equations conclude this case.

We also need a similar lemma about equivalent local substitutions.
lem:dt:lsubst-eq$ $

* If $\lttypwf[\Psi][\Gamma']i T l$ and $\ltsubeq i{\delta_1}{\delta_2}{\Gamma'}$, then
$\lttypeq i{T[\delta_1]}{T[\delta_2]} l$.

* If $\lttypeq[\Psi][\Gamma']i T{T'} l$ and $\ltsubeq i{\delta_1}{\delta_2}{\Gamma'}$, then
$\lttypeq i{T[\delta_1]}{T'[\delta_2]} l$.

* If $\lttyping[\Psi][\Gamma']i t T l$ and $\ltsubeq i{\delta_1}{\delta_2}{\Gamma'}$, then
$\lttyequiv i{t[\delta_1]}{t[\delta_2]}{T[\delta_1]} l$.

* If $\lttyequiv[\Psi][\Gamma']i t{t'} T l$ and $\ltsubeq i{\delta_1}{\delta_2}{\Gamma'}$, then
$\lttyequiv i{t[\delta_1]}{t'[\delta_2]}{T[\delta_1]} l$.

* If $\ltsubst[\Psi][\Gamma'] i{\delta}{\Gamma''}$ and $\ltsubeq i{\delta_1}{\delta_2}{\Gamma'}$, then
$\ltsubeq i{\delta \circ \delta_1}{\delta \circ \delta_2}{\Gamma''}$.

* If $\ltsubeq[\Psi][\Gamma'] i{\delta}{\delta'}{\Gamma''}$ and $\ltsubeq i{\delta_1}{\delta_2}{\Gamma'}$, then
$\ltsubeq i{\delta \circ \delta_1}{\delta' \circ \delta_2}{\Gamma''}$.

We proceed by mutual induction.
When we encounter well-formedness of types and well-typedness of terms, we conclude
by IHs and respective congruence rules.
What is more difficult are the asymmetric equivalence rules.
We must apply IHs a bit more carefully to obtain the conclusions.
We elaborate on a few cases.

[Ψ][Γ'] i tt'T l
[Ψ][Γ'] it't”T l
[Ψ][Γ'] i tt”T l

\begin{align*}
& \ltsubst i{\delta_1}{\Gamma'}
\tag{by presupposition} \\
& \lttyequiv i {t[\delta_1]}{t'[\delta_1]}{T[\delta_1]} l
\tag{by local substitution lemma} \\
& \lttyequiv i{t'[\delta_1]}{t''[\delta_2]}{T[\delta_1]} l
\byIH \\
& \lttyequiv i {t[\delta_1]}{t''[\delta_2]}{T[\delta_1]} l
\tag{by transitivity}
\end{align*}

[Ψ][Γ'] i tT'l
[Ψ][Γ'] i t T l

\begin{align*}
& \ltsubst i{\delta_1}{\Gamma'}
\tag{by presupposition} \\
& \lttypeq{\typeof i}{T[\delta_1]}{T'[\delta_1]}l
\tag{by local substitution lemma} \\
& \lttyequiv i {t[\delta_1]}{t[\delta_2]}{T'[\delta_1]}l
\byIH \\
& \lttyequiv i {t[\delta_1]}{t[\delta_2]}{T[\delta_1]}l
\tag{by conversion}
\end{align*}

[Ψ, U : [Δ] p l][Γ']mtT'l'
[Ψ][Δ] pT l
[Ψ][Γ'] mt[T/U](ll'U t)TT'[T/U]l'

\begin{align*}
& \ltsubst m{\delta_1}{\Gamma'}
\tag{by presupposition} \\
& \lttyequiv m{t[T/U][\delta_1]}{\TAPP{(\TLAM{l}{l'}U
\tag{by local substitution lemma} \\
& \lttyequiv[\Psi, U : \DTyp[\Delta] p
\byIH \\
& \lttyequiv m{\TAPP{(\TLAM{l}{l'}U {t[\delta_1]})}{T}}{\TAPP{(\TLAM{l}{l'}U
\tag{by congruence; note that $T'[T/U][\delta_1] = T'[\delta_1][T/U]$ as
$U$ is not in $\delta_1$} \\
& \lttyequiv m{t[T/U][\delta_1]}{\TAPP{(\TLAM{l}{l'}U
\tag{by transitivity}
\end{align*}

p Δ

[Ψ][Δ]c T l

[Ψ][Γ',x_T : [Δ]l  @ l]mMl'

[Ψ, U : [Δ]c l][Γ']mt'M[U/x_T]l'
[Ψ][Γ'] mt'[T/U]l'l Δx_T.MU.t'(T)M[T/x_T]l'

\begin{align*}
& \ltsubst m{\delta_1}{\Gamma'}
\tag{by presupposition} \\
& \lpjudge m{\Gamma}
\tag{by presupposition} \\
& \lttyequiv m{t'[T/U][\delta_1]}{\LETBTYP{l'}l
\Delta{x_T.M[\delta_1,x_T/x_T]}{U.t'[\delta_1]}{(\boxit T)}}{M[\boxit
\tag{by local substitution lemma} \\
& \lttypeq[\Psi][\Gamma,x_T : \CTyp[\Delta]l ~@~{\su
\byIH \\
& \lttyequiv[\Psi, U : \DTyp[\Delta]c
l]m{t'[\delta_1]}{t'[\delta_2]}{M[\delta_1,x_T/x_T][\boxit U/x_T]}{l'}
\byIH \\
& \quad {\LETBTYP{l'}l
\Delta{x_T.M[\delta_1,x_T/x_T]}{U.t'[\delta_1]}{(\boxit T)}} \\
& \approx {\LETBTYP{l'}l
\Delta{x_T.M[\delta_2,x_T/x_T]}{U.t'[\delta_2]}{(\boxit T)}}:
{M[\delta_1,x_T/x_T][\boxit T/x_T]}
\tag{by congruence} \\
& \lttyequiv m{t'[T/U][\delta_1]}{\LETBTYP{l'}l
\Delta{x_T.M[\delta_2,x_T/x_T]}{U.t'[\delta_2]}{(\boxit T)}}{M[\delta_1,x_T/x_T][\boxit
\tag{by transitivity}
\end{align*}

* Finally we consider a $\eta$ rule.

[Ψ][Γ'] mtg l Tl
[Ψ][Γ'] ml g (t g)tg l Tl

\begin{align*}
& \ltsubst m{\delta_1}{\Gamma'}
\tag{by presupposition} \\
& \lttyping m{t[\delta_1]}{\CPI g l{(T[\delta_1])}}{l}
\tag{by local substitution lemma} \\
& \lttyequiv m{\CLAM l g {(\CAPP{(t[\delta_1])} g)}}{t[\delta_1]}{\CPI g l{(T[\delta_1])}}{l}
\tag{by the same $\eta$ rule} \\
& \lttyequiv m{t[\delta_1]}{t[\delta_2]}{\CPI g l{(T[\delta_1])}}{l}
\byIH \\
& \lttyequiv m{\CLAM l g {(\CAPP{(t[\delta_1])} g)}}{t[\delta_2]}{\CPI g
\tag{by transitivity}
\end{align*}

Note that the statement of this lemma is left-biased.
For example, when considering terms, the types are substituted by $\delta_1$.
This bias causes the whole formulation of equivalence judgment between terms to be
left biased as well.
Otherwise, this lemma cannot be easily justified as above and requires the global
substitution lemma, which definitely causes issues as the latter depends on this
very lemma in the global variable cases.

A visible effect of this left bias is especially evident in the computation rules.
For example, if we define the following $\beta$ rule instead, then the lemma above
suddenly becomes unprovable at this stage:

[Ψ, U : [Δ] p l][Γ']mtT'l'
[Ψ][Δ] pT l
[Ψ][Γ'] m(ll'U t)Tt[T/U]T'[T/U]l'

Let us work on the proof to see what happens.
We now must prove

\[
\lttyequiv m{\TAPP{(\TLAM{l}{l'}U{(t[\delta_1])})}{T}}{t[T/U][\delta_2]}{T'[T/U][\delta_1]}{l'}
\]

The only way to introduce $\delta_2$ on the right hand side now is to apply the
local substitution lemma, which yields

\[
\lttyequiv
\]

Notice that the return type yields a local substitution $\delta_2$, instead of
$\delta_1$ as required by the goal.
At this stage, however, we are not able to prove the equivalence between
$T'[T/U][\delta_1]$ and $T'[T/U][\delta_2]$ as we are missing the global
substitution lemma to justify that $T'[T/U]$ remains well-formed.

Similarly, we are not able to prove a lemma if some $\eta$ rules are flipped
Consider the following “innocent” $\eta$ rule:

[Ψ][Γ'] mtg l Tl
[Ψ][Γ'] mtl g (t g)g l Tl

Since there is only one premise, we have no choice but to eventually use IH to

\[
\lttyequiv m{t[\delta_1]}{t[\delta_2]}{\CPI g l{(T[\delta_1])}}{l}
\]

This leaves us to prove

\[
\lttyequiv m{t[\delta_2]}{\CLAM l g {(\CAPP{(t[\delta_2])} g)}}{\CPI g l {(T[{\color{red}\delta_1}])}}{l}
\]

Notice how the equivalence itself talks about $\delta_2$ exclusively while the type
refers to $\delta_1$.
This asymmetry forces us to flip the equivalence to obtain a better proof.

Then we move on to the global substitution lemma.
We must first establish a number of other lemmas.
The lifting lemma is one of the guiding lemmas of the layering principle, where we
require that well-formedness can be carried over to higher layers.
lem:dt:lift If $i \le i'$, and

* $\lpjudge i \Gamma$, then $\lpjudge{i'} \Gamma$;

* $\lpequiv i \Gamma \Delta$, then $\lpequiv{i'} \Gamma \Delta$;

* $\lttypwf i T l$, then $\lttypwf{i'} T l$;

* $\lttypeq i T{T'} l$, then $\lttypeq{i'} T{T'} l$;

* $\lttyping i t T l$, then $\lttyping{i'} t T l$.

* $\lttyequiv i t{t'} T l$, then $\lttyequiv{i'} t{t'} T l$;

* $\ltsubst i{\delta}{\Delta}$, then $\ltsubst{i'}{\delta}{\Delta}$;

* $\ltsubeq i{\delta}{\delta'}{\Delta}$, then $\ltsubeq{i'}{\delta}{\delta'}{\Delta}$.

First, we realize that the $\ttypeof$ function is monotonic, i.e. $\typeof i \le
\typeof{i'}$.
We proceed by a mutual induction.
Most cases are obvious by IHs.
Notice that there are cases where we have premises like $\lpjudge{\typeof i}
\Gamma$, so we must apply IH to obtain $\lpjudge{\typeof{i'}} \Gamma$ with the
monotonicity property above.
It works similarly for the conversion rule, where we have $\lttypeq{\typeof i}T
{T'} l$.
In the cases of global variables, the transitivity of $\le$ eventually complete the
proof of this lemma.
We elaborate on one case:

u : [Δ]i”T l ∈Ψ
i” ∈{v, c}
i ∈{v, c, p, m}
i” ≤i
i δΔ

\begin{align*}
& \lpjudge{\typeof{i'}}\Gamma
\byIH \\
& \ltsubst{i'} \delta \Delta
\byIH \\
& i'' \le i \le i' \\
& \lttyping{i'}{u^\delta}{T[\delta]}{l}
\tag{by the same rule}
\end{align*}

The inverse of lifting sometimes is possible
$ $

* $\lttypwf p T l$, then $\lttypwf c T l$;

* $\lttyping p t T l$, then $\lttyping c t T l$.

* $\ltsubst p{\delta}{\Delta}$, then $\ltsubst c{\delta}{\Delta}$;

Notice that $\typeof p = \typeof c = p$.

The unlifting lemma says that the typing at layer $p$ can be unlifted back to layer

As another guiding lemma, we have the static code lemma, which states that code at
layer $v$ and $c$ has no computational behavior.
lem:dt:static If $i \in \{v, c\}$,

* $\lttypeq i T{T'} l$, then $T = T'$;

* $\lttyequiv i t{t'} T l$, then $t = t'$;

* $\ltsubeq i{\delta}{\delta'}{\Delta}$, then $\delta = \delta'$.

All equalities above are quotient over the equivalence of universe levels.

Mutual induction.
We are not concerned about the equivalence of types due to the conversion rule.

We emphasize again that the equalities hold modulo the equivalence of universe
For example, $\Ty{\ell \sqcup \ell'}$ and $\Ty{\ell' \sqcup \ell}$ as code are
considered equal, though their universe levels are not exactly syntactically
This is fine as we know how to decide the equality between two universe levels as
shown in <Ref>.

$ $

* If $\lpjudge[\Phi] i \Gamma$, $i \in \{p, m\}$ and $\ptyping{\sigma}{\Phi}$, then $\lpjudge i {\Gamma[\sigma]}$.

* If $\lpequiv[\Phi] i \Gamma \Delta$, $i \in \{p, m\}$ and $\ptyping{\sigma}{\Phi}$, then $\lpequiv i {\Gamma[\sigma]}{\Delta[\sigma]}$.

* If $\lttypwf[\Phi]i T l$ and $\ptyping\sigma\Phi$, then
$\lttypwf[\Psi][\Gamma[\sigma]] i{T[\sigma]} l$.

* If $\lttypeq[\Phi]i T{T'} l$ and $\ptyping\sigma\Phi$, then
$\lttypeq[\Psi][\Gamma[\sigma]] i{T[\sigma]}{T'[\sigma]} l$.

* If $\lttyping[\Phi]i t T l$ and $\ptyping\sigma\Phi$, then
$\lttyping[\Psi][\Gamma[\sigma]] i{t[\sigma]}{T[\sigma]} l$.

* If $\lttyequiv[\Phi]i t{t'} T l$ and $\ptyping\sigma\Phi$, then
$\lttyequiv[\Psi][\Gamma[\sigma]] i{t[\sigma]}{t'[\sigma]}{T[\sigma]} l$.

* If $\ltsubst[\Phi] i{\delta}{\Delta}$ and $\ptyping\sigma\Phi$, then
$\ltsubst[\Psi][\Gamma[\sigma]] i{\delta[\sigma]}{\Delta[\sigma]}$.

* If $\ltsubeq[\Phi] i{\delta}{\delta'}{\Delta}$ and $\ptyping\sigma\Phi$, then
$\ltsubeq[\Psi][\Gamma[\sigma]] i{\delta[\sigma]}{\delta'[\sigma]}{\Delta[\sigma]}$.

We proceed by a mutual induction.
Notice that in the first two statements, $i \in \{p, m\}$, namely the range of the
$\ttypeof$ function.
This ensures a lookup $\sigma(g)$ of a contextual variable $g$ to be well-formed at
layer $i$, due to <Ref>.
Most cases can be discharged by IHs directly.
The complex cases are the computation rules and the global variable cases.

We consider a few cases:

u : [Δ]i'T l ∈Φ
i' ∈{v, c}
i ∈{v, c, p, m}
i' ≤i
[Φ] i δδ' Δ
[Φ] iu^δu^δ'T[δ]l

\begin{align*}
& \lttyping[\Psi][\Delta[\sigma]]{i'}{\sigma(u)}{T[\sigma]}l
\tag{by lookup} \\
& \lttyping[\Psi][\Delta[\sigma]]{i}{\sigma(u)}{T[\sigma]}l
\tag{by lifting} \\
& \ltsubeq[\Psi][\Gamma[\sigma]] i
\byIH \\
\lttyequiv[\Psi][\Gamma[\sigma]]{i}{\sigma(u)[\delta[\sigma]]}{\sigma(u)[\delta'[\sigma]]}{T[\sigma][\delta[\sigma]]}l
\tag{by equivalent local substitution lemma}
\end{align*}

Notice that

\[
T[\sigma][\delta[\sigma]] = T[\delta][\sigma]
\]

[Φ] mtt'ℓl Tω
|ℓ| = |l| = |l'| > 0

∀0 ≤n < |l| ·[L]l(n)l'(n)
[Φ] mt $ lt' $ l'T[l/ℓ]l[l/ℓ]

\begin{align*}
& \lttyequiv[\Psi][\Gamma[\sigma]] m{t[\sigma]}{t'[\sigma]}{\UPI \ell l{(T[\sigma])}}{\omega}
\byIH \\
& \lttyequiv[\Psi][\Gamma[\sigma]] m{(t[\sigma])~\$~\vect l}{(t'[\sigma])~\$~\vect l'}{T[\sigma][\vect l/\vect \ell]}{l[\vect l/\vect \ell]}
\end{align*}

Note that

\[
T[\sigma][\vect l/\vect \ell] = T[\vect l/\vect \ell][\sigma[\vect l/\vect \ell]] = T[\vect l/\vect \ell][\sigma]
\]

because all $\vect\ell$ do not occur in $\sigma$.

[Φ] p Δ

[Φ][Δ] c S l
[Φ][Δ, x : S  @  l]cTl'

t = ll'x S T

s_S = l_1l_2M blΔ(S)

s_T = l_1l_2M bl'(Δ, x : S  @  l)(T)
[Φ] m t_Π[l/ℓ,l'/ℓ',Δ/g,S/U_S,T/U_T,s_S/x_S,
s_T/x_T]l_1l_2M b(l ⊔l')ΔtM[l⊔l'/ℓ,Δ/g,t/x_T]l_1

We first proceed by using IHs on the premises, which include the following

\begin{align*}
& \lpjudge p {\Delta[\sigma]} \\
& \lttypwf[\Psi][\Delta[\sigma]] c{S[\sigma]} l  \\
& \lttypwf[\Psi][\Delta[\sigma], x : S[\sigma] ~@~ l]c{T[\sigma]}{l'}
\end{align*}

By using the same $\beta$ rule, we must check the resulting left hand side and the
result type are equal to the target goal.
Let us first consider the left hand side:

\begin{align*}
& t_\Pi[\sigma,g/g,U_S^\id/U_S,U_T^\id/U_T][l/\ell,l'/\ell',\Delta[\sigma]/g,S[\sigma]/U_S,T[\sigma]/U_T,s_S[\sigma]/x_S,
s_T[\sigma]/x_T] \\
=~& t_\Pi[l/\ell,l'/\ell'][\sigma,g/g,U_S^\id/U_S,U_T^\id/U_T][\Delta[\sigma]/g,S[\sigma]/U_S,T[\sigma]/U_T,s_S[\sigma]/x_S,
\tag{by \Cref{lem:dt:interact}; $\ell$ and $\ell'$ do not occur in $\sigma$}\\
=~& t_\Pi[l/\ell,l'/\ell'][\sigma,\Delta[\sigma]/g,S[\sigma]/U_S,T[\sigma]/U_T][s_S[\sigma]/x_S,
s_T[\sigma]/x_T] \\
=~& t_\Pi[l/\ell,l'/\ell'][\Delta/g,S/U_S,T/U_T][\sigma][s_S[\sigma]/x_S,
\tag{by naturality} \\
=~& t_\Pi[l/\ell,l'/\ell'][\Delta/g,S/U_S,T/U_T][s_S/x_S, s_T/x_T][\sigma]
\tag{by \Cref{lem:dt:interact}}
\end{align*}

Then we consider the result type in a similar way:

\begin{align*}
& M[\sigma,g/g][l\sqcup l'/\ell,\Delta[\sigma]/g,t[\sigma]/x_T] \\
=~& M[l\sqcup l'/\ell][\sigma,g/g][\Delta[\sigma]/g,t[\sigma]/x_T] \\
=~& M[l\sqcup l'/\ell][\Delta/g][\sigma][t[\sigma]/x_T] \\
=~& M[l\sqcup l'/\ell][\Delta/g][t/x_T][\sigma]
\end{align*}

Both equations allow us to conclude the goal.

Next, we consider the effect of equivalent global substitutions on the judgments.
We first define the equivalence relation between global substitutions:

[L] Ψ

p ΓΔ
σ, Γ/gσ', Δ/gΦ, g:

[Φ] p Γ
i ∈{c, p}

[Ψ][Γ[σ]] iTl
[Ψ][Γ[σ]] iT'l

[Ψ][Γ[σ]] iTT'l
σ, T/Uσ', T'/UΦ, u : i l

[Φ] p T l

i ∈{v, c}
[Ψ][Γ[σ]] i tT[σ]l

[Ψ][Γ[σ]] it'T[σ]l

[Ψ][Γ[σ]] i tt'T[σ]l
[Ψ]σ, t/uσ', t'/uΦ, u : i T l

We can then consider similar properties of this equivalence relation.

If $\ptyequiv{\sigma}{\sigma'}{\Phi}$, then $\ptyping{\sigma}{\Phi}$ and $\ptyping{\sigma'}{\Phi}$.

lem:dt:gsubst-eq$ $

* If $\lpjudge[\Phi] i \Gamma$, $i \in \{p, m\}$ and $\ptyequiv{\sigma}{\sigma'}{\Phi}$, then $\lpequiv i {\Gamma[\sigma]}{\Gamma[\sigma']}$.

* If $\lpequiv[\Phi] i \Gamma \Delta$, $i \in \{p, m\}$ and $\ptyequiv{\sigma}{\sigma'}{\Phi}$, then $\lpequiv i {\Gamma[\sigma]}{\Delta[\sigma']}$.

* If $\lttypwf[\Phi]i T l$ and $\ptyequiv{\sigma}{\sigma'}{\Phi}$, then
$\lttypeq[\Psi][\Gamma[\sigma]] i{T[\sigma]}{T[\sigma']} l$.

* If $\lttypeq[\Phi]i T{T'} l$ and $\ptyequiv{\sigma}{\sigma'}{\Phi}$, then
$\lttypeq[\Psi][\Gamma[\sigma]] i{T[\sigma]}{T'[\sigma']} l$.

* If $\lttyping[\Phi]i t T l$ and $\ptyequiv{\sigma}{\sigma'}{\Phi}$, then
$\lttyequiv[\Psi][\Gamma[\sigma]] i{t[\sigma]}{t[\sigma']}{T[\sigma]} l$.

* If $\lttyequiv[\Phi]i t{t'} T l$ and $\ptyequiv{\sigma}{\sigma'}{\Phi}$, then
$\lttyequiv[\Psi][\Gamma[\sigma]] i{t[\sigma]}{t'[\sigma']}{T[\sigma]} l$.

* If $\ltsubst[\Phi] i{\delta}{\Delta}$ and $\ptyequiv{\sigma}{\sigma'}{\Phi}$, then
$\ltsubeq[\Psi][\Gamma[\sigma]] i{\delta[\sigma]}{\delta[\sigma']}{\Delta[\sigma]}$.

* If $\ltsubeq[\Phi] i{\delta}{\delta'}{\Delta}$ and $\ptyequiv{\sigma}{\sigma'}{\Phi}$, then
$\ltsubeq[\Psi][\Gamma[\sigma]] i{\delta[\sigma]}{\delta'[\sigma']}{\Delta[\sigma]}$.

We apply mutual induction.
This lemma is much less sensitive to the exact statement of rules compared to
Since now we have proved the global substitution lemma, we could use conversion
rules whenever necessary.

At this point, we have concluded that all substitutions are coherent with
well-formedness and typing judgments.
Next, we shall move towards the full presupposition lemma and end our discussion on
syntactic properties with it.

§.§ Context Equivalence and Presupposition

In order to establish presupposition, we must concern ourselves with the asymmetry in
the congruence rules of the equivalence judgments.
Presupposition, intuitively, requires us to show that this asymmetry “does not
This intuition is formalized by the context equivalence lemma.
In fact, we need two such lemmas, as we need to show one for local contexts and one
for global contexts.
In light of that, let us proceed with the lemma for local contexts first.

lem:dt:lctxeq1$ $

* If $\lttypwf[\Psi][\Delta]i T l$ and $\lpequiv{\typeof i}\Delta\Gamma$, then
$\lttypwf i{T} l$.

* If $\lttypeq[\Psi][\Delta]i T{T'} l$ and $\lpequiv{\typeof i}\Delta\Gamma$, then
$\lttypeq i{T}{T'} l$.

* If $\lttyping[\Psi][\Delta]i t T l$ and $\lpequiv{\typeof i}\Delta\Gamma$, then
$\lttyping i{t}{T} l$.

* If $\lttyequiv[\Psi][\Delta]i t{t'} T l$ and $\lpequiv{\typeof i}\Delta\Gamma$, then
$\lttyequiv i{t}{t'}{T} l$.

* If $\ltsubst[\Psi][\Delta] i{\delta}{\Gamma'}$ and $\lpequiv{\typeof i}\Delta\Gamma$, then
$\ltsubst i{\delta}{\Gamma'}$.

* If $\ltsubeq[\Psi][\Delta] i{\delta}{\delta'}{\Gamma'}$ and $\lpequiv{\typeof i}\Delta\Gamma$, then
$\ltsubeq i{\delta}{\delta'}{\Gamma'}$.

We start by mutual induction.
The base case is the local variable cases, where we simply apply the conversion rule
to the equivalence given by $\lpequiv{\typeof i}\Delta\Gamma$.
We might also use presupposition (<Ref>) to derive $\lpjudge{\typeof
Otherwise, most cases can be handled by IHs.
In cases where local contexts are extended with variables, we shall carefully use
IHs to obtain the necessary premises to extend the equivalence of $\Delta$ and
$\Gamma$ as well.

We consider a few cases:

[Ψ][Δ] i Sl_1
[Ψ][Δ] i

[Ψ][Δ, x : S  @  l_1] i tt'Tl_2
[Ψ][Δ] il_1l_2 x S tl_3l_4 xS't'll' x S Tl ⊔l'

In this case, the crucial part is to be able to invoke IH on $t \approx t'$.
We proceed as follows:

\begin{align*}
& \lttypwf i S{l_1}
\byIH \\
& \lpequiv{\typeof i}{\Delta, x : S ~@~ {l_1}}{\Gamma, x : S ~@~ {l_1}}
\tag{by lifting and step case of the equivalence} \\
& \lttyequiv[\Psi][\Gamma, x : S ~@~ {l_1}] i t{t'}{T}{l_2}
\byIH
\end{align*}

Then IHs will allow us to conclude the rest.

m Δ

[Ψ][Δ']c T l

[Ψ][Δ,x_T : [Δ']l  @ l]mMl'

[Ψ, U : [Δ']c l][Δ]mt'M[U/x_T]l'
[Ψ][Δ] mt'[T/U]l'lΔ'x_T.MU.t'(T)M[T/x_T]l'

\begin{align*}
& \lpjudge m \Gamma
\tag{by presupposition (\Cref{lem:dt:presup1})} \\
& \lpequiv m{\Delta,x_T : \CTyp[\Delta']l ~@~{\su l}}{\Gamma,x_T :
\CTyp[\Delta']l ~@~{\su l}}
\tag{note that well-formedness of $\CTyp[\Delta']l$ does not depend on
$\Delta$ or $\Gamma$} \\
& \lttypwf[\Psi][\Gamma,x_T : \CTyp[\Delta']l ~@~{\su l}]m{M}{l'}
\byIH \\
& \lpequiv[\Psi, U : \DTyp[\Delta']c l] m{\Delta}{\Gamma}
\tag{by global weakening} \\
& \lttyping[\Psi, U : \DTyp[\Delta']c l]m{t'}{M[\boxit U/x_T]}{l'}
\byIH \\
& \lttyequiv m{t'[T/U]}{\LETBTYP{l'}l{\Delta'}{x_T.M}{U.t'}{(\boxit T)}}{M[\boxit T/x_T]}{l'}
\end{align*}

As a corollary, we can prove the following lemma.
$ $

* If $\lpequiv i \Gamma \Delta$, then $\lpequiv i \Delta \Gamma$.

* If $\lpequiv i{\Gamma_1}{\Gamma_2}$ and $\lpequiv i{\Gamma_2}{\Gamma_3}$, then
$\lpequiv i{\Gamma_1}{\Gamma_3}$.

Induction. Note that transitivity replies on the local context equivalence lemma.

A similar lemma replaces the codomain local contexts of local substitutions.
This variant is much simpler just by conversion rules.
lem:dt:lctxeq2 $ $

* If $\ltsubst i{\delta}{\Gamma'}$ and $\lpequiv{\typeof i}{\Gamma'}{\Delta}$, then
$\ltsubst i{\delta}{\Delta}$.

* If $\ltsubeq i{\delta}{\delta'}{\Gamma'}$ and $\lpequiv{\typeof i}{\Gamma'}{\Delta}$, then
$\ltsubeq i{\delta}{\delta'}{\Delta}$.

By induction. Propagate conversion rules together with the local substitution lemma in the step case.

Then we work on the global context equivalence lemma.
To state this lemma, we should first specify what does that mean for two global
contexts are equivalent.

Ψ, g : Φ, g :

p Γ
[Φ] pΔ
p ΓΔ
i ∈{c, p}
Ψ, U : i lΦ, U : [Δ] i l

p T l
[Φ][Δ] pT' l
p TT' l
i ∈{v, c}
Ψ, u : i T lΦ, u : [Δ] iT' l

Essentially, the equivalence of global contexts are just point-wise equivalence of
types within.
We can reconstruct the well-formedness of both components from the premises:
If $\gequiv \Psi\Phi$, then $\judge[L]\Psi$ and $\judge[L]\Phi$.

For the global context equivalence lemma, we would like to take a shortcut by taking
advantage of the global substitution lemma.
If $\lpequiv{\typeof i}\Gamma \Delta$, then $\ltsubst i{\id}\Delta$.

If $\gequiv \Psi\Phi$, then $\ptyping{\id}\Phi$.

We proceed by induction.
In each step case, notice that weakening is used implicitly.
Use <Ref> to derive $\ltsubst p{\id}\Delta$ whenever necessary.

$ $

* If $\lpjudge[\Phi] i \Gamma$ and $\gequiv\Phi\Psi$, then $\lpjudge i {\Gamma}$.

* If $\lpequiv[\Phi] i \Gamma \Delta$ and $\gequiv\Phi\Psi$, then $\lpequiv i {\Gamma}{\Delta}$.

* If $\lttypwf[\Phi]i T l$ and $\gequiv\Phi\Psi$, then
$\lttypwf[\Psi][\Gamma] i{T} l$.

* If $\lttypeq[\Phi]i T{T'} l$ and $\gequiv\Phi\Psi$, then
$\lttypeq[\Psi][\Gamma] i{T}{T'} l$.

* If $\lttyping[\Phi]i t T l$ and $\gequiv\Phi\Psi$, then
$\lttyping[\Psi][\Gamma] i{t}{T} l$.

* If $\lttyequiv[\Phi]i t{t'} T l$ and $\gequiv\Phi\Psi$, then
$\lttyequiv[\Psi][\Gamma] i{t}{t'}{T} l$.

* If $\ltsubst[\Phi] i{\delta}{\Delta}$ and $\gequiv\Phi\Psi$, then
$\ltsubst[\Psi][\Gamma] i{\delta}{\Delta}$.

* If $\ltsubeq[\Phi] i{\delta}{\delta'}{\Delta}$ and $\gequiv\Phi\Psi$, then
$\ltsubeq[\Psi][\Gamma] i{\delta}{\delta'}{\Delta}$.

We have $\ptyping\id\Phi$ due to <Ref>.
Then by the global substitution lemma, we have our goal by knowing that a global
identity substitution $\id$ does no action.

Finally, we prove the presupposition lemma, which is the last guiding lemma of the
layering principle.
$ $

* If $\lttypwf i T l$, then $\lpjudge{\typeof i}\Gamma$ and $\typing[L]l\Level$ or $i = m \wedge l = \omega$.

* If $\lttypeq i T{T'} l$, then $\lpjudge{\typeof i}\Gamma$, $\lttypwf i T l$,
$\lttypwf i{T'}l$ and $\typing[L]l\Level$ or $i = m \wedge l = \omega$.

* If $\lttyping i t T l$, then $\lpjudge{\typeof i}\Gamma$, $\lttypwf{\typeof i} T l$
and $\typing[L]l\Level$ or $i = m \wedge l = \omega$.

* If $\lttyequiv i t{t'} T l$, then $\lpjudge{\typeof i}\Gamma$, $\lttyping i t
T l$, $\lttyping i{t'} T l$, $\lttypwf{\typeof i} T l$
and $\typing[L]l\Level$ or $i = m \wedge l = \omega$.

* If $\ltsubst i{\delta}{\Delta}$, then $\lpjudge{\typeof i}\Delta$.

* If $\ltsubeq i{\delta}{\delta'}{\Gamma'}$, then $\lpjudge{\typeof i}\Delta$.

Notice that in the statement of the lemma, we sometimes conclude $i = m \wedge l =
\omega$.
The only occasion when $\omega$ is used is when universe polymorphic functions are
In that case, we know for sure that $i = m$.
In any other cases, we obtain $\typing[L]l\Level$, which excludes $l = \omega$.

We proceed by a mutual induction.
In certain congruence rules, we must apply
<Ref> to resolve the asymmetry in the rules.
Otherwise, we simply apply the substitution lemmas whenever necessary.
Note that our rules are stated with redundant premises to make sure this lemma
eventually checks out.

mtt'U[Δ] ll'T”l ⊔l'
[Ψ][Δ] pTT'l

\begin{align*}
& \lttyping m{t}{\TPI U[\Delta] l{l'}{T''}}{\su l \sqcup l'}
\byIH \\
& \lttyping m{t'}{\TPI U[\Delta] l{l'}{T''}}{\su l \sqcup l'}
\byIH \\
& \lttypwf[\Psi][\Delta] p{T}l
\byIH \\
& \lttypwf[\Psi][\Delta] p{T'}l
\byIH \\
& \lttyping m{\TAPP{t'}{T'}}{T''[T'/U]}{l'} \\
& \lttypwf m{\TPI U[\Delta] l{l'}{T''}}{\su l \sqcup l'}
\byIH \\
& \lttypwf[\Psi, U : \DTyp[\Delta] p l] m{T''}{l'}
\tag{by inversion}
\end{align*}

Notice that

\[
T/U \approx T'/U
\]

We then have the goal by <Ref>.

§.§ Coverage and Progress of Recursive Principles

Before moving to the semantics, let us pause a second and think about the recursive
principles: is it guaranteed to always pick a case from the branches?
In this section, we would like to positively answer this question.
The ingredient lies in the typing judgment at layer $c$ and how the recursive
principle is formulated.
Recall that the recursive principle for code of terms is

p Δ
[Ψ][Δ]p Tl'

m t[Δ]Tl'l'
m l_1l_2M bl'ΔT tM'[l'/ℓ,Δ/g,T/U_T,t/x_t]l_2

In this rule, we see that the type of $t$ is indexed by $l$, $\Delta$ and $T$, both of
which live at layer $p$.
When $t = \boxit{t'}$, then $t'$ must be typed at layer $c$.
Then coverage is provided by the exhaustiveness of the branches which should enumerate
all possible types and terms at layer $c$.
This is simple as we simply check the syntax at layer $c$ and can confirm that the
branches are indeed exhaustive.
Progress, on the other hand, requires both $\Delta$ and $T$ are in the right form
prescribed by the $\beta$ rules.
For example, the following rule gives the $\beta$ rule for the $\Nat$ case as a term:

m Γ
p Δ
l =
m t'_[Δ/g]l_1l_2M blΔ()M'[l/ℓ,Δ/g,/U_T,/x_t]l_2

where $T = \Ty\ze$ is required.
In this section, we show that when $t= \boxit{t'}$ where $t'$ is of some concrete form
prescribed by a $\beta$ rule, then the indices must have the right form.

We first consider the well-formed types at layer $c$:

If $\lttypwf c \Nat l$, then $\tyequiv[L]{l}{\ze}\Level$.

By induction. The only applicable rules are the well-formedness rule and the
conversion rule.

Similar lemmas can be stated and proved.

If $\lttypwf c{\PI l{l'}x S T}{l''}$, then $\lttypwf c S{l}$ and
$\lttypwf[\Psi][\Gamma, x : S ~@~ l] c T{l'}$ and they are sub-derivations of the
assumption; moreover, $\tyequiv[L]{l''}{l \sqcup l'}\Level$.

That the judgments in the conclusion are sub-derivations ensures the well-foundedness
of the recursion.
Effectively, the recursive principles recurse on the structures of the typing
derivations, so they are the most general principles that can be formulated on top the
syntax of MLTT.

If $\lttypwf c{\Elt l t}{l'}$, then $\lttyping c t{\Ty l}{\su l}$ as a
sub-derivation and $\tyequiv[L]{l'}{l}\Level$.

If $\lttypwf c{\Ty l}{l'}$, then $\tyequiv[L]{l'}{\su l}\Level$.

Now we have exhausted all possible cases for types, so we move on to terms.

If $\lttyping c x T l$, then $x : T' ~@~{l'} \in \Gamma$ and $\lttypeq p{T}{T'}{l}$
and $\tyequiv[L]{l}{l'}\Level$.

The statement of lemmas for terms need to also consider the equivalence of types.
The equivalence of types is implicitly handled by when evaluating the recursive
principles: since the equivalence is at layer $p$, computation applies, so the
equivalence can be acknowledged by the conversion checking algorithm.

If $\lttyping c \Nat{T}{l}$, then $\lttypeq p{T}{\Ty \ze}{l}$ and $\tyequiv[L]{l}{\su \ze}\Level$.

If $\lttyping c{\PI l{l'}x s t}{T}{l''}$, then as sub-derivations $\lttyping c s{\Ty
l}{\su l}$ and
$\lttyping[\Psi][\Gamma, x : \Elt l s ~@~ l] c{t}{\Ty{l'}}{\su{l'}}$, $\lttypeq
p{T}{\Ty{l \sqcup l'}}{l''}$ and $\tyequiv[L]{l''}{\su{(l \sqcup l')}}\Level$.

If $\lttyping c{\Ty l}{T}{l'}$, then $\lttypeq p{T}{\Ty{\su l}}{l'}$ and
$\tyequiv[L]{l'}{\su{(\su l)}}\Level$.

If $\lttyping c \ze T l$, then $\lttypeq p{T}{\Nat}{\ze}$
and $\tyequiv[L]{l}{\ze}\Level$.

If $\lttyping c{\su t}{T}{l}$, then as a sub-derivation $\lttyping c t{\Nat}{\ze}$,
$\lttypeq p{T}{\Nat}{\ze}$ and

If $\lttyping c{\ELIMN l{x.M}{s}{x,y.s'}t}{T}{l'}$, then as sub-derivations

* $\lttypwf[\Psi][\Gamma, x : \Nat ~@~ \ze] c M l$,

* $\lttyping c s {M[\ze/x]}l$,

* $\lttyping[\Psi][\Gamma, x : \Nat ~@~ \ze, y : M ~@~ l] c {s'}{M[\su x/x]}l$

* $\lttyping c t \Nat \ze$;

moreover $\lttypeq p{T}{M[t/x]}{l'}$ and

If $\lttyping c{\LAM{l}{l'}x S t}{T'}{l''}$, then as sub-derivations

* $\lttypwf c S l$,

* $\lttyping[\Psi][\Gamma, x : S ~@~ l] c t{T}{l'}$;

moreover $\lttypeq p{T'}{\PI{l}{l'}x S T}{l''}$ and
$\tyequiv[L]{l''}{l \sqcup l'}\Level$.

Notice that in this case, we do not have the well-formedness of $T$ as a
This is reflected in the premises for the $t_\lambda$ branch that the global variable $U_T$
representing $T$ lives at layer $p$.
In general, a global assumption can live at layer $c$ and have a recursive call only
if it has a sub-derivation in the typing judgment.

If $\lttyping c{\APP t {l}{l'}x S T s}{T'}{l''}$, then as sub-derivations

* $\lttypwf c S l$,

* $\lttypwf[\Psi][\Gamma, x : S ~@~ l] c{T}{l'}$,

* $\lttyping c t{\PI l{l'} x S T}{l \sqcup l'}$,

* $\lttyping c s S l$;

moreover $\lttypeq p{T'}{T[s/x]}{l''}$ and

There is no other possible terms at layer $c$.
These lemmas give us a syntactic account of coverage and progress of the recursive
In the next section, we give a more rigorous semantic account.

§ REDUCTION AND CONVERTIBILITY

We have finished syntactic verification for .
In this section, let us consider its dynamics by providing the reduction rules for
types and terms and the convertibility checking algorithm between two terms.
The reduction relations to be given compute the weak head normal forms for
types and terms, respectively, and are sub-relations for equivalence judgments for
types and terms.
We first give the syntax for weak head normal forms and neutral forms, and then give
the rules for reduction.
We will need the reduction relations to write down the Kripke logical relations in the
next section as well as in the convertibility checking algorithm.

§.§ Weak Head Normal Forms

The following gives the syntax for weak head normal forms and neutral forms for types
and terms.
As usual, we use capital case for types and lower case for terms.

W    :=         ll'x S T l ℓl T
Weak head normal form for types

g l T U ll'T l T l

V     :=        U^δl μNeutral form for types

w    :=        μll'x s t l t ll' x S t
Weak head normal form for terms ($\Nf$)

l ℓt l g t ll' U t T t

μ   :=        x u^δlx.Msx, y.s'μ μll' x S T
s μl
Neutral form for terms ($\Ne$)

μΓμT l'lΓx_T. MU.t'μl'lΓTx_t. Mu.t'μ

l_1l_2MblΓμl_1l_2MblΓ(U^δ) l_1l_2MblΓT μl_1l_2MblΓT (u^δ)

Notice that for the recursive principles, we block on global variables, following

§.§ Reduction Relations

There are two required reduction relations, one for types and one for terms.
The one for types simply compute types from encodings via $\tEl$.
Unlike <cit.> who employed typed reductions, we deliberately
use untyped reductions and use preservation later to make sure the reductions are
This deviation from <cit.> requires us to establish enough
syntactic theorems before hand.
It is particularly important to use untyped reductions because of the way in which the logical relations
relate terms.
We let $\reds$ to be the reflexive transitive closure of $\redd$.

ll l

l ⊔l'll' x s tll' xl sl' t

t t'
lt lt'

The reduction rules for terms are simply the $\beta$ equivalence rules.

lx.Msx,y. s' s

lx.Msx,y. s'(t) s'[t/x,lx.Msx,y. s't/y]

ll' x S t ll' xS T s t[s/x]

(l ℓt) $ l t[l/ℓ]

(l g t)Δ t[Δ/g]

(ll'U t)T t[T/U]

l'l Δx_T.MU.t'(T) t'[T/U]

l'l ΔTx_t.Mu.t'(t) t'[t/u]

The reduction rules for recursors follow the same principle.
We write down only one rule as an example and omit the rest as they are just
$\beta$ rules:

l_1l_2M bΔ() t_[Δ/g]

The congruence rules reduce the terms at the weak head positions to discover further
There are at least one congruence rules for all elimination forms.

t t'
lx.Msx,y. s't lx.Msx,y. s't'

t t'
t ll' xS T s t'll' xS T s

For elimination forms for meta-programming, we have

t t'
t $ l t' $ l

t t'
tΔ t'Δ

t t'
tT t'T

t t'
l'l Δx_T.MU.st l'l Δx_T.MU.st'

t t'
l'l ΔTx_t.Mu.st l'l ΔTx_t.Mu.st'

There are also congruence rules for the recursive principles.
For the recursive principle for code of terms, we choose to reduce the type to weak
head normal form first and then reduce the term itself.
This order is arbitrary and can be flipped.
We simply fix a choice here.

t t'
l_1l_2M bl'Δt l_1l_2M bl'Δt'

T T'
l_1l_2M bl'ΔT t l_1l_2M bl'ΔT't

t t'
l_1l_2M bl'ΔW t l_1l_2M bl'ΔW t'

We first verify the fact that reductions are just sub-relations of the
equivalence judgments:

Given $\compt i$,

* if $\lttypwf i T l$ and $T \redd T'$, then $\lttypeq i T{T'} l$;

* if $\lttyping i t T l$ and $t \redd t'$, then $\lttyequiv i t{t'} T l$.

We proceed by mutual induction on the typing judgments and then invert the reduction
We use $\compt i$ to make sure computation rules are available.
We select a few cases for discussion:

* The following is the only possible rule for types:

[L] l
i tll
il tl

Inversion of $\Elt l t \redd T'$ gives four possible subcases.
We only consider two:

\[
{\Elt{l_1 \sqcup l_2}{\PI {l_1}{l_2} x s t}}\redd{\PI {l_1}{l_2} x{\Elt{l_1} s}{\Elt{l_2} t}}
\]

Then we know

\[
\lttyping i{\PI {l_1}{l_2} x s t}{\Ty l}{\su l}
\]

We further do an inner induction on the typing judgment above after generalizing
$\Ty l$ to some arbitrary $T$.
There are only three cases to consider:

i sl_1l_1
[Ψ][Γ, x : l_1 s  @ l_1] i tl_2l_2
il_1l_2 x s tl_1 ⊔l_2(l_1 ⊔l_2)

Then this case we derive the goal immediately from the $\tEl$ rule for $\Pi$

i l_1l_2 x s tT'l'
i l_1l_2 x s tTl'

In this case, we simply apply the inner IH to obtain the goal.

i l_1l_2 x s t Tl'
i l_1l_2 x s t T l

Similarly, we use the inner IH to obtain the goal.

In general, when we know the form of a term, an inner induction must reveal only
three cases to consider.
This pattern appears a lot when we consider cases for types.

* We have this case

t t'
lt lt'

Then by IH, we have

\[
\lttyequiv i t{t'}{\Ty l}{\su l}
\]

We obtain the goal by the congruence rule for $\tEl$.

i tT'l
i t T l

By IH, we have

\[
\lttyequiv i{t}{t'}{T'}l
\]

We obtain the goal by the conversion rule.

i tTl'
i t T l

By IH, we have

\[
\lttyequiv i{t}{t'}{T}{l'}
\]

We obtain the goal by the conversion rule.

* For the recursive principle for natural numbers, there are three subcases after
inverting the reduction premise.
We apply $\beta$ rules or the congruence rule properly.

The same principle applies for the recursive principles for code, but a bit more
We will use theorems from <Ref> in combination of the congruence
rules to obtain our goals.

As a corollary,
$ $

* If $\lttypwf i T l$ and $T \redd T'$, then $\lttypwf i {T'} l$.

* If $\lttyping i t T l$ and $t \redd t'$, then $\lttyping i {t'} T l$.

We analyze $i$.
If $i = v$, then there is no applicable reduction rule.
If $i = c$, then we use lifting to lift $i$ to $p$, then use the soundness,
presupposition and unlifting lemmas to obtain the goals.
Otherwise, we use the soundness lemma and the presupposition lemma.

The substitution lemmas require the well-formedness of types and the well-typedness of
terms to make use of algebraic laws of substitutions.
$ $
Given $\compt i$,

* if $\lttypwf[\Psi][\Gamma][L'] i T l$, $T \redd T'$ and $\typing[L]{\phi}{L'}$, then $T[\phi] \redd T'[\phi]$;

* if $\lttyping[\Psi][\Gamma][L'] i t T l$, $t \redd t'$ and
$\typing[L]{\phi}{L'}$, then $t[\phi] \redd t'[\phi]$.

$ $
Given $\compt i$,

* if $\lttypwf[\Psi][\Delta] i T l$, $T \redd T'$ and $\ltsubst i \delta \Delta$, then $T[\delta] \redd T'[\delta]$;

* if $\lttyping[\Psi][\Delta] i t T l$, $t \redd t'$ and
$\ltsubst i \delta \Delta$, then $t[\delta] \redd t'[\delta]$.

$ $
Given $\compt i$,

* if $\lttypwf[\Phi] i T l$, $T \redd T'$ and $\ptyping \sigma \Phi$, then $T[\sigma] \redd T'[\sigma]$;

* if $\lttyping[\Phi] i t T l$, $t \redd t'$ and
$\ptyping \sigma \Phi$, then $t[\sigma] \redd t'[\sigma]$.

All lemmas above also work for the reflexive transitive closure versions of

$ $

* If $T \redd T'$ and $T \redd T'$, then $T' = T''$.

* If $t \redd t'$ and $t \redd t''$, then $t' = t''$.

If a multi-step reduction reaches a normal form, then we know this normal form is also
uniquely determined:
$ $

* If $T \reds W$ and $T \reds W'$, then $W = W'$.

* If $t \reds w$ and $t \reds w'$, then $w = w'$.

Induction. Use the fact that weak head normal forms do not reduce and determinacy of
single-step reduction.

Due to preservation, we often are interested in keeping track of well-formedness and
well-typedness of types and terms.
Therefore it is convenient to give the following convenient auxiliary judgments:

i T l
T T'
i TT' l

i T l
T T'
i TT' l

i t T l
t t'
i tt' T l

i t T l
t t'
i tt' T l

§.§ Convertibility Checking

The convertibility checking is standard: we first reduce types or terms to their
weak head normal forms using reduction, and then recursively compare the
Either we detect a mismatch which causes a failure, or everything checks out and the
convertibility is verified.

Following this line, we give the following judgments for convertibility checking.
Here we always quantify $\compt i$.
The layering index $i$ restricts only types (i.e. those in MLTT or in ), but
not terms.
In other words, it is possible for convertibility checking to relate at layer $p$ two
terms only well-typed at layer $m$, as long as these two terms have type well-formed
at layer $p$ (i.e. MLTT).
This is a critical property to establish a relation between the logical relations at
both layers.

* $\tconvtyp i T{T'} l$ denotes that $T$ and $T'$ are convertible at universe level $l$.

* $\tconvtypnf i W{W'} l$ denotes that $W$ and $W'$ are convertible normal types.

* $\tconvtypne i V{V'}l$ denotes that $V$ and $V'$ are convertible neutral types.

* $\tconvctx i \Gamma \Delta$ denotes that $\Gamma$ and $\Delta$ are convertible contexts.
This judgment is defined by using $\tconvtyp i T{T'} l$ pairwise.

* $\tconvtrm i t{t'}T l$ denotes that $t$ and $t'$ of type $T$ are convertible.

* $\tconvtrmnf i w{w'}W l$ denotes that $w$ and $w'$ are convertible normal terms of a normal
type $W$.

* $\tconvtrmne i \mu{\mu'}T l$ denotes that $\mu$ and $\mu'$ are convertible
neutral terms.
$T$ is the result of inference.

* $\tconvtrmnee i \mu{\mu'}W l$ denotes that $\mu$ and $\mu'$ are convertible neutral terms of
a normal type $W$.
$W$ is the result of inference.

* $\tconvsub i{\delta}{\delta'}\Delta$ denotes that $\delta$ and $\delta'$ are convertible
local substitutions.
This judgment is defined by using $\tconvtrm i t{t'}T l$ pairwise.

We give the following convertibility checking rules for types first:

i T W l
iT'W' l
i WW' l
i TT' l

i Γ

i Γ
i ll'l

i SS' l
[Ψ][Γ, x : S  @  l] i TT'l'
ill'xSTll'xS'T'l ⊔l'

i Γ
U : [Δ]i' l ∈Ψ
i' ∈{c, p}
i' ≤i
i δδ' Δ

i μμ'll
il μl'μ'l

For the types only available at layer $m$:

m Γ
[Ψ][Γ][L, ℓ] mTT'l
mℓl Tℓl'T'ω

m Γ
[Ψ, g : ] mTT'l
mg l Tgl'T'l

m Γ
[Ψ, U : [Δ] pl_1] mTT'l_2
mU [Δ]l_1l_2 TU[Δ']l_3l_4T'l_1

m Γ

m Γ
[Ψ][Δ]p TT'l
m[Δ] Tl[Δ']T'll

We propagate the convertibility for types pairwise to obtain the convertibility for local contexts.

[L] Ψ
i ··

[L] Ψ
g : ∈Ψ

i ΓΔ
i TT' l
iΓ, x : T  @  lΔ, x : T'  @ l'

The convertibility of terms proceeds similarly.
The following are checking rules that are available at both layers:

T W
i t w T l
t'w'T l
i ww'W l
i tt'T l

i Γ

i Γ
i ll'll

i ss'll
[Ψ][Γ, x : l s  @  l] i tt'l'l'
ill'xstll'xs't'l ⊔l'(l ⊔l')

i Γ

i tt'

i μμ'
i μμ'

i S l
i w ll'xSTl ⊔l'
i w'll'xSTl ⊔l'
[Ψ][Γ, x : S  @ l] i wll'xSTxw'll'xSTxTl'
iww'll'xSTl ⊔l'

i μμ'W l
i μμ'V l

i ww'Wl'
i ww'W l

The following rules check terms that are available only at layer $m$:

m w ℓl Tω
m w'ℓl Tω
[Ψ][Γ][L, ℓ] mtℓt'ℓTl
mww'ℓl Tω

m wg l Tl
m w'g l Tl
[Ψ, g : ] mwgw'gTl
mww'g l Tl

m w U [Δ]ll' Tl ⊔l'
m w'U [Δ]ll' Tl ⊔l'
[Ψ, U : [Δ] pl] mwU^𝕀_Δw'U^𝕀_ΔTl'
mww'U [Δ]ll' Tl ⊔l'

m Γ
[Ψ][Δ] c T l
T = T'
mTT'[Δ] ll

m μμ'[Δ] ll
m μμ'[Δ] ll

m Γ
[Ψ][Δ] c t T l
t = t'
mtt'[Δ] T ll

m μμ'[Δ] T ll
m μμ'[Δ] T ll

Notice here convertibility of $\tbox$'ed types and terms are checked simply with
syntactic equality.
The convertibility of neutral terms proceeds as follows.
Similarly, we first give the checking rules that are available at both layers:

i μμ'Tl
T W
i μμ'W l

i μμ'Tl'
i μμ'T l

i Γ
x : T  @  l ∈Γ
i xxT l

i Γ
u : [Δ]i'T l ∈Ψ
i' ∈{v, c}
i' ≤i
i δδ' Δ

[Ψ][Γ, x :  @  ] i MM' l

i s_1s_3 M[/x]l

[Ψ][Γ, x :  @  , y : M  @  l] is_2s_4M[x/x]l

i μμ'
ilx.Ms_1x,y. s_2μl'x.M's_3x,y. s_4μ'M[μ/x]l

i SS'l_1

[Ψ][Γ, x : S  @ l_1] iTT'l_2

i μμ'l_1l_2 xS”T”l_1 ⊔l_2
i ss' Sl_1
iμl_1l_2 x S T sμ'l_3l_4 x S'T's'T[s/x]l_2

When checking applications, we simply ignore the type inferred by checking $\mu$ and
This is fine because we already know $\mu$ and $\mu'$ are well-typed so the type
annotations must be equivalent.

Then we give the rules only available at layer $m$:

mμμ'ℓl Tω
|ℓ| = |l| = |l'| > c

∀c ≤n < |l| ·[L]l(n)l'(n)
mμlμ' $ l'T[l/ℓ]l[l/ℓ]

mμμ'g l Tl
p ΔΔ'

mμμ'U[Δ] ll'T”l ⊔l'
[Ψ][Δ] pTT'l

m Γ
p ΔΔ'

[Ψ][Γ,x_T : [Δ]l_2  @ l_2]mMM'l_1

[Ψ, U : [Δ]cl_2]mt_1t_2M[U/x_T]l_1
ml_1l_2 Δx_T.MU.t_1μl_3l_4Δ'x_T.M'U.t_2μ'M[t/x_T]l_1

m Γ
p ΔΔ'

p TT'l_2

[Ψ][Γ,x_T : [Δ]Tl_2  @ l_1]mMM'l_1

[Ψ, u : [Δ]c Tl_2]mt_1t_2M[u/x_t]l_1
ml_1l_2 ΔTx_t.MU.t_1μl_3l_4Δ'T'x_T.M'U.t_2μ'M[t/x_t]l_1

The remaining piece of the convertibility checking for neutral recursive principles.
The recursive principles get stuck when the scrutinees are neutral or $\tbox$'ed
global variables.
To check the convertibility of neutral recursive principles, we recursively check the
convertibility between motives, corresponding branches and the indexing universe
levels, local contexts and potentially types.
To derive the following two conclusions:

\begin{gather*}
\tconvtrmne m{\ELIMTYP{l_1}{l_2}Mbl\Delta
\mu}{\ELIMTYP{l_3}{l_4}{M_1}{b_1}{l'}{\Delta'}{\mu'}}{M[\mu/x_T]}{l_1} \\
\tconvtrmne m{\ELIMTRM{l_1}{l_2}Mbl\Delta T \mu}{\ELIMTYP{l_3}{l_4}{M_1}{b_1}{l'}{\Delta'}{T'}{\mu'}}{M'[\mu/x_t]}{l_1}
\end{gather*}

We proceed by checking the convertibility of motives:

[L]l_2l_4[Ψ, g : ][Γ, x_T : [g]ℓ][L,ℓ] m MM_1l_1

[Ψ, g : , U_T : [g]pℓ][Γ, x_t : [g]U_T^𝕀ℓ][L,ℓ] mM'M_1'l_2

We do the same for all the branches as well.
Following the previous conventions, we group all these checking into $C_A$ for
convertibility checking for all premises.
Then what we have left is to make sure the scrutinees are convertible.

ml_1l_2MblΔT μl_3l_4M_1b_1l'Δ'T'μ'M'[μ/x_t]l_1

If the scrutinees are $\tbox$'ed global variables, then the check is always the same,
except that the global variables are compared syntactically:

U :
[Δ]c l ∈Ψ
c δΔ

u : [Δ]i'T l ∈Ψ
i' ∈{v, c}
c δΔ

Now we have finished all the convertibility rules for neutral terms.

We simply let the convertibility for terms to propagate pairwise to derive the
convertibility for local substitutions:

$\Gamma$ ends with $\cdot$
|Γ| = m
i ·^m·^m·

g : ∈Ψ
$\Gamma$ ends with $g$
|Γ| = m
i ·_g^m·_g^m·

g : ∈Ψ

$\Gamma$ ends with $g$
|Γ| = m
i _g^m_g^mg

i δδ'Δ

[Ψ][Δ]i T l
i tt'T[δ] l
i δ, t/xδ', t'/xΔ, x : T  @  l

The convertibility algorithm is obtained by reading all the components for
convertibility rules as inputs and the neutral judgments consider types as outputs.
If there is no corresponding rule, then two terms are not convertible; otherwise, two
terms are convertible.
We verify some basic properties as follows:
Assuming $\compt i$,

* if $\tconvtyp i T{T'} l$, then $\lttypeq i T{T'} l$;

* if $\tconvtypnf i W{W'} l$, then $\lttypeq i W{W'} l$;

* if $\tconvtypne i V{V'}l$, then $\lttypeq i{V}{V'}l$;

* if $\tconvctx i \Gamma \Delta$, then $\lpequiv i \Gamma \Delta$;

* if $\tconvtrm i t{t'}T l$, then $\lttyequiv i t{t'} T l$;

* if $\tconvtrmnf i w{w'}W l$, then $\lttyequiv i w{w'} W l$;

* if $\tconvtrmne i \mu{\mu'}T l$, then $\lttyequiv i\mu{\mu'} T l$;

* if $\tconvtrmnee i \mu{\mu'}W l$, then $\lttyequiv i \mu{\mu'} W l$;

* if $\tconvsub i{\delta}{\delta'}\Delta$, then $\ltsubeq i

Mutual induction.
Use $\eta$ rules for all kinds of function types.
Use congruence rules, presupposition and conversion rules when checking neutral

$ $

* If $\tconvtypnf i W{W'} l$, then $\tconvtyp i W{W'} l$.

* If $\tconvtrmnf i w{w'}W l$, then $\tconvtrm i w{w'} W l$.

Other lemmas like PER require the fundamental theorems so we postpone their proofs
until we have the semantic models.

§ LOGICAL RELATIONS FOR

Previously, we have given the judgments of , verified its syntactic
properties and given its reduction and convertibility algorithms.
Starting this section, we establish the logical relation and prove the (weak)
normalization and convertibility properties of .
Following <cit.>, we proceeds as follows:

* First we give a set of generic equivalence conditions for a parameterized
discussion of the logical relation.

* Then we give the definition of the Kripke logical relations of types and
The logical relations are parameterized by layers.
In this step, we are only concerned about types that are available at all layers,
i.e. those in MLTT and unrelated to meta-programming.

* Then we give the definition  of the Kripke logical relations of local contexts
and local substitutions.

* Then we branch off two orthogonal developments.

* We give the definition of the Kripke logical relations of global contexts and
global substitutions.

* We give the definition of the Kripke logical relations of types and terms,
But in this case, we must also give the definition for types that are related to
meta-programming, i.e. contextual types.

In fact, the definitions given by the two sub-steps above must consider each
Otherwise, we will not able to extend related global substitutions during the proof
of the fundamental theorems.

* Next we give the semantic judgments.
The semantic judgments require types, terms, etc. to be stable under all universe,
global and local substitutions.

* Finally, we establish the fundamental theorems for the semantic judgments.
Instantiating the generic equivalence gives us the proof of convertibility.

Due to layering, following <Ref>, the generic equivalence, logical
relation and validity judgments are all layered.
In fact, since computation exists at both layers $p$ and $m$, the situation is very
<cit.> instantiate their generic equivalence twice to obtain
the decidability of convertibility checking, and we will also be doing the same.
Due to the complication of layering, our fundamental theorems must talk about all
The difficulties of the logical relations lie in that how we can support code running
and recursions on code at the same time and justify them in the semantics.

§.§ Generic Equivalence

Similar to <Ref>, we first quantify four generic equivalence relations,
which will be instantiated to syntactic equivalence and convertibility later, and
their laws.
This step provides modularity to logical relation argument: we simply instantiate this
generic equivalence to obtain different versions of the fundamental theorems.
Due to dependent types, we define generic equivalence over $i \in \{p, m\}$:

* $\lttypgneeq i V{V'} l$ describes a generic type equivalence between two neutral
types at universe level $l$ at layer $i$.

* $\lttypgeq i {T}{T'} l$ describes a generic type equivalence between two types at
universe level $l$ at layer $i$.

* $\lttrmgneeq i \mu{\mu'} T l$ describes a generic type equivalence between two neutral
terms of type $T$ at universe level $l$ at layer $i$.

* $\lttrmgeq i t{t'} T l$ describes a generic type equivalence between two
terms of type $T$ at universe level $l$ at layer $i$.

From the four generic equivalence, we induce two equivalence of local contexts and
local substitutions by using the generic equivalence pairwise:

[L] Ψ
i ··

[L] Ψ
g : ∈Ψ

i ΓΔ
i TT' l
iΓ, x : T  @  lΔ, x : T'  @ l'

$\Gamma$ ends with $\cdot$
|Γ| = m
i ·^m·^m·

g : ∈Ψ
$\Gamma$ ends with $g$
|Γ| = m
i ·_g^m·_g^m·

g : ∈Ψ

$\Gamma$ ends with $g$
|Γ| = m
i _g^m_g^mg

i δδ'Δ

[Ψ][Δ]i T l

i tt'T[δ] l
i δ, t/xδ', t'/xΔ, x : T  @  l

The generic equivalence and the logical relations are invariant under all
Therefore, we should make these notions clear here.
Since there are three different contexts, we have three corresponding kinds of
In particular, $\theta :: L \To L'$ is the universe weakening.
Following previous conventions, $\gamma :: L \sep \Psi \To_g \theta$ is a global
weakening, and $\tau :: L \sep \Psi;\Gamma \To_i \Delta$ is a local weakening.
The subscript $i$ denotes which layer the contexts $\Gamma$ and $\Delta$ live in.
We can simultaneously weaken all three contexts at the same time.
We simply apply $\theta$, $\gamma$ and $\tau$ in this order.
We let $\psi$ represent this triple:

\[
\psi := (\theta, \gamma, \tau) :: L \sep \Psi; \Gamma \To_i L' \sep \Phi;\Delta
\]

\begin{align*}
\theta &:: L \To L' \\
\gamma &:: L' \sep \Psi[\theta] \To_g \Phi \\
\tau &:: L' \sep \theta; \Gamma[\theta][\gamma] \To_i \Delta
\end{align*}

Similarly we let

\[
\alpha := (\theta, \gamma) :: L \sep \Psi \To L' \sep \Phi
\]

We can apply weakenings like substitutions to universe levels, types, terms, contexts
and substitutions as expected.
The action is to shift the variables according to the specified weakenings.
This is a standard action, despite having three separate notions, so we take it for
granted here.
When it is clear from the context, we do not write down the weakening action at all to
avoid clutter.

Then we give the laws of the generic equivalence.
Since the generic equivalence at layer $m$ subsumes that at layer $p$, we first give
the laws that hold for both layers, and then incrementally add those that only hold at
layer $m$.

[Subsumption]$ $

* If $\lttypgneeq i V{V'} l$, then $\lttypgeq i V {V'} l$.

* If $\lttypgeq i T{T'} l$, then $\lttypeq i T{T'} l$.

* If $\lttrmgneeq i \mu{\mu'} T l$, then $\lttrmgeq i \mu{\mu'} T l$.

* If $\lttrmgeq i t{t'} T l$, then $\lttyequiv i t{t'} T l$.

As a lemma, subsumption propagates to contexts and local substitutions:
$ $

* If $\ltctxgeq i \Gamma \Delta$, then $\lpequiv i \Gamma \Delta$.

* If $\ltsubgeq i \delta {\delta'} \Delta$, then $\ltsubeq i \delta {\delta'} \Delta$.

Due to subsumption, we know that components in generic equivalence are well-formed or
$ $

* If $\lttypgeq i T{T'} l$, then $\lttypwf i T l$ and $\lttypwf i{T'} l$.

* If $\lttrmgeq i t{t'} T l$, then $\lttyping i t T l$ and $\lttyping i{t'}T

By subsumption and presupposition.

All four relations are PERs.

[Type Conversion] $ $

* If $\lttrmgneeq i \mu {\mu'} T l$ and $\lttypeq i T{T'} l$, then $\lttrmgneeq i \mu {\mu'}{T'} l$.

* If $\lttrmgeq i t {t'} T l$ and $\lttypeq i T{T'} l$, then $\lttrmgeq i t
{t'}{T'} l$.

[Context Equivalence] $ $

* If $\lttypgneeq i V {V'} l$, $\gequiv\Phi\Psi$ and
$\lpequiv[\Phi]{i}\Delta\Gamma$, then $\lttypgneeq[\Phi][\Delta] i V {V'} l$.

* If $\lttypgeq i T{T'} l$, $\gequiv\Phi\Psi$ and
$\lpequiv[\Phi]{i}\Delta\Gamma$, then $\lttypgeq[\Phi][\Delta] i T{T'} l$.

* If $\lttrmgneeq i \mu {\mu'} T l$, $\gequiv\Phi\Psi$ and
$\lpequiv[\Phi]{i}\Delta\Gamma$, then $\lttrmgneeq[\Phi][\Delta] i \mu {\mu'}{T} l$.

* If $\lttrmgeq i t {t'} T l$, $\gequiv\Phi\Psi$ and
$\lpequiv[\Phi]{i}\Delta\Gamma$, then $\lttrmgeq[\Phi][\Delta] i t {t'}{T} l$.

[Weakening] $ $

* If $\lttypgneeq i V {V'} l$ and
$\psi :: L \sep \Psi; \Gamma \To_i L' \sep \Phi;\Delta$, then
$\lttypgneeq[\Phi][\Delta][L'] i{V[\psi]}{V'[\psi]}{l[\psi]}$.

* If $\lttypgeq i T{T'} l$ and
$\psi :: L \sep \Psi; \Gamma \To_i L' \sep \Phi;\Delta$, then
$\lttypgeq[\Phi][\Delta][L'] i{T[\psi]}{T'[\psi]}{l[\psi]}$.

* If $\lttrmgneeq i \mu {\mu'} T l$ and
$\psi :: L \sep \Psi; \Gamma \To_i L' \sep \Phi;\Delta$, then
$\lttrmgneeq[\Phi][\Delta][L'] i{\mu[\psi]}{\mu'[\psi]}{T[\psi]}{l[\psi]}$.

* If $\lttrmgeq i t {t'} T l$ and
$\psi :: L \sep \Psi; \Gamma \To_i L' \sep \Phi;\Delta$, then
$\lttrmgeq[\Phi][\Delta][L'] i{t[\psi]}{t'[\psi]}{T[\psi]}{l[\psi]}$.

[Weak Head Closure] $ $

* If $\ttypreds i T W l$, $\ttypreds i{T'}{W'} l$ and $\lttypgeq i W{W'} l$, then $\lttypgeq i T{T'} l$.

* If $\ttrmreds i t w T l$, $\ttrmreds i{t'}{w'}T l$ and $\lttrmgeq i w{w'} T l$, then $\lttrmgeq i t{t'} T l$.

[Type Constructors]
If $\lpjudge i \Gamma$,

* if $\tyequiv[L] l{l'}\Level$, then $\lttypgeq i{\Ty l}{\Ty l'}{\su l}$ and
$\lttrmgeq i{\Ty l}{\Ty l'}{\Ty{\su l}}{\su{(\su l)}}$;

* then $\lttypgeq i{\Nat}{\Nat}\ze$ and $\lttrmgeq i{\Nat}{\Nat}{\Ty \ze}{\su \ze}$;

* if $\lttypgeq i S{S'} l$ and $\lttypgeq[\Psi][\Gamma, x : S ~@~ l] i
T{T'}{l'}$, then $\lttypgeq i{\PI{l}{l'}x S T}{\PI{l}{l'}x{S'}{T'}}{l \sqcup

* if $\lttrmgeq i s{s'}{\Ty l}{\su l}$ and $\lttrmgeq[\Psi][\Gamma, x : \Elt l s ~@~ l] i
t{t'}{\Ty{l'}}{\su{l'}}$, then $\lttrmgeq i{\PI{l}{l'}x s t}{\PI{l}{l'}x{s'}{t'}}{\Ty{l \sqcup
l'}}{\su{(l \sqcup l')}}$.

[Neutral Types]  $ $

* If $\lpjudge i \Gamma$, $U : \DTyp[\Delta]{i'} l \in \Psi$, $i' \in \{c, p\}$,
$i' \le i$ and
$\ltsubgeq i \delta{\delta'} \Delta$, then
$\lttypgneeq i{U^\delta}{U^{\delta'}}{l}$.

* If $\tyequiv[L]{l}{l'}\Level$ and $\lttrmgneeq i \mu{\mu'}{\Ty l}{\su l}$,
then $\lttypgneeq i{\Elt l \mu}{\Elt{l'}{\mu'}}{l}$.

[Congruence] $ $

* If $\lpjudge i \Gamma$, then $\lttrmgeq i \ze \ze \Nat \ze$.

* If $\lttrmgeq i t{t'}\Nat \ze$, then $\lttrmgeq i {\su t}{\su{t'}}\Nat \ze$.

* If $\lttypwf i S l$, $\lttyping i t {\PI{l}{l'}x{S}{T}}{l \sqcup l'}$,
$\lttyping i {t'}{\PI{l}{l'}x{S}{T}}{l \sqcup l'}$ and $\lttrmgeq[\Psi][\Gamma, x
: S ~@~{l}] i {\APP{t}{l}{l'}x{S}{T}{x}}{\APP{t'}{l}{l'}x{S}{T}{x}}{T}{l'}$,
then $\lttrmgeq i t{t'}{\PI{l}{l'}x{S}{T}}{l \sqcup l'}$.

[Congruence for Neutrals] $ $

* If $\lpjudge i \Gamma$ and $x : T ~@~ l \in \Gamma$, then $\lttrmgneeq i x x
T l$.

* If $\lpjudge i \Gamma$, $u : \DTrm[\Delta]{i'}T l \in \Psi$, $i' \in \{v,
c\}$, $i' \le i$ and $\ltsubgeq i \delta{\delta'} \Delta$, then $\lttrmgneeq i{u^\delta}{u^{\delta'}}
{T[\delta]} l$.

* If $\tyequiv[L]l{l'}\Level$, $\lttypgeq[\Psi][\Gamma, x : \Nat ~@~ \ze] i M{M'} l$,
$\lttrmgeq i {s_1}{s_3} {M[\ze/x]}l$,
$\lttrmgeq[\Psi][\Gamma, x : \Nat ~@~ \ze, y : M ~@~ l] i{s_2}{s_4}{M[\su
x/x]}l$ and
$\lttrmgneeq i \mu{\mu'} \Nat \ze$, then
$\lttrmgneeq i{\ELIMN l{x.M}{s_1}{x,y. s_2}\mu}{\ELIMN{l'}{x.M'}{s_3}{x,y. s_4}{\mu'}}{M[\mu/x]}{l}$.

* If $\tyequiv[L]{l_1}{l_3}\Level$, $\tyequiv[L]{l_2}{l_4}\Level$, $\lttypgeq i S{S'}{l_1}$,
$\lttypgeq[\Psi][\Gamma, x : S ~@~{l_1}] i{T}{T'}{l_2}$, $\lttrmgneeq i \mu{\mu'}{\PI {l_1}{l_2} x{S''}{T''}}{l_1 \sqcup l_2}$ and $\lttrmgeq i
s{s'} S{l_1}$, then $\lttrmgneeq i{\APP \mu {l_1}{l_2} x S T s}{\APP{\mu'}{l_3}{l_4} x

We derive that

If $\lpequiv i \Gamma \Delta$, then
$\ltsubgeq i{\id_{\Gamma}}{\id_{\Gamma}}{\Delta}$.

$ $

* If $\lpequiv i \Gamma \Delta$, $u : \DTrm[\Delta]{i'}T l \in \Psi$, $i' \in \{v, c\}$ and
$i' \le i$, then $\lttrmgneeq i {u^{\id_{\Gamma}}}{u^{\id_{\Gamma}}} T l$.

* If $\lpequiv i \Gamma \Delta$, $U : \DTyp[\Delta]{i'} l \in \Psi$,
$i' \in \{c, p\}$ and $i' \le i$, then $\lttypgneeq i{U^{\id_{\Gamma}}}{U^{\id_{\Gamma}}}{l}$.

At this point, we give the laws that should hold for both layers.
Next, we consider laws that only hold at layer $i = m$.
We first give the laws for type constructors.
[Type Constructors] $ $

* If $\lpjudge m \Gamma$, $\lttypgeq[\Psi][\Gamma][L, \vect\ell] m{T}{T'}{l}$
and $\tyequiv[L,\vect\ell]{l}{l'}{\Level}$, then $\lttypgeq m{\UPI \ell l T}{\UPI \ell{l'}{T'}}\omega$.

* If $\lpjudge m \Gamma$, $\lttypgeq[\Psi, g : \Ctx] m{T}{T'}{l}$ and
$\tyequiv[L]{l}{l'}{\Level}$, then $\lttypgeq m{\CPI g l T}{\CPI g{l'}{T'}}{l}$.

* If $\lpjudge m \Gamma$, $\lttypgeq[\Psi, U : \DTyp[\Delta] p{l_1}]
m{T}{T'}{l_2}$, $\ltctxgeq p{\Delta}{\Delta'}$, $\tyequiv[L]{l_1}{l_3}{\Level}$
and $\tyequiv[L]{l_2}{l_4}{\Level}$, then
$\lttypgeq m{\TPI U [\Delta]{l_1}{l_2} T}{\TPI U[\Delta']{l_3}{l_4}{T'}}{\su l_1
\sqcup l_2}$.

* If $\lpjudge m \Gamma$ and $\ltctxgeq p{\Delta}{\Delta'}$, then $\lttypgeq
m{\CTyp[\Delta]l}{\CTyp[\Delta']l}{\su l}$.

* If $\lpjudge m \Gamma$, $\ltctxgeq p{\Delta}{\Delta'}$ and
$\lttypgeq[\Psi][\Delta]p T{T'}l$, then $\lttypgeq m{\CTrm[\Delta] Tl}{\CTrm[\Delta']{T'}l}{l}$.

[Congruence] $ $

* If $\lttyping m t {\UPI \ell l T}{\omega}$, $\lttyping m {t'}{\UPI \ell l
T}{\omega}$ and $\lttrmgeq[\Psi][\Gamma][L, \vect\ell] m{\UAPP
t{\ell}}{\UAPP{t'}{\ell}}{T}{l}$, then
$\tconvtrmnf m{t}{t'}{\UPI \ell l T}{\omega}$.

* If $\lttyping m t{\CPI g l T}{l}$, $\lttyping m {t'}{\CPI g l T}{l}$ and $\lttrmgeq[\Psi, g : \Ctx] m{\CAPP t{g}}{\CAPP{t'}{g}}{T}{l}$, then $\lttrmgeq
m{t}{t'}{\CPI g l T}{l}$.

* If $\lttyping m t {\TPI U [\Delta]{l}{l'} T}{\su l \sqcup l'}$, $\lttyping m
{t'}{\TPI U [\Delta]{l}{l'} T}{\su l \sqcup l'}$, and $\lttrmgeq[\Psi, U :
\DTyp[\Delta] p{l}] m{\TAPP t{U^{\id_\Delta}}}{\TAPP{t'}{U^{\id_\Delta}}}{T}{l'}$,
then $\lttrmgeq m{w}{w'}{\TPI U [\Delta]{l}{l'} T}{\su l \sqcup l'}$.

* If $\lpjudge m \Gamma$ and $\lttypwf[\Psi][\Delta] c T l$, then $\lttrmgeq
m{\boxit T}{\boxit{T}}{\CTyp[\Delta] l}{\su l}$.

* If $\lpjudge m \Gamma$ and $\lttyping[\Psi][\Delta] c t T l$, then
$\lttrmgeq m{\boxit t}{\boxit{t}}{\CTrm[\Delta] T l}{l}$.

[Congruence for Neutrals] $ $

* If $\lttrmgneeq m{\mu}{\mu'}{\UPI \ell l T}{\omega}$, $|\vect\ell| = |\vect l| = |\vect
l'| > c$ and
$\forall ~ c \le n < |\vect l| \cdot \tyequiv[L]{\vect l(n)}{\vect l'(n)}\Level$,
then $\lttrmgneeq m{\UAPP \mu l}{\mu'~\$~\vect l'}{T[\vect l/\vect \ell]}{l[\vect
l/\vect \ell]}$.

* If $\lttrmgneeq m{\mu}{\mu'}{\CPI g l T}{l}$ and $\ltctxgeq p
\Delta{\Delta'}$, then $\lttrmgneeq m{\CAPP \mu
\Delta}{\CAPP{\mu'}{\Delta'}}{T[\Delta/g]}{l}$.

* If $\lttrmgneeq m{\mu}{\mu'}{\TPI U[\Delta] l{l'}{T''}}{\su l \sqcup l'}$ and
$\lttypgeq[\Psi][\Delta] p{T}{T'}l$, then
$\lttrmgneeq m{\TAPP \mu{T}}{\TAPP{\mu'}{T'}}{T''[T/U]}{l'}$.

* If $\lpjudge m \Gamma$, $\tyequiv[L]{l_1}{l_3}\Level$,
$\tyequiv[L]{l_2}{l_4}\Level$, $\ltctxgeq p \Delta{\Delta'}$, $\lttrmgneeq m{\mu}{\mu'}{\CTyp[\Delta]{l_2}}{\su {l_2}}$,
$\lttypgeq[\Psi][\Gamma,x_T : \CTyp[\Delta]{l_2} ~@~{\su{l_2}}]m{M}{M'}{l_1}$
and $ \lttrmgeq[\Psi, U : \DTyp[\Delta]c{l_2}]m{t_1}{t_2}{M[\boxit{U^\id}/x_T]}{l_1}$, then $\lttrmgneeq m{\LETBTYP{l_1}{l_2}
\Delta{x_T.M}{U.t_1}\mu}{\LETBTYP{l_3}{l_4}{\Delta'}{x_T.M'}{U.t_2}{\mu'}}{M[t/x_T]}{l_1}$.

* If $\lpjudge m \Gamma$, $\tyequiv[L]{l_1}{l_3}\Level$,
$\tyequiv[L]{l_2}{l_4}\Level$, $\ltctxgeq p \Delta{\Delta'}$,
$\lttypgeq p T{T'}{l_2}$,
$\lttrmgneeq m{\mu}{\mu'}{\CTrm[\Delta]T{l_2}}{l_2}$,
$\lttypgeq[\Psi][\Gamma,x_T : \CTrm[\Delta]T{l_2} ~@~{l_1}]m{M}{M'}{l_1}$
and $ \lttrmgeq[\Psi, u : \DTrm[\Delta]c T{l_2}]m{t_1}{t_2}{M[\boxit{u^\id}/x_t]}{l_1}$, then $\lttrmgneeq m{\LETBTRM{l_1}{l_2}
\Delta{T}{x_t.M}{U.t_1}\mu}{\LETBTRM{l_3}{l_4}{\Delta'}{T'}{x_T.M'}{U.t_2}{\mu'}}{M[t/x_t]}{l_1}$.

Then we consider the law for neutral forms for recursive principles for code.
The law follows a similar line to the equivalence judgments and the convertibility
checking: the evaluation is blocked when the scrutinee is neutral or is a $\tbox$'ed
global variable.
[Neutral Recursion on Code] $ $

* If all motives and branches are related by corresponding generic equivalence,
moreover, $\tyequiv[L]{l}{l'}\Level$, $\ltctxgeq p{\Delta}{\Delta'}$ and
$\lttrmgneeq m{\mu}{\mu'}{\CTyp[\Delta]{l}}{l}$, then $\lttrmgneeq m{\ELIMTYP{l_1}{l_2}Mbl\Delta
\mu}{\ELIMTYP{l_3}{l_4}{M_1}{b_1}{l'}{\Delta'}{\mu'}}{M[\mu/x_T]}{l_1}$.

* If all motives and branches are related by corresponding generic equivalence,
moreover, $\tyequiv[L]{l}{l'}\Level$, $\ltctxgeq p{\Delta}{\Delta'}$,
$U : \DTyp[\Delta]{c} l \in \Psi$ and $\ltsubst c \delta \Delta$, then $\lttrmgneeq m{\ELIMTYP{l_1}{l_2}Mbl\Delta{(\boxit{U^\delta})}}{\ELIMTYP{l_3}{l_4}{M_1}{b_1}{l'}{\Delta'}{(\boxit{U^\delta})}}{M[\boxit{U^\delta}/x_T]}{l_1}$.

* If all motives and branches are related by corresponding generic equivalence,
moreover, $\tyequiv[L]{l}{l'}\Level$, $\ltctxgeq p{\Delta}{\Delta'}$,
$\tconvtyp p T{T'}{l}$ and
$\tconvtrmnee m{\mu}{\mu'}{\CTrm[\Delta]T{l}}{l}$, then $\lttrmgneeq m{\ELIMTRM{l_1}{l_2}Mbl\Delta T \mu}{\ELIMTYP{l_3}{l_4}{M_1}{b_1}{l'}{\Delta'}{T'}{\mu'}}{M'[\mu/x_t]}{l_1}$.

* If all motives and branches are related by corresponding generic equivalence,
moreover, $\tyequiv[L]{l}{l'}\Level$, $\ltctxgeq p{\Delta}{\Delta'}$,
$\tconvtyp p T{T'}{l}$, $u : \DTrm[\Delta]{i'}T l \in \Psi$,
$ i' \in \{v, c\}$ and $\ltsubst c \delta \Delta$, then $\lttrmgneeq m{\ELIMTRM{l_1}{l_2}Mbl\Delta T

We conclude all the laws here fore the generic equivalence.

This generic equivalence will be instantiated twice times: the syntactic equivalence
judgments, and the convertibility checking judgments.
is way more complex than <cit.>'s work because
has computations at two layers, $p$ and $m$.
Therefore, we must derive the necessary properties from the fundamental theorems to be
proved shortly at each layer.

§.§ Kripke Logical Relations for MLTT

The Kripke logical relations are parameterized by the generic equivalence.
It is additionally indexed by another layering index $j \in \{p, m\}$, which
quantifies the types described by the relations.
When $j = p$, we consider types from MLTT.
When $j = m$, we consider all possible types.
The reason for this distinction is to handle the lifting property from layer $c$
(which has the terms as $p$) or $p$ to
$m$, where terms from MLTT are brought to .
On the semantic side, we need to make sure that terms from MLTT can interact with
“native” terms in coherent.
We further restrict $j = p$ when $i = p$.

The Kripke logical relations are defined by

* recursion on $i$,

* recursion on $j$, which effectively means the logical relations are
2-layered; also note when $i = p$, $j = p$ is determined;

* a transfinite well-founded recursion on the universe levels, and

* induction-recursion on related types and terms.

In particular, the recursion on $j$ is necessary, as the relations when $j = m$ depend
on the validity judgments of $j = p$.
When we do a recursion on universe levels, we must mind the well-foundedness of
universe levels.
As we have discussed in <Ref>, we are sure that all universe
levels must find a finite number of steps to descend to $\ze$.
The only problem is $\omega$, which is not finite.
Thus we must include one large cardinal to handle this level, hence the transfinite
Luckily, we do not have to think about it most of the time as we cannot really use
$\omega$ to do anything special at all.
Note that our relations do not exactly follow <cit.> tightly,
where two relations are defined for types and terms respectively.
In our case, we provide simpler inductive-recursive definitions, where only one
relation is defined for types and for terms respectively.
This style is more akin to the PER models in untyped domains by
<cit.>, except that our logical
relations are Kripke.
We follow a proof schema that combines that of <cit.> and that
of <cit.>.
We define the following judgments:

* $\D :: \ldtypeq i j T{T'} l$ denotes that two types $T$ and $T'$ are related.
This relation is defined inductively.
We use $\D$ to mark give a name to the derivation as we will do recursion on it.

* $\ldtyequiv i j t{t'} \D$ denotes that two terms $t$ and $T'$ related by $\D$.
This relation is defined by a recursion on $\D$.

* $\E :: \ldctxeq i j \Gamma \Delta$ denotes that two contexts are related.
It is a generalization of $\D$.

* $\ldsubeq i j \delta{\delta'} \E$ denotes that two local substitutions
$\delta$ and $\delta'$ are related.
It is a generalization of $\ldtyequiv i j t{t'} \D$ by doing recursion on $\E$.

For convenience, we define the following:

\begin{align*}
\ldtypwf i j T l &:= \ldtypeq i j T T l \\
\ldtyequivt i j t{t'} T l & := \text{for some $T'$, } \D :: \ldtypeq i j T{T'}
l \tand \ldtyequiv i j t{t'}{\D} \\
\ldtyping i j t T l & := \ldtyequivt i j t{t} T l \\
\ldctxwf i j \Gamma &:=  \ldctxeq i j \Gamma \Gamma \\
\ldsubeq i j \delta{\delta'} \Delta &:= \text{for some $\Delta'$, }\E :: \ldctxeq i
j \Delta{\Delta'} \tand \ldsubeq i j \delta{\delta'} \E \\
\ldsubst i j \delta \Delta &:= \ldsubeq i j \delta{\delta} \Delta
\end{align*}

Now we proceed to define the relations.
We begin with the natural numbers.

:: i T
i T'
i j TT'

Then $\ldtyequiv i j t{t'} \D$ is defined by $\ldtyeqnat i t{t'}$, which we
define as follows:

i t w
i ww'
i ww'
i tt'

i tt'

i μμ'

Then we consider universes.

:: i Tl_1l_1
i T'l_2l_2

i jTT'l

Then $\ldtyequiv i j t{t'} \D$ is defined by

* $\ttrmreds i t w{\Ty l}{\su l}$,

* $\ttrmreds i {t'}{w'}{\Ty l}{\su l}$,

* $\lttrmgeq i w{w'}{\Ty l}{\su l}$, which means that $t$ and $t'$ are equivalent
types at level $l$,

* $\ldtypeq i j{\Elt l w}{\Elt l{w'}}{l}$, which means that the corresponding
types of $w$ and $w'$ are related.

The last condition requires the well-founded recursion on the universe levels in order
to refer back to the relation for types.
Notice that the universe level decreases by one so this definition is valid.

Then we define the relation for $\Pi$ types.

:: i Tll' xS_1T_1l ⊔l'
i T'll'
xS_2T_2l ⊔l'

iS_1 l
iS_2 l
[Ψ][Γ, x : S_1  @  l]

[Ψ][Γ, x : S_2  @  l] iT_2l'

ill' xS_1T_1ll' xS_2T_2l ⊔l'

:: (∀  ψ:: L' Φ;Δ_i L Ψ; Γ·[Φ][Δ][L'] i jS_1S_2l)

:: (∀  ψ:: L' Φ;Δ_i L Ψ; Γ[Φ][Δ][L']
i j ss'(ψ) ·[Φ][Δ][L'] i jT_1[s/x]T_2[s'/x]l')
i jTT'l ⊔l'

This case is particularly complex.
Let us digest the premises one by one.
First, we require that both types $T$ and $T'$ to reduce to some $\Pi$ types.
The typing judgments require the components of the $\Pi$ types are well-formed.
Further, the $\Pi$ types themselves are equivalent.
Then $\E$ requires that $S_1$ and $S_2$ are related under any weakening.
This makes the relation Kripke.
$\F$ is similar but require $T_1$ and $T_2$ remain related given any two related terms
$s$ and $s'$.
Furthermore, in reality, we should put down sufficient premises for equivalent
universes to allow syntactically different universes to appear in both $T$ and $T'$,
but due to the size of this rule, we only use $l$ and $l'$ here.
We apply the same principle in other rules in the rest of this technical report.

Then $\ldtyequiv i j t{t'} \D$ is defined by

* $\ttrmreds i t w{\PI l{l'} x{S_1}{T_1}}{l \sqcup l'}$,

* $\ttrmreds i {t'}{w'}{\PI l{l'} x{S_2}{T_2}}{l \sqcup l'}$,

* $\lttrmgeq i w{w'}{\PI l{l'} x{S_1}{T_1}}{l \sqcup l'}$,

* $\lttrmgeq i w{w'}{\PI l{l'} x{S_2}{T_2}}{l \sqcup l'}$, which is duplicated to
make symmetry a simpler property,

* $\forall\ \psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma \tand \Ac ::
\ldtyequiv[\Phi][\Delta][L'] i j {s}{s'}{\E(\psi)} \cdot$, moreover, we add
equivalence assumptions to remove the effect of type annotations,
$\lttypgeq[\Phi][\Delta][L'] i{S_1}{S_1'}l$, $\lttypgeq[\Phi][\Delta][L'] i{S_2}{S_2'}l$, $\lttypgeq[\Phi][\Delta, x : S_1 ~@~ l][L'] i{T_1}{T_1'}{l'}$,
$\lttypgeq[\Phi][\Delta, x : S_2 ~@~ l][L'] i{T_2}{T_2'}{l'}$, then $\ldtyequiv[\Phi][\Delta][L'] i j{\APP w l{l'} x{S_1'}{T_1'} s}{\APP{w'}l{l'}
x{S_2'}{T_2'}{s'}}{\F(\psi, \Ac)}$.

The next case is neutral types.

:: i TVl

i VV' l
i jTT'l

Then $\ldtyequiv i j t{t'} \D$ is defined by

* $\ttrmreds i t \mu{V}{l}$,

* $\ttrmreds i {t'}{\mu'}{V'}{l}$,

* $\lttrmgneeq i \mu{\mu'}{V}{l}$,

* $\lttrmgneeq i \mu{\mu'}{V'}{l}$.

Again, we duplicate $\mu \sim \mu'$ to make symmetry easy.

The last case possible for both layers is equivalence of universe levels.
This case is introduced for bureaucratic purposes and often ignored.

:: :: i jTT'l'
i jTT'l

Then $\ldtyequiv i j t{t'} \D$ is defined by $\ldtyequiv i j t{t'} \E$.

Now we have given all logical relations for types and terms that are available at both layers.
In order to give the logical relations for layer $m$, we need to first give the
logical relations for local contexts and local substitutions, as the semantics of
contextual types depend on them.
The complexity of our logical relations primarily comes from the fact that we must be
able to handle computation at two layers ($p$ and $m$) and different lifting

We proceed by defining related local contexts inductively and then the corresponding
recursive case for local substitutions.

:: [L] Ψ
i j ··

Then $\ldsubeq i j \delta{\delta'} \E$ is defined by $\lpjudge i \Gamma$ and then checking $\Gamma$:

* if $\Gamma$ ends with $\cdot$, then $\delta = \delta' = \cdot^{|\Gamma|}$;

* if $\Gamma$ ends with $g$, then $g : \Ctx \in \Psi$ and $\delta = \delta' = \cdot^{|\Gamma|}_g$;

:: [L] Ψ
g : ∈Ψ
i j gg

Then $\ldsubeq i j \delta{\delta'} \E$ is defined as $\lpjudge i \Gamma$ and

* $\Gamma$ also ends with $g$,

* $\delta = \delta' = \wk^{|\Gamma|}_g$.

:: :: ∀ α:: L' ΦL Ψ·[Φ][L'] i j
:: i j TT' l
i jΔ, x : T  @  lΔ', x : T'  @ l'

Then $\ldsubeq i j \delta{\delta'} \E$ is defined as

* $\delta = \delta_1, t/x$,

* $\delta' = \delta_1', t'/x$,

* $\Cc :: \forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot \ldsubeq[\Phi][\Gamma][L'] i j {\delta_1}{\delta_1'}{\F(\alpha)}$,

* $\forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot \ldtyequiv[\Phi][\Gamma][L'] i j t{t'}{\D(\alpha,
\Cc(\alpha))}$.

where we let $\D :: \ldStypeq \F i j T{T'} l$ to be

\[
\forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot ~ \ldsubeq[\Phi][\Gamma][L'] i j \delta{\delta'}{\F(\alpha)} \cdot \ldtypeq[\Phi][\Gamma][L'] i j {T[\delta]}{T'[\delta']}{l}
\]

The judgment $\ldStypeq \F i j T{T'} l$ requires the stability under local substitutions
of the relation between $T$ and $T'$.
We apply the same principle to related terms and derive the judgment
$\ldStyequiv \F i j t{t'}{\D}$, which is given by

\[
\forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot ~ \Cc :: \ldsubeq[\Phi][\Gamma][L'] i j
\delta{\delta'}{\F(\alpha)} \cdot \ldtyequiv[\Phi][\Gamma][L'] i j {t[\delta]}{t'[\delta']}{\D(\alpha,
\Cc)}
\]

§.§ Properties for Logical Relations When $j = p$

In this section, we pause our progress of defining the logical relations when $j =
Following previous lines of work, when we give the Kripke logical relations to
contextual types, we will have to refer to the validity judgments of types and terms
in the logical relations.
Therefore, in this section, we first work out a list of properties of the logical
relations when $j = p$, and then in the next section, we define semantic judgments for
global contexts and global substitutions, and then validity judgments.
Once we have the validity judgments when $j = p$, we can then finish writing down the
logical relations for contextual types.
Without further ado, let us start proving some lemmas.
The list of lemmas mainly follows <cit.>
though we also take <cit.> into consideration.

$ $

* If $\D :: \ldtypeq i p{T}{T'}{l}$ and
$\psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma$, then
$\E :: \ldtypeq[\Phi][\Delta][L'] i p{T}{T'}{l}$.

* If $\ldtyequiv i p{t}{t'}\D$ and
$\psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma$, then
$\ldtyequiv[\Phi][\Delta][L'] i p{t'}{t}\E$.

Induction on $\D$.
Note that typing judgments are invariant under weakenings.
Also use the weakening law for generic equivalence.

$ $

* If $\D :: \ldtypeq i p{T}{T'}{l}$, then $\lttypgeq i {T}{T'} l$.

* If $\ldtyequiv i p{t}{t'}\D$, then $\lttrmgeq i t{t'} T l$ and $\lttrmgeq i t{t'}{T'} l$.

Induction on $\D$.
Use the subsumption law of the generic equivalence.

If $\D :: \ldtypeq i p{T}{T'}l$, $\lttrmgneeq i \mu{\mu'} T l$ and $\lttrmgneeq i \mu{\mu'}{T'} l$, then $\ldtyequiv i p{\mu}{\mu'}\D$.

Induction on $\D$.
Use the conversion and subsumption laws of generic equivalence and then the
soundness of multi-step reductions and the escape lemma to obtain the equivalence
between $\mu$ and $\mu'$ as normal forms.
In the function case, we use the congruence for neutral law of generic equivalence
to show that the results of applying two neutral function are related.

$ $

* If $\D :: \ldtypeq i p{T}{T'}{l}$, $\ttypreds i{T_1} T l$ and $\ttypreds
i{T_1'}{T'}l$, then $\ldtypeq i p {T_1}{T_1'} l$.

* If $\ldtyequiv i p{t}{t'}\D$, $\ttrmreds i{t_1}{t}{T} l$ and $\ttrmreds
i{t_1'}{t'}{T'}l$, then $\ldtyequiv i p {t_1}{t_1'} \D$.

Induction on $\D$. Use transitivity of reductions.

$ $

* If $\D :: \ldtypeq i p{T}{T'}{l}$, then $\E :: \ldtypeq i p{T'}{T}{l}$.

* If $\ldtyequiv i p{t}{t'}\D$, then $\ldtyequiv i p{t'}{t}\E$.

We do induction on $\D$.
Since our definition is designed with symmetry in mind, symmetry is rather immediate.

If $\D :: \ldtypeq i p{T}{T'}{l}$, $\E :: \ldtypeq i p{T}{T''}{l}$ and
$\ldtyequiv i p{t}{t'}\D$, then $\ldtyequiv i p{t}{t'}\E$.

We do induction on $\D$ and then invert $\E$.
We consider the function case.
In this case, we have premises

\begin{align*}
\D_1 &:: (\forall~ \psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma \cdot
\ldtypeq[\Phi][\Delta][L'] i p{S_1}{S_2}{l_1}) \\
\D_2 &:: (\forall~ \psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma \cdot \forall~ \ldtyequiv[\Phi][\Delta][L']
i p {s}{s'}{\D_1(\psi)} \cdot
\ldtypeq[\Phi][\Delta][L'] i p{T_1[s/x]}{T_2[s'/x]}{l_2}) \\
\E_1 &:: (\forall~ \psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma \cdot
\ldtypeq[\Phi][\Delta][L'] i p{S_1}{S_2'}{l_1}) \\
\E_2 &:: (\forall~ \psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma \cdot \forall~ \ldtyequiv[\Phi][\Delta][L']
i p {s}{s'}{\E_1(\psi)} \cdot
\ldtypeq[\Phi][\Delta][L'] i p{T_1[s/x]}{T_2'[s'/x]}{l_2})
\end{align*}

from $\D$ and $\E$.
Here $\D_1$ and $\D_2$ are the premises of $\D$, and likewise for $\E$.
By determinacy, we know that

\[
T \reds \PI{l_1}{l_2} x{S_1}{T_1}
\]

must be unique.
Moreover, we also know

\begin{gather*}
T' \reds \PI{l_1}{l_2} x{S_2}{T_2} \\
T'' \reds \PI{l_1}{l_2} x{S_2'}{T_2'}
\end{gather*}

The most difficult part is to show that given

* $\psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma$,

* $\Ac :: \ldtyequiv[\Phi][\Delta][L'] i p {s}{s'}{\E_1(\psi)}$

* $\lttypgeq[\Phi][\Delta][L'] i{S_1}{S_3}l$,

* $\lttypgeq[\Phi][\Delta][L'] i{S_2}{S_4}l$,

* $\lttypgeq[\Phi][\Delta, x : S_1 ~@~{l_1}][L'] i{T_1}{T_3}{l_2}$, and

* $\lttypgeq[\Phi][\Delta, x : S_2' ~@~{l_1}][L'] i{T_2'}{T_4}{l_2}$,

\[
\ldtyequiv[\Phi][\Delta][L'] i p{\APP w{l_1}{l_2} x{S_3}{T_3} s}{\APP{w'}{l_1}{l_2}
x{S_4}{T_4}{s'}}{\E_2(\psi, \Ac)}
\]

From $\ldtyequiv i p{t}{t'}\D$, together with

* $\Bc :: \ldtyequiv[\Phi][\Delta][L'] i p {s}{s'}{\D_1(\psi)}$ by IH,

* $\lttypgeq[\Phi][\Delta, x : S_2 ~@~{l_1}][L'] i{T_2}{T_4}{l_2}$, where we
know $\lttypeq i{S_2}{S_2'}{l_1}$ by escape, the subsumption law of generic
equivalence, transitivity and local context equivalence of syntactic and generic

we have

\[
\ldtyequiv[\Phi][\Delta][L'] i p{\APP w{l_1}{l_2} x{S_3}{T_3} s}{\APP{w'}{l_1}{l_2}
x{S_4}{T_4}{s'}}{\D_2(\psi, \Bc)}
\]

By another IH, we have the goal.

If $\D :: \ldtypeq i p{T'}{T}{l}$, $\E :: \ldtypeq i p{T''}{T}{l}$ and
$\ldtyequiv i p{t}{t'}\D$, then $\ldtyequiv i p{t}{t'}\E$.

Immediate by symmetry and right irrelevance.

The left and right irrelevance lemmas are called the irrelevance lemma.
It says that the exact relation between types is not important as long as their normal
forms are related.

$ $

* If $\D_1 :: \ldtypeq i p{T_1}{T_2}{l}$ and $\D_2 :: \ldtypeq i
p{T_2}{T_3}{l}$, then $\D_3 :: \ldtypeq i p{T_1}{T_3}{l}$.

* If $\E :: \ldtypeq i p{T_1}{T_1}{l}$, $\ldtyequiv i p{t_1}{t_2}{\D_1}$ and
$\ldtyequiv i p{t_2}{t_3}{\D_2}$, then $\ldtyequiv i p{t_1}{t_3}{\D_3}$.

* $\F :: \ldtypeq i p{T_1}{T_1}{l}$.

* If $\ldtyequiv i p{t_1}{t_2}{\D_1}$, then $\ldtyequiv i p{t_1}{t_1}{\F}$.

We do induction on $\D_1$ and then invert $\D_2$.
The function case is the most complex one.
We have the following premises:

\begin{align*}
\Ac_1 &:: (\forall~ \psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma \cdot
\ldtypeq[\Phi][\Delta][L'] i p{S_1}{S_2}{l_1}) \\
\Ac_2 &:: (\forall~ \psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma \cdot \forall~ \ldtyequiv[\Phi][\Delta][L']
i p {s}{s'}{\Ac_1(\psi)} \cdot
\ldtypeq[\Phi][\Delta][L'] i p{S_1'[s/x]}{S_2'[s'/x]}{l_2}) \\
\Bc_1 &:: (\forall~ \psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma \cdot
\ldtypeq[\Phi][\Delta][L'] i p{S_2}{S_3}{l_1}) \\
\Bc_2 &:: (\forall~ \psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma \cdot \forall~ \ldtyequiv[\Phi][\Delta][L']
i p {s}{s'}{\E_1(\psi)} \cdot
\ldtypeq[\Phi][\Delta][L'] i p{S_2'[s/x]}{S_3'[s'/x]}{l_2})
\end{align*}

from $\D$ and $\E$.
Here $\Ac_1$ and $\Ac_2$ are the premises of $\D_1$, and $\Bc_1$ and $\Bc_2$ are from $\D_2$.
By determinacy, we know that

\begin{gather*}
T_1 \reds \PI{l_1}{l_2} x{S_1}{S_1'} \\
T_2 \reds \PI{l_1}{l_2} x{S_2}{S_2'} \\
T_3 \reds \PI{l_1}{l_2} x{S_3}{S_3'}
\end{gather*}

Now, we should construct the transitivity for types and terms at the same time to
understand how this proof is going to check out.
First we let

\[
\Cc_1 :: (\forall~ \psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma \cdot
\ldtypeq[\Phi][\Delta][L'] i p{S_1}{S_3}{l_1})
\]

be the result of IH on $\Ac_1$ and $\Bc_1$.
Then our goal is to show that

The most difficult part is to show that given

* $\psi :: L' \sep \Phi;\Delta \To_i L \sep \Psi; \Gamma$,

* $\F :: \ldtyequiv[\Phi][\Delta][L'] i p {s}{s'}{\Cc_1(\psi)}$

* $\lttypgeq[\Phi][\Delta][L'] i{S_1}{S_4}l$,

* $\lttypgeq[\Phi][\Delta][L'] i{S_3}{S_5}l$,

* $\lttypgeq[\Phi][\Delta, x : S_1 ~@~{l_1}][L'] i{S_1'}{S_4'}{l_2}$, and

* $\lttypgeq[\Phi][\Delta, x : S_3 ~@~{l_1}][L'] i{S_3'}{S_5'}{l_2}$,

\[
\Cc_2 :: \ldtypeq[\Phi][\Delta][L'] i p{S_1'[s/x]}{S_3'[s'/x]}{l_2}
\]

\[
\ldtyequiv[\Phi][\Delta][L'] i p{\APP w_1{l_1}{l_2} x{S_4}{S_4'} s}{\APP{w_3}{l_1}{l_2}
\]

where $t_k \reds w_k$ for $k \in \{1, 2, 3\}$.

Our plan is the following:

* We first relate $S_1'[s/x]$ and $S_2'[s/x]$, resp.
$\APP {w_1}{l_1}{l_2} x{S_4}{S_4'} s$ and $\APP {w_2}{l_1}{l_2} x{S_4}{S_4'} s$, which

\[
\ldtyequiv[\Phi][\Delta][L'] i p {s}{s}{\Ac_1(\psi)}
\]

which is derived from reflexivity and irrelevance;

* and then relate $S_2'[s/x]$ and $S_3'[s/x]$, resp.
$\APP {w_2}{l_1}{l_2} x{S_4}{S_4'} s$ and $\APP {w_2}{l_1}{l_2} x{S_5}{S_5'}{s'}$,
which requires

\[
\ldtyequiv[\Phi][\Delta][L'] i p {s}{s'}{\Bc_1(\psi)}
\]

which is immediate from irrelevance.

The final missing piece is reflexivity.
For types, it is just a result from transitivity and symmetry.
For terms, it is reflexivity and transitivity of related types and then

This concludes the function case.

Next, we work on the properties for related local contexts and local substitutions.
We first consider the built property of weakening.
Weakening can be seen as a case of the Yoneda lemma, where we only depend on
composition of weakenings.
$ $

* If $\D :: \ldctxeq i p \Delta{\Delta'}$ and  $\alpha :: L' \sep \Phi \To L \sep
\Psi$, then $\E :: \ldctxeq[\Phi][L'] i p \Delta{\Delta'}$.

* If $\ldsubeq i p{\delta}{\delta'}\D$, $\alpha :: L' \sep \Phi \To L \sep \Psi$
and $\tau :: L' \sep \Phi; \Gamma' \To_i \Gamma$, then
$\ldsubeq[\Phi][\Gamma'][L'] i p{\delta}{\delta'}\E$.

Induction on $\D$.
In the two base cases, we know $\judge[L']\Phi$ by weakening.
In the step case, we simply store the given weakenings in a composition.

Notice that the second statement is a little bit strengthened.
It is possible due to local weakening of related types and terms.

We should first prove the reflexivity between identity local substitutions before
proving the the escape lemma.

If $\lpequiv i{\Delta,\Gamma}{\Delta',\Gamma}$ and $\D :: \ldctxeq i p \Delta{\Delta'}$, then $\ldsubeq[\Psi][\Delta,\Gamma] i p{\wk^{|\Gamma|}_{\Delta}}{\wk^{|\Gamma|}_{\Delta}}\D$.

We do induction on $\D$ and consider the step case

:: :: ∀α:: L' ΦL Ψ·[Φ][L'] i p ΔΔ'

:: i p TT' l
i pΔ, x : T  @  lΔ', x : T'  @ l'

\begin{align*}
\Bc :: & \forall \alpha :: L' \sep \Phi \To L \sep \Psi \cdot \ldsubeq[\Phi][\Delta, x : T ~@~ l,\Gamma][L'] i p{\wk^{1 + |\Gamma|}_{\Delta}}{\wk^{1 + |\Gamma|}_{\Delta}}{\E(\alpha)}
\byIH \\
\alpha :: & L' \sep \Phi \To L \sep \Psi
\tag{by assumption} \\
& \ldtypeq[\Phi][\Delta, x : T ~@~ l,\Gamma][L'] i p {T[\wk^{1 + |\Gamma|}_{\Delta}]}{T'[\wk^{1 + |\Gamma|}_{\Delta}]}{l}
\tag{as $\F(\alpha, \Bc(\alpha))$} \\
\Ac :: & \ldtypeq[\Phi][\Delta, x : T ~@~ l,\Gamma][L'] i p {T}{T'}{l} \\
& \lpjudge[\Phi][L'] i{\Gamma, x : T ~@~ l,\Delta}
\tag{by weakening and presupposition} \\
& \lttrmgneeq[\Phi][\Delta, x : T ~@~ l,\Gamma][L'] i x x T l
\tag{by congruence for neutrals of generic equivalence} \\
& \ldtyequiv[\Phi][\Delta, x : T ~@~ l,\Gamma][L'] i p{x}{x}\Ac
\tag{by reflexivity of neutral} \\
& \ldsubeq[\Psi][\Gamma, x : T ~@~ l,\Delta] i p{\wk^{1 + |\Gamma|}_{\Delta},x/x}{\wk^{1 + |\Gamma|}_{\Delta},x/x}\D
\end{align*}

Thus we conclude the goal.

If $\lpequiv i \Gamma \Delta$ and $\D :: \ldctxeq i p \Gamma \Delta$, then $\ldsubeq i p{\id}{\id}\D$.

This is a specialization of the previous lemma.

Knowing all local identity substitutions are reflexively related, we can then prove
the escape lemma.
$ $

* If $\D :: \ldctxeq i p{\Delta_1}{\Delta_2}$, then $\ltctxgeq i{\Delta_1}{\Delta_2}$.

* If $\ldsubeq i p{\delta}{\delta'}\D$, then $\ltsubgeq i
{\delta}{\delta'}{\Delta_1}$ and $\ltsubgeq i {\delta}{\delta'}{\Delta_2}$.

Induction on $\D$.
We consider the step case.

:: :: ∀α:: L' ΦL Ψ·[Φ][L'] i
:: i p TT' l
i pΔ_1, x : T  @  lΔ_2, x : T'  @ l'

\begin{align*}
& \ltctxgeq i{\Delta_1}{\Delta_2}
\byIH \\
& \ldsubeq[\Psi][\Delta_1] i p{\id}{\id}{\E(\id)}
\tag{by \Cref{lem:dt:refl-lid}} \\
& \ldtypeq[\Psi][\Delta_1] i p {T}{T'}{l}
\tag{as $\F(\id, \E(\id))$} \\
& \lttypgeq[\Psi][\Delta_1] i {T}{T'} l
\tag{by escape}
\end{align*}

Hence we conclude the first statement.

In the second statement, we have $\delta = \delta_1, t/x$ and $\delta' = \delta_1',
t'/x$, then

\begin{align*}
& \ldsubeq i p {\delta_1}{\delta_1'}{\E(\id)}
\tag{by assumption} \\
& \ltsubgeq i {\delta_1}{\delta_1'}{\Delta_1} \tand \ltsubgeq i {\delta_1}{\delta_1'}{\Delta_2}
\byIH \\
& \ldtyequiv i p t{t'}{\F(\id, \E(\id))}
\tag{by assumption} \\
& \lttrmgeq i t{t'}{T[\delta_1]}l
\tag{by escape of related terms}
\end{align*}

Therefore we conclude the second statement as well.

$ $

* If $\D :: \ldctxeq i p{\Delta_1}{\Delta_2}$, then $\E :: \ldctxeq i p{\Delta_2}{\Delta_1}$.

* If $\ldsubeq i p{\delta}{\delta'}\D$, then $\ldsubeq i p{\delta'}{\delta}\E$.

Induction on $\D$.
Use the symmetry of related types to obtain the goal.

If $\D :: \ldctxeq i p{\Delta_1}{\Delta_2}$, $\E :: \ldctxeq i
p{\Delta_1}{\Delta_3}$ and $\ldsubeq i p{\delta}{\delta'}\D$, then
$\ldsubeq i p{\delta}{\delta'}\E$.

Do induction on $\D$ and then invert $\E$.
Use the right irrelevance of related terms.

If $\D :: \ldctxeq i p{\Delta_1}{\Delta_2}$, $\E :: \ldctxeq i
p{\Delta_3}{\Delta_1}$ and $\ldsubeq i p{\delta}{\delta'}\D$, then
$\ldsubeq i p{\delta}{\delta'}\E$.

A direct consequence of right irrelevance and symmetry.

$ $

* If $\D_1 :: \ldctxeq i p{\Delta_1}{\Delta_2}$ and
$\D_2 :: \ldctxeq i p{\Delta_2}{\Delta_3}$, then
$\D_3 :: \ldctxeq i p{\Delta_1}{\Delta_3}$.

* If $\ldsubeq i p{\delta_1}{\delta_2}{\D_1}$ and
$\ldsubeq i p{\delta_2}{\delta_3}{\D_2}$, then
$\ldsubeq i p{\delta_1}{\delta_3}{\D_3}$.

* $\E :: \ldctxeq i p{\Delta_1}{\Delta_1}$.

* If $\ldsubeq i p{\delta_1}{\delta_2}{\D_1}$, then $\ldsubeq i p{\delta_1}{\delta_1}{\E}$.

Do induction on $\D_1$ and then invert $\D_2$.
The proof proceeds very similarly to the relations for types and terms.
We only consider the step case.
In this case, we have the following premises:

* $\F_1 :: \forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot
\ldctxeq[\Phi][L'] i p {\Delta_1'}{\Delta_2'}$,

* $\F_2 :: \forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot
\ldctxeq[\Phi][L'] i p {\Delta_2'}{\Delta_3'}$,

* $\Ac_1 :: \ldStypeq{\F_1} i p {T_1}{T_2} l$,

* $\Ac_2 :: \ldStypeq{\F_2} i p{T_2}{T_3} l$,

* If $\ldStypeq{\F_1} i p T{T'} l$ and $\ldStypeq{\F_2} i p{T'}{T''} l$, then
$\ldStypeq {\F_3} i p T{T''} l$.

* $\forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot \ldtyequiv[\Phi][\Gamma][L']
i p {t_1}{t_2}{\Ac_1(\alpha, \F_1(\alpha))}$,

* $\forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot \ldtyequiv[\Phi][\Gamma][L']
i p {t_2}{t_3}{\Ac_2(\alpha, \F_2(\alpha))}$,

By IH, it is easy to show

\[
\F_3 :: \forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot
\ldctxeq[\Phi][L'] i p {\Delta_1'}{\Delta_3'}
\]

The difficult goals are

* $\Ac_3 :: \ldStypeq{\F_3} i p{T_1}{T_3} l$, and

* $\forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot \ldtyequiv[\Phi][\Gamma][L']
i p {t_1}{t_3}{\Ac_3(\alpha, \F_3(\alpha))}$.

We first assume $\alpha :: L' \sep \Phi \To L \sep \Psi$.
To prove the first statement, we further assume $\ldsubeq[\Phi][\Gamma][L'] i j
\delta{\delta'}{\F_3(\alpha)}$.
Then we do a similar reasoning to the function case for transitivity of related

* We first relate $T_1[\delta]$ and $T_2[\delta]$ by using reflexivity.

* Then we related $T_2[\delta]$ and $T_3[\delta']$.

* Then we apply transitivity of related types.

To prove the second statement, we can simply use irrelevance so that transitivity
can eventually apply on $\Ac_3(\alpha, \F_3(\alpha))$.

* $\F_1 :: \forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot \ldctxeq[\Phi][L'] i p

* $\F_2 :: \forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot \ldctxeq[\Phi][L'] i p
{\Delta_2}{\Delta_3}$, and

* $\F_3 :: \forall~\alpha :: L' \sep \Phi \To L \sep \Psi \cdot \ldctxeq[\Phi][L'] i p

* if $\D_1 :e: \ldStypeq{\F_1} i p T{T'} l$ and $\D_2 :: \ldStypeq{\F_2} i
p{T'}{T''} l$, then $\D_3 :: \ldStypeq{\F_3} i p T{T'} l$;

* if $\ldStyequiv{\F_1} i p t{t'}{\D_1}$ and $\ldStyequiv{\F_2} i p
{t'}{t''}{\D_3}$, then $\ldStyequiv{\F_3} i p t{t''}{\D_3}$.

The first statement is what we have proved in transitivity previously.
The second statement uses the transitivity of related terms.

§ CONSEQUENCES AND DECIDABILITY OF CONVERTIBILITY

In the previous section, we have established the fundamental theorems, and using the
escape lemma, we see that all syntactic equivalent types and terms are also
semantically related by the Kripke logical relations.
In this section, we will instantiate the generic equivalence so that we can obtain
desired properties that are difficult to prove syntactically.

§.§ First Instantiation: Syntactic Equivalence

First we instantiate the generic equivalence with syntactic equivalences of types and
The laws are all easily instantiated by the corresponding equivalence rules.
We also see that the derived equivalences between local contexts and local
substitutions are equivalent to the corresponding syntactic equivalences.
From the fundamental theorems and the escape lemma, we are able to derive the
following lemmas.

$ $

* If $\lttypeq i{\PI{l}{l'} x S T}{\PI{l}{l'} x{S'}{T'}}{l \sqcup l'}$ and
$i \in \{p, m\}$, then $\lttypeq i{S}{S'}l$ and
$\lttypeq[\Psi][\Gamma, x : S ~@~l]i{T}{T'}{l'}$.

* If
$\lttyequiv i{\PI{l}{l'} x s t}{\PI{l}{l'} x{s'}{t'}}{\Ty{l \sqcup l'}}{\su{(l
\sqcup l')}}$ and $i \in \{p, m\}$, then $\lttyequiv i{s}{s'}{\Ty l}{\su l}$ and
$\lttyequiv[\Psi][\Gamma, x : \Elt l s ~@~l]i{t}{t'}{\Ty{l'}}{\su{l'}}$.

* If $\lttypeq m{\CTyp[\Delta]l}{\CTyp[\Delta']l}{\su l}$, then
$\lpequiv p \Delta{\Delta'}$.

* If $\lttypeq m{\CTrm[\Delta] T l}{\CTrm[\Delta'] T l}{l}$, then
$\lpequiv p \Delta{\Delta'}$ and $\lttypeq[\Psi][\Delta] p{T}{T'}l$.

* If $\lttypeq m{\CPI g l T}{\CPI g l{T'}}l$, then
$\lttypeq[\Psi, g : \Ctx] m{T}{T'}l$.

* If
$\lttypeq m{\TPI{U}[\Delta]{l}{l'}{T}}{\TPI{U}[\Delta']{l}{l'}{T'}}{\su l \sqcup
l'}$, then $\lpequiv p \Delta{\Delta'}$ and
$\lttypeq[\Psi, U : \DTyp[\Delta] p l] m{T}{T'}{l'}$.

* If $\lttypeq m{\UPI \ell l T}{\UPI \ell l{T'}}\omega$, then
$\lttypeq[\Psi][\Gamma][L, \vect \ell] m{T}{T'}{l}$.

By fundamental theorems, we pass in all identity substitutions and then we can
extract this fact from the logical relations of types.

We follow <cit.> and give us the consistency proof of .

There is no term $t$ that satisfies this typing judgment:

\[
\lttyping[\cdot][\cdot][\ell] m t{\PI{\su \ell}{\ell}x{\Ty \ell}x}{\su \ell}
\]

That is, there is not a generic way to construct a term of an arbitrary type.

The lemma effectively asks to reject the following derivation after applying the
fundamental theorems:

\[
\lttyping[\cdot][x : \Ty \ell ~@~\su \ell][\ell] m t x \ell
\]

Now by the logical relations of the neutral type $x$, we know that $t$ must also be
neutral, so we now move on to rejecting

\[
\lttyping[\cdot][x : \Ty \ell ~@~\su \ell][\ell] m v x \ell
\]

Then we do induction on $v$.
It is impossible to do any operation on $v$ but to refer to $x$ ultimately, but then
$x$ has type $\Ty \ell$ which cannot be equivalent to $x$, as they both have reached
normal forms and it is not possible to relate any two distinguished normal forms in
any case by the logical relations.

§.§ Second Instantiation: Convertibility Checking

In this section, we perform our second instantiation by specifying the generic
equivalence to be the convertibility checking judgments.
This second instantiation is not very immediate for some laws for the generic
equivalence, so we must do some verification, using the results from the first

* $\lttypgneeq i V{V'} l$ is $\tconvtypne i V{V'}l$.

* $\lttypgeq i {T}{T'} l$ is $\tconvtyp i T{T'} l$.

* $\lttrmgneeq i \mu{\mu'} T l$ is $\tconvtrmne i \mu{\mu'}{T'} l$ and
$\lttypeq i T{T'} l$.

* $\lttrmgeq i t{t'} T l$ is $\tconvtrm i t{t'}T l$.

Most laws are quite straightforward, except the conversion laws and the PER laws.
Let us consider the conversion laws first.
We must show that the convertibility checking algorithm is invariant under contexts
and types.
Intuitively, this should be true, but it is not very easy to prove, until we obtain
the injectivity lemma after the first instantiation.

$ $

* if $\tconvtyp i T{T'} l$, $\gequiv\Phi\Psi$ and
$\lpequiv[\Phi]{i}\Delta\Gamma$, then $\tconvtyp[\Phi][\Delta] i T{T'} l$.

* if $\tconvtypnf i W{W'} l$, $\gequiv\Phi\Psi$ and
$\lpequiv[\Phi]{i}\Delta\Gamma$, then $\tconvtypnf[\Phi][\Delta] i W{W'} l$.

* if $\tconvtypne i V{V'}l$, $\gequiv\Phi\Psi$ and
$\lpequiv[\Phi]{i}\Delta\Gamma$, then $\tconvtypne[\Phi][\Delta] i V{V'}l$.

* if $\tconvctx i \Gamma \Delta$ and $\gequiv\Phi\Psi$, then $\tconvctx[\Phi] i \Gamma \Delta$.

* if $\tconvtrm i t{t'}T l$, $\gequiv\Phi\Psi$, $\lpequiv[\Phi]{i}\Delta\Gamma$
and $\lttypeq[\Phi][\Delta] i{T'} T l$, then
$\tconvtrm[\Phi][\Delta] i t{t'}{T'} l$.

* if $\tconvtrmnf i w{w'}W l$, $\gequiv\Phi\Psi$, $\lpequiv[\Phi]{i}\Delta\Gamma$
and $\lttypeq[\Phi][\Delta] i{W'}W l$, then $\lttyequiv[\Phi][\Delta] i w{w'}{W'} l$;

* if $\tconvtrmne i \mu{\mu'}T l$, $\gequiv\Phi\Psi$ and
$\lpequiv[\Phi]{i}\Delta\Gamma$, then $\tconvtrmne[\Phi][\Delta] i \mu{\mu'}{T'} l$
and $\lttypeq i{T'}{T}l$ for some $T'$.

* if $\tconvtrmnee i \mu{\mu'}W l$, $\gequiv\Phi\Psi$ and
$\lpequiv[\Phi]{i}\Delta\Gamma$, then $\lttyequiv[\Phi][\Delta] i \mu{\mu'}{W'} l$
and $\lttypeq i{W'}{W}l$ for some $W'$.

* if $\tconvsub i{\delta}{\delta'}\Delta$, $\gequiv\Phi\Psi$,
$\lpequiv[\Phi]{i}{\Gamma'}\Gamma$ and $\lpequiv[\Phi]{i}{\Delta'}\Delta$, then
$\tconvsub[\Phi][\Gamma'] i{\delta}{\delta'}{\Delta'}$.

We do induction on all derivations.
Most cases are immediate.
When we get under binders, we need to extend the context equivalences, in which case
we should use the soundness lemma to obtain the well-formedness of the type that
needs to be extended to the contexts.

We consider a few cases.

T W
i t w T l
t'w'T l
i ww'W l
i tt'T l

The most important thing to notice is that by $\lttypeq[\Phi][\Delta] i{T'} T l$
and $T \reds W$, we know that $T' \reds W'$ for some $W'$. Therefore we can prove
this case using IH.
Other premises are satisfied by syntactic context equivalence lemmas.

i S l
i w ll'xSTl ⊔l'
i w'll'xSTl ⊔l'
[Ψ][Γ, x : S  @ l] i wll'xSTxw'll'xSTxTl'
iww'll'xSTl ⊔l'

In this case, we know $\lttypeq[\Phi][\Delta] i{W'}{\PI{l}{l'}x{S}{T}}{l \sqcup
By the fundamental theorems, we know that $W'$ can only reduce to some $\Pi$
Since $W'$ is already normal, it is only possible for $W'$ to be some $\Pi$
Say $W' = {\PI{l}{l'}x{S'}{T'}}$.
Then by injectivity, we know $S \approx S'$ and $T \approx T'$.
We obtain our goal by extending the local contexts.

i μμ'W l
i μμ'V l

In this case, the type equivalence is irrelevant.
When hitting neutral types, we simply ignore the type $W$ inferred by
$\tconvtrmnee i \mu{\mu'}{W} l$.

i μμ'Tl
T W
i μμ'W l

In this case, we simply apply IH. Then we know

\[
T \reds W \tand T' \reds W'
\]

Our goal is to show $W \approx W'$.
But this is immediate from the determinacy lemma of multi-step reduction and the
fundamental theorems.

i Γ
x : T  @  l ∈Γ
i xxT l

The goal is given by the equivalence between $\Gamma$ and $\Delta$.

i SS'l_1

[Ψ][Γ, x : S  @ l_1] iTT'l_2

i μμ'l_1l_2 xS”T”l_1 ⊔l_2
i ss' Sl_1
iμl_1l_2 x S T sμ'l_3l_4 x S'T's'T[s/x]l_2

By IH, we know from
$\tconvtrmnee i \mu{\mu'}{\PI {l_1}{l_2} x{S''}{T''}}{l_1 \sqcup l_2}$ that there
must be $W'$, so that

\[
\lttypeq i{W'}{\PI {l_1}{l_2} x{S''}{T''}}{l_1 \sqcup l_2}
\]

By the fundamental theorems, we know $W'$ must be some $\Pi$ types.
The return type is fixed so we do not have to do anything.

From the conversion lemma, we see that both $\tconvtrmne i \mu{\mu'}T l$ and
$\tconvtrmnee i \mu{\mu'}W l$ return some equivalent types because they are in fact
inference steps.
Therefore, it makes sense when we instantiate $\lttrmgneeq i \mu{\mu'} T l$, we hide a
syntactic equivalence judgment inside.

For the PER laws, we see that the difficulties primarily come from the convertibility
checking of neutrals, because again they are inference steps.
Moreover, due to their left-biased design, in general it is not true that the inferred
types can be replaced by their equivalence.
However, since we are hiding an equivalence judgment in $\lttrmgneeq i \mu{\mu'} T l$
during instantiation, following the same principle as the conversion lemma, we are
able to erase the effect of the left bias and establish the PER laws.

The instantiation immediately gives us the convertibility lemma once we apply the
escape lemma:
$ $

* If $\lttypwf i T l$, then $\tconvtyp i T T l$.

* If $\lttypeq i T{T'} l$, then $\tconvtyp i T{T'} l$.

* If $\lttyping i t T l$, then $\tconvtrm i t t T l$.

* If $\lttyequiv i t{t'} T l$, then $\tconvtrm i t{t'} T l$.

In particular, we see that the convertibility checking algorithm is both sound and
complete w.r.t. the syntactic equivalence judgments.
The decidability of type checking requires the following lemma by attempting to relate
two reflexively convertible types or terms.

$ $

* if $\tconvtyp[\Phi][\Delta] i T{T} l$, $\tconvtyp i {T'}{T'} l$,
$\gequiv\Phi\Psi$ and $\lpequiv[\Phi]{i}\Delta\Gamma$, then whether
$\tconvtyp[\Phi][\Delta] i T{T'} l$ is decidable.

* if $\tconvtypnf[\Phi][\Delta] i W{W} l$, $\tconvtypnf i{W'}{W'} l$,
$\gequiv\Phi\Psi$ and $\lpequiv[\Phi]{i}\Delta\Gamma$, then whether
$\tconvtypnf[\Phi][\Delta] i W{W'} l$ is decidable.

* if $\tconvtypne[\Phi][\Delta] i V{V}l$, $\tconvtypne i {V'}{V'}l$,
$\gequiv\Phi\Psi$ and $\lpequiv[\Phi]{i}\Delta\Gamma$, then whether
$\tconvtypne[\Phi][\Delta] i V{V'}l$ is decidable.

* if $\tconvctx[\Phi] i \Gamma \Gamma$, $\tconvctx i \Delta \Delta$ and
$\gequiv\Phi\Psi$, then whether $\tconvctx[\Phi] i \Gamma \Delta$ is decidable.

* if $\tconvtrm[\Phi][\Delta] i t{t}T l$, $\tconvtrm i{t'}{t'}{T} l$,
$\gequiv\Phi\Psi$ and $\lpequiv[\Phi]{i}\Delta\Gamma$, then whether
$\tconvtrm[\Phi][\Delta] i t{t'}{T} l$ is decidable.

* if $\tconvtrmnf[\Phi][\Delta] i w{w}W l$, $\tconvtrmnf i {w'}{w'}{W} l$,
$\gequiv\Phi\Psi$ and $\lpequiv[\Phi]{i}\Delta\Gamma$, then whether
$\lttyequiv[\Phi][\Delta] i w{w'}{W} l$ is decidable.

* if $\tconvtrmne[\Phi][\Delta] i \mu{\mu}T l$,
$\tconvtrmne i {\mu'}{\mu'}{T'} l$, $\gequiv\Phi\Psi$ and
$\lpequiv[\Phi]{i}\Delta\Gamma$, then whether
$\tconvtrmne[\Phi][\Delta] i \mu{\mu'}{T''} l$ for some $T''$ is decidable.

* if $\tconvtrmnee[\Phi][\Delta] i \mu{\mu}W l$,
$\tconvtrmnee i {\mu'}{\mu'}{W'} l$, $\gequiv\Phi\Psi$ and
$\lpequiv[\Phi]{i}\Delta\Gamma$, then whether
$\lttyequiv[\Phi][\Delta] i \mu{\mu'}{W''} l$ is decidable.

* if $\tconvsub[\Phi][\Gamma'] i{\delta}{\delta}{\Delta}$,
$\tconvsub i{\delta'}{\delta'}{\Delta}$, $\gequiv\Phi\Psi$ and
$\lpequiv[\Phi]{i}{\Gamma'}\Gamma$, then whether
$\tconvsub[\Phi][\Gamma'] i{\delta}{\delta'}{\Delta}$ is decidable.

We do a mutual induction on the first derivations and then invert the second ones.
We can reject most cases when they have different root derivations.
We consider a few cases.

[Φ][Δ] i T W l

i WW l
[Φ][Δ] i TT l

iT'W' l

iW'W' l
i TT' l

In this case, we apply IH to decide whether $W$ and $W'$ are convertible.

[Φ][Δ] i SS l
[Φ][Δ, x : S  @  l] i TTl'
[Φ][Δ] ill'xSTll'xSTl ⊔l'

iS'S' l
[Ψ][Γ, x : S'  @  l] iT'T'l'
ill'xS'T'll'xS'T'l ⊔l'

We can decide whether $S$ and $S'$ are convertible by IH.
When we decide $T$ and $T'$, we must extend the equivalent local contexts.

T W
[Φ][Δ] i t w T l

[Φ][Δ] i wwW l
[Φ][Δ] i ttT l

T' W'
it'w'T' l

i w'w'W' l
i t't'T l

By fundamental theorems, we know $W \approx W'$.
Then by IH, we can decide whether $w$ and $w'$ are convertible.

[Φ][Δ] i S l
[Φ][Δ] i w
ll'xSTl ⊔l'

[Φ][Δ, x : S  @ l] i wll'xSTxwll'xSTxTl'
[Φ][Δ] iwwll'xSTl ⊔l'

iS l
iw'll'xSTl ⊔l'

[Ψ][Γ, x : S  @ l] i w'll'xSTxw'll'xSTxTl'
iw'w'll'xSTl ⊔l'

Again, it is quite immediate by IH.

[Φ][Δ] i μμW l
[Φ][Δ] i μμV l

i μ'μ'W' l
i μ'μ'V l

By IH, we know $\tconvtrmnee[\Phi][\Delta] i \mu{\mu'}{W''} l$ for some $W''$.

[Φ][Δ] i μμTl
T W
[Φ][Δ] i μμW l

i μ'μ'T'l
T' W'
i μ'μ'W' l

By IH, we have $\tconvtrmne i {\mu'}{\mu'}{T''}{l}$ for some $T''$.
$T''$ will reduce to some normal form by the fundamental theorems.

$ $

* If $\lttypwf i T l$ and $\lttypwf i{T'} l$, then whether $\tconvtyp i T{T'} l$
is decidable.

* If $\lttyping i t T l$ and $\lttyping i{t'} T l$, then whether
$\tconvtrm i t{t'}T l$ is decidable.

First we use the fundamental theorems from the second instantiation to show that
both types (or terms, resp.) are reflexively convertible.
Then we use the decidability lemma above.

At this point, we have justified the decidability of convertibility checking of
and therefore conclude our investigations.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

authorpersonAndreas Abel.
titleNormalization by evaluation: dependent types
and impredicativity.
Habilitation thesis.
schoolLudwig-Maximilians-Universität München.

[Abel, Öhman, and VezzosiAbel
et al2017]
authorpersonAndreas Abel, personJoakim
Öhman, and personAndrea Vezzosi.
Decidability of conversion for type theory in type
journalProceedings of the ACM on Programming
Languages volume2, numberPOPL (dateDec.
year2017), pages23:1–23:29.

[Bezem, Coquand, Dybjer, and EscardóBezem
et al2023]
authorpersonMarc Bezem, personThierry
Coquand, personPeter Dybjer, and personMartín
Escardó. year2023.
Type Theory with Explicit Universe
Polymorphism. In
publisherSchloss-Dagstuhl - Leibniz Zentrum für Informatik.

[Hu, Jang, and PientkaHu
et al2023]
authorpersonJason Z. S. Hu, personJunyoung
Jang, and personBrigitte Pientka.
Normalization by evaluation for modal dependent
type theory.
journalJournal of Functional Programming
volume33 (year2023), pagese7.

[Hu and PientkaHu and Pientka2024a]
authorpersonJason Z. S. Hu and
personBrigitte Pientka. year2024a.
titleLayered Modal Type Theories.
[arxiv]2305.06548 [cs.LO]

[Hu and PientkaHu and Pientka2024b]
authorpersonJason Z. S. Hu and
personBrigitte Pientka. year2024b.
Layered Modal Type Theory: Where Meta-programming
Meets Intensional Analysis. In booktitleProgramming
Languages and Systems, editorpersonStephanie
Weirich (Ed.). publisherSpringer Nature Switzerland,
addressCham, pages52–82.

authorpersonErik Palmgren.
On universes in type theory.
In booktitleTwenty Five Years of Constructive
Type Theory. publisherOxford University Press.
978-0-19-850127-5 978-0-19-191654-0

[Pujet and TabareauPujet and
authorpersonLoïc Pujet and personNicolas
Tabareau. year2023.
Impredicative Observational Equality.
journalProceedings of the ACM on Programming
Languages volume7, numberPOPL (dateJan.
year2023), pages74:2171–74:2196.