notes-formal-02.md

---

title: |
  Overview on Formalization - Type Theory part 2
date: 2024-04-08

---

\newcommand{\type}{\ \text{type}} \newcommand{\id}{\operatorname{id}} \newcommand{\prd}[1]{\Pi_{(#1)}} \newcommand{\comp}{\operatorname{comp}}

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:

ParseError: KaTeX parse error: Undefined control sequence: \type at position 34: …Gamma \vdash A \̲t̲y̲p̲e̲}{\Gamma,x':A \…

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

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

Also need the congruence rule:

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

$\Pi$-introduction rule

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

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

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:

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

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

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

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

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

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

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

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

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

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:

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

And here is the formal declaration of the "new notation":

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

Construction of the identity function

Given a type $A$ in context $\Gamma$, let's construct the identity function ParseError: KaTeX parse error: Undefined control sequence: \id at position 1: \̲i̲d̲ ̲= \id_A:A \to A using the generic term:

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Gamm…

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 ParseError: KaTeX parse error: Undefined control sequence: \comp at position 1: \̲c̲o̲m̲p̲(g,f) for $g \circ f$. Then ParseError: KaTeX parse error: Undefined control sequence: \comp at position 1: \̲c̲o̲m̲p̲ 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 ParseError: KaTeX parse error: Undefined control sequence: \comp at position 1: \̲c̲o̲m̲p̲ is $$(B \to C) \to ((A \to B) \to (A \to C))$$ Thus for $g:B \to C$, we have ParseError: KaTeX parse error: Undefined control sequence: \comp at position 1: \̲c̲o̲m̲p̲(g):(A \to B) \…

We are going to define ParseError: KaTeX parse error: Undefined control sequence: \comp at position 1: \̲c̲o̲m̲p̲ by the rule ParseError: KaTeX parse error: Undefined control sequence: \comp at position 1: \̲c̲o̲m̲p̲ ̲= \lambda g.\la….

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

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

Now here is the full derivation:

ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

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

• associativity, i.e. ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

• left and right unit laws ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\Ga…

  ParseError: KaTeX parse error: No such environment: prooftree at position 7: \begin{̲p̲r̲o̲o̲f̲t̲r̲e̲e̲}̲ \AxiomC{$\…

Bibliography

::: {.refs} :::