A derivation about renaming variables

We are going to derive the inference rule

\[\dfrac{\Gamma, x:A,\Delta \vdash \mathscr{J}} {\Gamma,x':A,\Delta[x'/x] \vdash \mathscr{J}[x'/x]}x'/x\] which essentially says “we an replace variable \(x:A\) by variable \(x':A\)”.

The derivation uses substitution, weakening and the generic element:

\[\dfrac{ \dfrac{\Gamma \vdash A \ \text{type}}{\Gamma,x':A \vdash x':A}\delta \quad \dfrac{\Gamma \vdash A \ \text{type}\quad \Gamma, x:A, \Delta \vdash \mathscr{J}} {\Gamma,x':A,x:A,\Delta \vdash \mathscr{J}}W } {\Gamma,x':A,\Delta[x'/x]\vdash \mathscr{J}[x'/x]}S\]

Dependent function types

Let \(b\) be a section of a family \(B\) over \(A\) in context \(\Gamma\). Thus \[\Gamma,x:A \vdash b(x): B(x).\]

Two points of view here:

• can think of \(b\) as a “program” \(x \mapsto b(x)\) that takes as input \(x:A\) and produces a term \(b(x):B(x)\).

• or, can view \(b(x)\) as just a “choice of element” in each \(B(x)\) for \(x:A\). i.e. \(x \mapsto b(x)\) is a dependent function

The type of all such dependent functions is called the dependent function type, written: \[\Pi_{(x:A)} B(x)\]

Part of what we must formulate in our type theory are inference rules guaranteeing that these types are well-formed. For this we need various sorts of rules:

• formation rule specifying how we may form dependent function types
• introduction rule specifying how to introduce new terms of dependent function types
• elimination rule specifying how to use arbitrary terms of dependent function types
• computation rules specifying how introduction rules and elimination rules interact

For the first three of these rules, we also need rules asserting that the constructions play nice with judgmental equality.

\(\Pi\)-formation rule

Also need the congruence rule:

\(\Pi\)-introduction rule

This rule specifies that we may “construct” dependent functions provided that we have constructed a section:

We use the notation \(\lambda x.b(x)\) for the “dependent function”. This introduction rule is also called the \(\lambda\)-abstraction rule.

Again, we need to know that \(\lambda\)-abstraction respects judgmental equality:

\(\Pi\)-elimination rule

The way to use a dependent function is to evaluate it at any an element of the domain type. The \(\Pi\)-elimination rule is thus sometimes called the evaluation rule.

(Note that in practice – e.g. in type-theory based programming languages Lean, Haskell, ML, … – we write “\(f\ x\)” for “\(f(x)\)”).

\(\Pi\)-computation rule

We need to postulate rules controlling our functions.

The \(\beta\)-rule stipulates that \(\lambda x. b(x)\) behaves in the way that we understand the function \(x \mapsto b(x)\).

The second rule – known as the \(\eta\)-rule – postulates that the only elements of \(\Pi_{(x:A)}B(x)\) are dependent functions.

Ordinary function types

We obtain ordinary functions as a special case of dependent functions. Let’s describe the setting.

Suppose that \(A\) and \(B\) are types in context \(\Gamma\). We can view \(B\) as the “constant family” \(B(x) = B\) over \(a:A\). From this point of view, we obtain the type of functions as \[A \to B := \Pi_{(x:A)} B(x)\] i.e. \[A \to B := \Pi_{(x:A)}B\]

Here is the formal derivation:

And here is the formal declaration of the “new notation”:

Construction of the identity function

Given a type \(A\) in context \(\Gamma\), let’s construct the identity function \(\operatorname{id}= \operatorname{id}_A:A \to A\) using the generic term:

Construction of the composition of two functions

Given types \(A\), \(B\), \(C\) and terms \(f:A \to B\), \(g:B \to C\), we can form \(g \circ f:A \to C\).

In fact, write \(\operatorname{comp}(g,f)\) for \(g \circ f\). Then \(\operatorname{comp}\) is in some sense a function of two arguments \(g\) and \(f\). Let’s pause to discuss functions of multiple arguments.

Consider a function \[f : A \to (B \to C)\] For an argument \(a:A\), \(f(a):B \to C\) so \(f(a)\) is again a function. For \(b :B\), we can write \[f(a)(b) \quad \text{or} \quad f(a,b) \quad \text{or} \quad f\ a \ b\] for the value of \(f(a)\) at \(b:B\).

Now we see that the type of the function \(\operatorname{comp}\) is \[(B \to C) \to ((A \to B) \to (A \to C))\] Thus for \(g:B \to C\), we have \(\operatorname{comp}(g):(A \to B) \to (A \to C).\)

We are going to define \(\operatorname{comp}\) by the rule \[\operatorname{comp}= \lambda g.\lambda f. \lambda x.g(f(x))\].

Before we give the derivation, we need a preliminary result using the generic element; we’ll refer to this as \((\clubsuit)\) below:

Now here is the full derivation:

One can now derive a number of properties of function composition:

• associativity, i.e. \[\begin{prooftree} \AxiomC{$\Gamma \vdash f:A \to B$} \AxiomC{$\Gamma \vdash g:B \to C$} \AxiomC{$\Gamma \vdash h:C \to D$} \TrinaryInfC{$\Gamma \vdash (h \circ g) \circ f \doteq h \circ (g \circ f):A \to D$} \end{prooftree}\]
• left and right unit laws \[\begin{prooftree} \AxiomC{$\Gamma \vdash f : A \to B$} \UnaryInfC{$\Gamma \vdash \operatorname{id}_B \circ f \doteq f : A \to B$} \end{prooftree}\] \[\begin{prooftree} \AxiomC{$\Gamma \vdash f : A \to B$} \UnaryInfC{$\Gamma \vdash f \circ \operatorname{id}_A \doteq f : A \to B$} \end{prooftree}\]

Bibliography