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 of contexts;
For , the meta-set of types over ;
For and , the meta-set of terms of type over ;
For , the meta-set 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

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 , each of which may depend on the previous one. We therefore treat and as presuppositions for the judgement .

For a judgement thesis we read as

Assuming hypotheses , the judgement thesis holds.

or what is the same

Given a variables of each type , the judgement thesis holds.

Judgemental equality of contexts

We can define equality of contexts recursively by

which is why this judgement is considered redundant.

Substitutions form a category

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

In concert these ensure that the meta-set of contexts and the meta-sets of substitutions form a category, which we also denote . 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:

Given a substitution , these inference rules give rise to the following “pullback” meta-functions, all denoted by :

;
;
.

^PB1 and ^PB3 can be combined to give

Cartesian contexts

First we establish is the terminal object in :

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 :

Notation

To reduce proliferation of parentheses, binds more tightly then .

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

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

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

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,

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

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

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

which in the formal syntax is

Elementary properties

Terms are in bijection with substitutions satisfying .
For , , and we have .
For and we have a bijection natural in so that for any commutes.

Proof of 1–3

For ^P1, first suppose we have . Then letting we have by . This gives the forward direction of our bijection. On the other hand, suppose we have where . Then by , we have . This gives us the reverse direction of our bijection. To see that these are indeed inverses, note

and

which completes the proof of ^P1.

For ^P2, first note

proving ^P2.

For ^P3, first suppose we have . Then we have

and

so and gives us the forward direction of our bijection. On the other hand, suppose and . Then

so gives us the reverse direction. To see that these are indeed inverses, note that by , by , and by . For naturality, suppose and . Since

and

it follows

This completes the proof of ^P3.

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