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 $Γ$ ).[^1]
$Γ ⊢ 𝑎 : 𝐴$ , 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 ⊢ Γ ⊢ Γ ⊢ 𝐴 Γ . 𝐴 ⊢

A context is thus a list of types $Γ = \emptyset . 𝐴 1 \dots 𝐴 𝑛$ , each of which may depend on the previous one. Thus we ready $Γ ⊢ 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$ .

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$ .

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]

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 subsitution extension $𝛾 . 𝑎$ , which given a substitution $Δ : 𝛾 ⊢ Γ$ allows us to use the hypotheses of $Δ$ to fill an additional hypothesis $Γ ⊢ 𝐴$ :

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

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 𝛾) . (𝐪 Γ, 𝐴 [𝛾]) : Γ . 𝐴 (𝜂 𝐩 𝐪)

Syntax sugar for named variables

While the above presentation has nice formal properties, its use of De Brujin indices makes it hard to parse. 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 [𝐢 𝐝 . 𝑎]

tidy | en | SemBr

Table of Contents

Cartesian calculus of substitutions

Judgements

Inference rules

Context formation

Substitutions form a category

Substitutions act on types and terms from the right

Cartesian contexts

Syntax sugar for named variables

Graph View

Backlinks