# nLab Initiality Project - Substitution

Initiality Project - Substitution

# Initiality Project - Substitution

## Statements

Based on the definition of the partial interpretation functions, we now prove the following substitution properties by mutual induction over raw terms and types.

### Weakening, exchange, and contraction

Let $V_1,V_2 \subseteq Var$ be finite, and suppose $\theta : V_1\to V_2$ is a function. Then:

• For any raw type $A$, the composite partial morphism $Tm^{V_2} \xrightarrow{Tm^\theta} Tm^{V_1} \overset{\⟦ A \⟧^{V_1}_{type}}\rightharpoonup Ty$ is contained in the partial morphism $Tm^{V_2} \overset{\⟦ A[\theta] \⟧^{V_2}_{type}}\rightharpoonup Ty$.
• For any raw term $T$, the composite partial morphism $Tm^{V_2} \xrightarrow{Tm^\theta} Tm^{V_1} \overset{\⟦ T \⟧^{V_1}_{\Rightarrow}}\rightharpoonup Tm$ is contained in the partial morphism $Tm^{V_2} \overset{\⟦ T[\theta] \⟧^{V_2}_{\Rightarrow}}\rightharpoonup Tm$.
• For any raw term $T$, the composite partial morphism $Tm^{V_2}\times Ty \xrightarrow{Tm^\theta} Tm^{V_1} \times Ty \overset{\⟦ T \⟧^{V_1}_{\Leftarrow}}\rightharpoonup Tm$ is contained in the partial morphism $Tm^{V_2}\times Ty \overset{\⟦ T[\theta] \⟧^{V_2}_{\Leftarrow}}\rightharpoonup Tm$.

Here $A[\theta]$ and $T[\theta]$ denote simultaneous capture-avoiding substitution of $\theta(x)$ for each variable $x\in V_1$. When $\theta$ is a bijection, this asserts invariance under renaming of free variables. When $\theta$ is an inclusion, it asserts weakening, and when $\theta$ is surjective it is contraction. Note that in general these containments can be strict, e.g. if some variable in $V_2 \setminus \theta(V_1)$ appears freely in $A$ or $T$, then the composites may have empty domain while the morphisms they are being compared to might not.

### Substitution

Let $V\subseteq Var$ be finite and $x\in Var\setminus V$, while $N$ is a raw term. Then:

• For any raw type $A$, the composite partial morphism $Tm^V \overset{(id,\⟦ N \⟧^V_{\Rightarrow})}{\rightharpoonup} Tm^{V\cup \{x\}} \overset{\⟦ A \⟧^{V\cup \{x\}}_{type}}{\rightharpoonup} Ty$ is contained in the partial morphism $Tm^V \overset{\⟦ A[N/x] \⟧^V_{type}}{\rightharpoonup} Ty$.
• For any raw term $T$, the composite partial morphism $Tm^V \overset{(id,\⟦ N \⟧^V_{\Rightarrow})}{\rightharpoonup} Tm^{V\cup \{x\}} \overset{\⟦ T \⟧^{V\cup \{x\}}_{\Rightarrow}}{\rightharpoonup} Tm$ is contained in the partial morphism $Tm^V \overset{\⟦ T[N/x] \⟧^V_{\Rightarrow}}{\rightharpoonup} Tm$.
• For any raw term $T$, the composite partial morphism $Tm^V\times Ty \overset{(id,\⟦ N \⟧^V_{\Rightarrow},id)}{\rightharpoonup} Tm^{V\cup \{x\}}\times Ty \overset{\⟦ T \⟧^{V\cup \{x\}}_{\Leftarrow}}{\rightharpoonup} Tm$ is contained in the partial morphism $Tm^V \times Ty\overset{\⟦ T[N/x] \⟧^V_{\Leftarrow}}{\rightharpoonup} Tm$.

## Inductive clauses

TODO.

Last revised on November 2, 2018 at 19:45:40. See the history of this page for a list of all contributions to it.