Cartesian calculus of substitutions

The (cartesian) calculus of substitutions is one way of presenting a (dependent, cartesian) type theory as a formal system which is naturally viewed as having semantics in a cartesian category. It can be viewed as an extension of the linear calculus of substitutions, but here we give a full presentation following Principles of dependent type theory.

Notes on this presentation

We use De Brujin indices, and describe Syntax sugar for named variables. Following Principles, “implicit” arguments are made explicit in grey, for example we have $Γ ⊢ 𝐢 𝐝 Γ : Γ$ . We also have “meta-implicit arguments” for judgements, which are called presuppositions (notation 2.2.1). The surface syntax for our judgements differs slightly.

Judgements

We have the following basic judgements:

$Γ ⊢$ asserts that $Γ$ is a context.
$Γ ⊢ 𝐴$ asserts that $𝐴$ is a type (in context $Γ$ ).
$Γ ⊢ 𝑎 : 𝐴$ , presupposing $Γ ⊢$ and $⊢ 𝐴$ , asserts that $𝑎$ is a term of type $𝐴$ in context $Γ$ .
$Γ ⊢ 𝛾 : Δ$ , presupposing $Γ ⊢$ and $Δ ⊢$ , asserts that $𝛾$ is a substitution from $Γ$ to $Δ$ , that is, $𝛾$ fills all the hypotheses of $Δ$ with terms in $Γ$ .

We also have the following manifestations of judgemental equality:

$Δ ⊢ 𝛾 = 𝛾' : Γ$ , presupposing $Δ ⊢ 𝛾 : Γ$ and $Δ ⊢ 𝛾' : Γ$ , asserts that $𝛾$ and $𝛾'$ are equal substitutions from $Δ$ to $Γ$ .
$Γ ⊢ 𝐴 = 𝐴'$ , presupposing $Γ ⊢ 𝐴$ and $Γ ⊢ 𝐴'$ , asserts that $𝐴$ and $𝐴'$ are equal types in context $Γ$ .
$Γ ⊢ 𝑎 = 𝑎' : 𝐴$ , presupposing $Γ ⊢ 𝑎 : 𝐴$ and $Γ ⊢ 𝑎' : 𝐴$ , asserts that $𝑎$ and $𝑎'$ are equal terms of type $𝐴$ in context $Γ$ .

We will also sometimes consider

$Δ = Γ ⊢$ , presupposing $Δ ⊢$ and $Γ ⊢$ , asserts that $Δ$ and $Γ$ are equal contexts,

although this is redundant as it reduces to equality of types. Judgemental structure suggests the following meta-sets:

The meta-set $C x = {Γ : ∣ : Γ ⊢}$ of contexts;
For $Γ \in C x$ , the meta-set $T y (Γ) = {𝑇 : ∣ : Γ ⊢ 𝑇}$ of types over $Γ$ ;
For $Γ \in C x$ and $𝑇 \in T y (Γ)$ , the meta-set $T m (Γ, 𝑇) = {𝑡 : ∣ : Γ ⊢ 𝑡 : 𝑇}$ of terms of type $𝑇$ over $Γ$ ;
For $Γ, Δ \in C x$ , the meta-set $S b (Δ, Γ) = {𝛾 : ∣ : Δ ⊢ 𝛾 : Γ}$ of substitutions from $Δ$ to $Γ$ .

In practice these may be thought of as equivalence classes of derivation trees with the appropriate judgement at the root.

Inference rules

Context formation

The creation of contexts is governed by

\emptyset ⊢ Γ ⊢ Γ ⊢ 𝐴 Γ . 𝐴 ⊢

giving the empty context and context extension respectively. Since these are the only way contexts are formed, they establish that every context is a list of types $Γ = \emptyset . 𝐴 1 \dots 𝐴 𝑛$ , each of which may depend on the previous one. We therefore treat $Γ ⊢$ and $Γ ⊢ 𝐴$ as presuppositions for the judgement $Γ . 𝐴 ⊢$ .

For a judgement thesis $J$ we read $Γ ⊢ J$ as

Assuming hypotheses $𝐴 1, \dots, 𝐴 𝑛$ , the judgement thesis $J$ holds.

or what is the same

Given a variables of each type $𝐴 1, \dots, 𝐴 𝑛$ , the judgement thesis $J$ holds.

Judgemental equality of contexts

We can define equality of contexts recursively by

\emptyset = \emptyset ⊢ Γ = Δ ⊢ Γ ⊢ 𝐴 = 𝐵 Γ, 𝐴 = Δ, 𝐵 ⊢

which is why this judgement is considered redundant.

Substitutions form a category

The “algebra” of substitutions is governed by the following inference rules:

Γ ⊢ Γ ⊢ 𝐢 𝐝 Γ : Γ Γ 2 ⊢ 𝛾 1 : Γ 1 Γ 1 ⊢ 𝛾 0 : Γ 0 Γ 2 ⊢ 𝛾 0 \circ Γ 0, Γ 1, Γ 2 𝛾 1 : Γ 0

Δ ⊢ 𝛾 : Γ Δ ⊢ 𝐢 𝐝 Γ \circ 𝛾 = 𝛾 : Γ Δ ⊢ 𝛾 : Γ Δ ⊢ 𝛾 \circ 𝐢 𝐝 Δ = 𝛾 : Γ

Γ 1 ⊢ 𝛾 0 : Γ 0 Γ 2 ⊢ 𝛾 1 : Γ 1 Γ 3 ⊢ 𝛾 2 : Γ 2 Γ 3 ⊢ 𝛾 0 \circ (𝛾 1 \circ 𝛾 2) = (𝛾 0 \circ 𝛾 1) \circ 𝛾 2 : Γ 0

In concert these ensure that the meta-set of contexts $C x$ and the meta-sets of substitutions $S b (Δ, Γ)$ form a category, which we also denote $C x$ . Due to the final rule, we unambiguously omit brackets in compositions.

Substitutions act on types and terms from the right

Substitutions act on both types and terms on the right, so:

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝐴 Δ ⊢ 𝐴 [𝛾] Δ, Γ Δ ⊢ 𝛾 : Γ Γ ⊢ 𝑎 : 𝐴 Δ ⊢ 𝑎 [𝛾] Δ, Γ : 𝐴 [𝛾]

Moreover, this action respects the categorical structure of substitutions:

Γ ⊢ 𝐴 Γ ⊢ 𝐴 [𝐢 𝐝 Γ] = 𝐴 Γ ⊢ 𝑎 : 𝐴 Γ ⊢ 𝑎 [𝐢 𝐝 Γ] = 𝑎 : 𝐴

Γ 2 ⊢ 𝛾 1 : Γ 1 Γ 1 ⊢ 𝛾 0 : Γ 0 Γ 0 ⊢ 𝐴 Γ 2 ⊢ 𝐴 [𝛾 0 \circ 𝛾 1] = 𝐴 [𝛾 0] [𝛾 1]

Γ 2 ⊢ 𝛾 1 : Γ 1 Γ 1 ⊢ 𝛾 0 : Γ 0 Γ 0 ⊢ 𝑎 : 𝐴 Γ 2 ⊢ 𝑎 [𝛾 0 \circ 𝛾 1] = 𝑎 [𝛾 0] [𝛾 1] : 𝐴 [𝛾 0 \circ 𝛾 1]

Given a substitution $Δ ⊢ 𝛾 : Γ$ , these inference rules give rise to the following “pullback” meta-functions, all denoted by $𝛾 *$ :

$𝛾 * : 𝜉 \mapsto 𝜉 \circ 𝛾 : S b (Γ, Ξ) \to S b (Δ, Ξ)$ ;
$𝛾 * : 𝐴 \mapsto 𝐴 [𝛾] : T y (Γ) \to T y (Δ)$ ;
$𝛾 * : 𝑎 \mapsto 𝑎 [𝛾] : T m (Γ, 𝐴) \to T m (Δ, 𝛾 * 𝐴)$ .

^PB1 and ^PB3 can be combined to give

$∐ 𝛿 * 𝛿 * : (𝛾, 𝑎) \mapsto (𝛿 * 𝛾, 𝛿 * 𝑎) : ∐ 𝛾 \in S b (Δ 1, Γ) T m (Δ 1, 𝐴 [𝛾]) \to ∐ 𝛾 \in S b (Δ 0, Γ) T m (Δ 0, 𝐴 [𝛾])$

Cartesian contexts

First we establish $\emptyset$ is the terminal object in $C x$ :

Γ ⊢ Γ ⊢! Γ : \emptyset Γ ⊢ 𝛿 : \emptyset Γ ⊢! Γ = 𝛿 : \emptyset

We now establish that $Γ . 𝐴$ is something like a categorical product. For the “universal morphism” we have the substitution extension $𝛾 . 𝑎$ , which given a substitution $Δ : 𝛾 ⊢ Γ$ allows us to use the hypotheses of $Δ$ to fill an additional hypothesis $Γ ⊢ 𝐴$ :

Δ ⊢ 𝛾 : Γ Γ ⊢ 𝐴 Δ ⊢ 𝑎 : 𝐴 [𝛾] Δ ⊢ 𝛾 . Δ, Γ, 𝐴 𝑎 : Γ . 𝐴 (X)

Notation

To reduce proliferation of parentheses, $(.)$ binds more tightly then $(\circ)$ .

The left projection $𝐩$ is called weakening, since it allows us to add arbitrary hypotheses onto the end of a domain context:

Γ ⊢ 𝐴 Γ . 𝐴 ⊢ 𝐩 Γ, 𝐴 : Γ (W)

The right projection $𝐪$ is called the variable substitution since it allows us to recover the last variable declared in a context:

Γ ⊢ 𝐴 Γ . 𝐴 ⊢ 𝐪 Γ, 𝐴 : 𝐴 [𝐩 Γ, 𝐴] (V)

Finally, we have ” $𝛽$ ” and “ $𝜂$ ” rules giving the universal property:

Δ ⊢ 𝛾 : Γ Δ ⊢ 𝑎 : 𝐴 [𝛾] Δ ⊢ 𝐩 Γ, 𝐴 \circ (𝛾 . 𝑎) = 𝛾 : Γ (𝛽 𝐩) Δ ⊢ 𝛾 : Γ Δ ⊢ 𝑎 : 𝐴 [𝛾] Δ ⊢ 𝐪 Γ, 𝐴 [𝛾 . 𝑎] = 𝑎 : 𝐴 [𝛾] (𝛽 𝐪)

Δ ⊢ 𝛾 : Γ . 𝐴 Δ ⊢ 𝛾 = (𝐩 Γ, 𝐴 \circ 𝛾) . (𝐪 Γ, 𝐴 [𝛾]) : Γ . 𝐴 (𝜂 𝐩 𝐪)

We can use these to define the auxiliary operation of Substitution extension by a type.

Syntax sugar for named variables

While the above presentation has nice formal properties, its use of De Brujin indices has a negative effect on human readability. Note that by the variable and weakening rules,

\emptyset . 𝐴 0 \dots 𝐴 𝑛 ⊢ 𝐪 [𝐩 𝑖] : 𝐴 𝑛 - 𝑖

so we can see $𝐪 [𝐩 𝑖]$ as picking out the $𝑖$ th last variable declared (0-indexed). We will informally use the alternate surface syntax of named variables

𝑥 𝑛 : 𝐴 0, \dots, 𝑥 0 : 𝐴 𝑛 ⊢ 𝑥 𝑖 : 𝐴 𝑛 - 𝑖

for the same judgement. These should be viewed as syntax sugar reducing to judgements of the form given above, so for example

𝑦 𝑛 : 𝐴 0, \dots, 𝑦 0 : 𝐴 𝑛 ⊢ 𝑦 𝑖 : 𝐴 𝑛 - 𝑖

is the same judgement. When applying substitutions into named contexts, we are explicit about which named variable is being substituted into, for example we have

Γ, 𝑥 : 𝐴 ⊢ J Γ ⊢ 𝑎 : 𝐴 Γ ⊢ J [𝑎 / 𝑥]

which in the formal syntax is

Γ . 𝐴 ⊢ J Γ ⊢ 𝑎 : 𝐴 Γ ⊢ J [𝐢 𝐝 . 𝑎]

Elementary properties

Terms $Γ ⊢ 𝑎 : 𝐴$ are in bijection with substitutions $Γ ⊢ 𝛾 : Γ . 𝐴$ satisfying $𝐩 \circ 𝛾 = 𝐢 𝐝$ .
For $Δ ⊢ 𝛾 : Γ$ , $Ξ ⊢ 𝛿 : Δ$ , and $Δ ⊢ 𝑎 : 𝐴 [𝛾]$ we have $Ξ ⊢ 𝛾 . 𝑎 \circ 𝛿 = (𝛾 \circ 𝛿) . 𝑎 [𝛿] : Γ . 𝐴$ .
For $Γ, Δ \in C x$ and $𝐴 \in T y (Γ)$ we have a bijection $𝜄 Δ, Γ, 𝐴 : S b (Δ, Γ . 𝐴) ≅ ∐ 𝛾 \in S b (Δ, Γ) T m (Δ, 𝐴 [𝛾])$ natural in $Δ$ so that for any $Δ 0 ⊢ 𝛿 : Δ 1$ commutes.

Proof of 1–3

For ^P1, first suppose we have $Γ ⊢ 𝑎 : 𝐴$ . Then letting $Γ ⊢ 𝛾 : = 𝐢 𝐝 . 𝑎 : Γ . 𝐴$ we have $𝐩 \circ 𝛾 = 𝐢 𝐝$ by $𝛽 𝐩$ . This gives the forward direction of our bijection. On the other hand, suppose we have $Γ ⊢ 𝛾 : Γ . 𝐴$ where $𝐩 \circ 𝛾 = 𝐢 𝐝$ . Then by $V$ , we have $Γ ⊢ 𝐪 [𝛾] : 𝐴$ . This gives us the reverse direction of our bijection. To see that these are indeed inverses, note

Γ ⊢ 𝐢 𝐝 . 𝐪 [𝛾] = (𝐩 \circ 𝛾) . 𝐪 [𝛾] 𝜂 𝐩 𝐪 = 𝛾 : Γ . 𝐴

and

Γ ⊢ 𝐪 [𝐢 𝐝 . 𝑎] 𝛽 𝐪 = 𝑎 : 𝐴 [𝐢 𝐝] = 𝐴

which completes the proof of ^P1.

For ^P2, first note

𝛾 . 𝑎 \circ 𝛿 = (𝐩 \circ 𝛾 . 𝑎 \circ 𝛿) . 𝐪 [𝛾 . 𝑎 \circ 𝛿] (𝜂 𝐩 𝐪) = (𝛾 \circ 𝛿) . 𝐪 [𝛾 . 𝑎] [𝛿] (𝛽 𝐩) = (𝛾 \circ 𝛿) . 𝑎 [𝛿] (𝛽 𝐪)

proving ^P2.

For ^P3, first suppose we have $Δ ⊢ 𝛾 : Γ . 𝐴$ . Then we have

Δ ⊢ 𝛾 : Γ . 𝐴 Γ ⊢ 𝐴 Γ . 𝐴 ⊢ 𝐩 : Γ (W) Δ ⊢ 𝐩 \circ 𝛾 : Γ

and

Δ ⊢ 𝛾 : Γ . 𝐴 Γ ⊢ 𝐴 Γ . 𝐴 ⊢ 𝐪 : 𝐴 [𝐩] (V) Δ ⊢ 𝐪 [𝛾] : 𝐴 [𝐩 \circ 𝛾]

so $𝛾 0 : = 𝐩 \circ 𝛾$ and $𝑎 : = 𝐪 [𝛾]$ gives us the forward direction of our bijection. On the other hand, suppose $Δ ⊢ 𝛾 0 : Γ$ and $Δ ⊢ 𝑎 : 𝐴 [𝛾 0]$ . Then

Δ ⊢ 𝛾 0 : Γ Γ ⊢ 𝐴 Δ ⊢ 𝑎 : 𝐴 [𝛾] Δ ⊢ 𝛾 0 . 𝑎 : Γ . 𝐴 (E)

so $𝛾 : = 𝛾 0 . 𝑎$ gives us the reverse direction. To see that these are indeed inverses, note that $Δ ⊢ 𝐩 \circ 𝛾 0 . 𝑎 = 𝛾 0 : Γ$ by $𝛽 𝐩$ , $Δ ⊢ 𝐪 [𝛾 0 . 𝑎] = 𝑎 : 𝐴 [𝛾 0]$ by $𝛽 𝐪$ , and $Δ ⊢ (𝐩 \circ 𝛾) . 𝐪 [𝛾] = 𝛾 : Γ . 𝐴$ by $𝜂 𝐩 𝐪$ . For naturality, suppose $Δ 0 ⊢ 𝛿 : Δ 1$ and $Δ 1 ⊢ 𝛾 : Γ . 𝐴$ . Since

𝛿 * (𝐩 \circ 𝛾) = 𝐩 \circ 𝛾 \circ 𝛿 = 𝐩 \circ 𝛿 * 𝛾

and

𝛿 * (𝐪 [𝛾]) = 𝐪 [𝛾 \circ 𝛿] = 𝐪 [𝛿 * 𝛾]

it follows

∐ 𝛿 * 𝛿 * \circ 𝜄 Δ 1, Γ, 𝐴 (𝛾) = 𝜄 Δ 0, Γ, 𝐴 \circ 𝛿 * (𝛾) .

This completes the proof of ^P3.

#state/tidy | #lang/en | #SemBr