Type (Type Theory)

Definition

To specify a type, we need:

• Formation rule
• Constructors (introduction rules)
• Eliminators (elimination rules)
• Computation rule (β-reduction)
• optional uniqueness principle (η-expansion)

Formation rule

A formation rule tells you when a type is well-formed, $i$.$e$. when you are allowed to form a new type expression.

Constructors

how to construct elements of that type

Eliminators

An eliminator is the canonical principle for using (eliminating) values of a type

The eliminator states the elimination principle by giving a term with a specific type

$i$.$e$. defining functions out of that type by analyzing how the value could have been constructed.

There are two common forms:

Non-dependent eliminator (recursor)

it defines a function into a constant target type.

Comment

What a bad name!, a recursor is not recursive

defines a plain function:

$$f:T\to C$$

where $C$ does not depend on the input

Dependent eliminator (induction)

Defines a dependent function (Π-types (Dependent function types)):

$$f:{\Pi }_{(x:T)}C(x)$$

where type $C(x)$ depend on $x$.

Computation rule

how an eliminator acts on a constructor

The computation rule (β-rule) states how that recursor reduces/evaluates when you apply it to a constructor.

Examples

Example: Product type A×B

Formation rule: If $A:\mathcal{U}$ and $B:\mathcal{U}$, then

$$A\times B:\mathcal{U}$$

Constructor: If $a:A$ and $b:B$, then

$$(a,b):A\times B$$

or the constructor is pairing: $(\cdot ,\cdot ):A\to B\to A\times B$

Eliminator (recursor):

$$re{c}_{A\times B}:\prod _{C:\mathcal{U}}(A\to B\to C)\to (A\times B\to C)$$

Meaning: we choose a result type $C$ we give a rule $g:A\to B\to C$ telling how to produce a $C$ from components $a:A$ and $b:B$, then ${\text{rec}}_{A\times B}(C,g)$ is the function $f:A\times B\to C$

Computation rule (β):

$$re{c}_{A\times B}(C,g,(a,b))\equiv g(a)(b)$$

We can define special cases:

• ${\text{pr}}_1:A\times B\to A$ with computation rule ${\text{pr}}_1(a,b)\equiv a$
• ${\text{pr}}_2:A\times B\to A$ with computation rule ${\text{pr}}_2(a,b)\equiv b$

Uniqueness: $\forall x:A\times B,x=({\text{pr}}_1(x),{\text{pr}}_2(x))$

NOTE

actually we could define $A\times B:\equiv {\prod }_{x:2}{\text{rec}}_2(\mathcal{U},A,B,x)$ Note that $A\times B$ could be constructed as an indexed one over the two-element type 2

Example: Coproduct type A+B

Formation rule: If $A:\mathcal{U}$ and $B:\mathcal{U}$, then

$$A+B:\mathcal{U}$$

Constructors:

$$inl:A\to A+B$$ $$inr:B\to A+B$$

Eliminator (recursor):

$$re{c}_{A+B}:\prod _{C:\mathcal{U}}(A\to C)\to (B\to C)\to (A+B\to C)$$

Computation rules (β):

$$re{c}_{A+B}(C,f,g,inl(a))\equiv f(a)$$ $$re{c}_{A+B}(C,f,g,inr(b))\equiv g(b)$$

NOTE

actually we could define $A+B:\equiv {\sum }_{x:2}{\text{rec}}_2(\mathcal{U},A,B,x)$ Note that $A+B$ could be constructed as an indexed one over the two-element type 2

Example: Unit type 1

Formation rule: $1:\mathcal{U}$

Constructor (introduction rule): $\star :1$

Eliminator (recursor):

$$re{c}_1:\prod _{C:\mathcal{U}}C\to (1\to C)$$

Induction: ${\text{ind}}_1:{\Pi }_{C:1\to \mathcal{U}}C(\star )\to {\Pi }_{x:1}C(x)$ This means, if you have a family $C:1\to \mathcal{U}$, to produce $f:{\Pi }_{x:1}C(x)$ it suffices to give $c:C(\star )$ ${\text{ind}}_1:(C,c,\star ):\equiv c$

Computation rule (β-rule):

$$re{c}_1(C,c,\star )\equiv c$$

prove the propositional uniqueness principle for 1

Step 1: Define family $C:1\to \mathcal{U}$ by $C(x):\equiv (x=\star )$ so a term of ${\prod }_{x:1}C(x)$ is exactly a term of ${\prod }_{x:1}(x=\star )$

Step 2: Induction for the unit type says: ${\text{ind}}_1:{\Pi }_{C:1\to \mathcal{U}}C(\star )\to {\Pi }_{x:1}C(x)$ so it suffices to give a term of $C(\star )$

Step 3: base case Compute: $C(\star )\equiv (\star =\star )$ and we always have ${\text{refl}}_{\star }:\star =\star$

Step 4: we define $\text{upun}:\equiv {\text{ind}}_1(\lambda x.x=\star ,{\text{refl}}_{\star })$

check:

• for any $x:1$, $\text{upun}(x):x=\star$
• by computation rule $\text{upun}(\star )\equiv {\text{refl}}_{\star }$

Example: Empty type 0

Formation rule: $0:\mathcal{U}$

Constructor: (none)

Eliminator (recursor / ex falso):

$$re{c}_0:\prod _{C:\mathcal{U}}0\to C$$

Computation rule: (none)

Example: Natural numbers N

Formation rule:

$$\mathbb{N}:U$$

Constructors:

$$0:\mathbb{N}$$ $$succ:\mathbb{N}\to \mathbb{N}$$

Eliminator (recursor / primitive recursion):

$$re{c}_{\mathbb{N}}:\prod _{C:U}C\to (\mathbb{N}\to C\to C)\to (\mathbb{N}\to C)$$

Computation rules (β):

$$re{c}_{\mathbb{N}}(C,c_0,c_s,0)\equiv c_0$$ $$re{c}_{\mathbb{N}}(C,c_0,c_s,succ(n))\equiv c_s(n,re{c}_{\mathbb{N}}(C,c_0,c_s,n))$$

Example: Lists List(A)

Formation rule: If $A:U$, then

$$List(A):U$$

Constructors:

$$nil:List(A)$$ $$cons:A\to List(A)\to List(A)$$

Eliminator (recursor / fold):

$$re{c}_{List(A)}:\prod _{C:U}C\to (A\to List(A)\to C\to C)\to (List(A)\to C)$$

Computation rules (β):

$$rec(\_,c_{nil},c_{cons},nil)\equiv c_{nil}$$ $$rec(\_,c_{nil},c_{cons},cons(a,\ell ))\equiv c_{cons}(a,\ell ,rec(\_,c_{nil},c_{cons},\ell ))$$

Other examples

Similarly we can also define types like $A\to B$, ${\prod }_{(a:A)}B(a)$ or ${\sum }_{(a:A)}B(a)$

Propositions

We treat propositions as types and the evidence (proofs) as elements of this type.

$A\to B$ means: we can find a function such that it matches all elements of $A$ to elements of $B$. $⟹$ For every proof of $A$ we can find a proof of $B$. Case 1: if $A$ is true $⟹$ there is a proof of $A$ $⟹$ there is a proof of $B$ $⟹$ $B$ is true Case 2: if $A$ is false $⟹$ it is easy to define a function from $A$ to $B$, (any mapping would do the job, since the function is never called) $⟹$ $A\to B$ is true

We see $A\to B$ (type theory) and $A\to B$ (first order logic) are equivalent.