Inductive Types

In type theory, a system has inductive types if it has facilities for creating a new type from constants and functions that create terms of that type. —— Wikipedia

eg.

data Bool: Type where
  true false: Bool

Examples

bool

$$ bool\text{-}form: \require{bussproofs} \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash bool\ type$} \end{prooftree} $$

$$ bool\text{-}intro: \require{bussproofs} \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash true:bool$} \end{prooftree} \ \ \ \ \require{bussproofs} \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash false:bool$} \end{prooftree} $$

$$ bool\text{-}elim: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma,x:bool \vdash D(x)\ type$} \AxiomC{$\Gamma \vdash a: D(true)$} \AxiomC{$\Gamma \vdash a: D(false)$} \TrinaryInfC{$\Gamma,x:bool \vdash ind_{bool}(a,b,x):D(x)$} \end{prooftree} $$

$$ bool\text{-}comp: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma,x:bool \vdash D(x)\ type$} \AxiomC{$\Gamma \vdash a: D(true)$} \AxiomC{$\Gamma \vdash a: D(false)$} \TrinaryInfC{$\displaylines {\Gamma \vdash ind_{bool}(a,b,true) \doteq a:D(true)\\ \Gamma \vdash ind_{bool}(a,b,false) \doteq b:D(false)}$} \end{prooftree} $$

Coproduct

$$ +\text{-}form: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma \vdash P\ type$} \AxiomC{$\Gamma \vdash Q\ type$} \BinaryInfC{$\Gamma \vdash P+Q\ type$} \end{prooftree} $$

$$ +\text{-}intro: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma \vdash p:P$} \UnaryInfC{$\Gamma \vdash inl(p):P+Q$} \end{prooftree} \ \ \ \ \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma \vdash q:Q$} \UnaryInfC{$\Gamma \vdash inr(q):P+Q$} \end{prooftree} $$

$$ +\text{-}elim: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma,x:P+Q \vdash D(x)\ type$} \AxiomC{$\Gamma \vdash a: D(inl(p))$} \AxiomC{$\Gamma \vdash b: D(inr(q))$} \TrinaryInfC{$\Gamma,x:P+Q \vdash ind_+(a,b,x):D(x)$} \end{prooftree} $$

$$ +\text{-}comp: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma,x:P+Q \vdash D(x)\ type$} \AxiomC{$\Gamma \vdash a: D(inl(p))$} \AxiomC{$\Gamma \vdash b: D(inr(q))$} \TrinaryInfC{$\displaylines {\Gamma \vdash ind_+(a,b,inl(p)) \doteq a:D(inl(p))\\ \Gamma \vdash ind_+(a,b,inr(q)) \doteq b:D(inr(q))}$} \end{prooftree} $$

Proving example

Prove: For any types A,B,C, there's a function $A\times B + A\times C \rightarrow A \times (B+C)$.

We start from writing what we want to prove down:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{} \UnaryInfC{$\vdash\ \ ?:A\times B + A\times C \rightarrow A \times (B+C)$} \end{prooftree} $$

When we want to construct a term which is of type $P\rightarrow Q$, the most natural way is to use the $\rightarrow-intro$ rule, ie. assume there exists a term which is of type $A\times B + A\times C$.

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$x:A\times B + A\times C \vdash\ ?\ : A \times (B+C)$} \UnaryInfC{$\Gamma\ \ ?:A\times B + A\times C \rightarrow A \times (B+C)$} \end{prooftree} $$

Now on the left side of $\vdash$, we have a term in the form of $P + Q$, which leads us to use $+-elim$.

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$x_1: A\times B \vdash\ ?\ : A \times (B+C)$} \AxiomC{$x_2: A\times C \vdash\ ?\ : A \times (B+C)$} \BinaryInfC{$x:A\times B + A\times C \vdash\ ?\ : A \times (B+C)$} \UnaryInfC{$\Gamma\ \ ?:A\times B + A\times C \rightarrow A \times (B+C)$} \end{prooftree} $$

Let's take the left one for example, to construct a term in type $A \times (B+C)$, we can just use pairing to construct a term in type $P\times Q$.

So now we just need to construct a term like $(p, q): (A, B+C)$, note $()$s here means pair.

For the first element of the pair, which type is A, we just need to take the first element of the pair $x_1$, ie $pr_1x_1$.

And for the second element, which type is B+C, we should use the $+-intro$ rule and put the second element of the pair $x_2$ in with $inl$.

And this is what we got:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$x_1: A\times B \vdash(pr_1x_1, inl(pr_2x_1)): A \times (B+C)$} \AxiomC{$x_2: A\times C \vdash\ ?\ : A \times (B+C)$} \BinaryInfC{$x:A\times B + A\times C \vdash\ ?\ : A \times (B+C)$} \UnaryInfC{$\Gamma\ \ ?:A\times B + A\times C \rightarrow A \times (B+C)$} \end{prooftree} $$

The similar technique can be used on the right side:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$x_1: A\times B \vdash(pr_1x_1, inl(pr_2x_1)): A \times (B+C)$} \AxiomC{$x_2: A\times C \vdash(pr_1x_2, inr(pr_2x_2)): A \times (B+C)$} \BinaryInfC{$x:A\times B + A\times C \vdash\ ?\ : A \times (B+C)$} \UnaryInfC{$\Gamma\ \ ?:A\times B + A\times C \rightarrow A \times (B+C)$} \end{prooftree} $$

Then fill the hole we left when applying $+-elim$:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$x_1: A\times B \vdash(pr_1x_1, inl(pr_2x_1)): A \times (B+C)$} \AxiomC{$x_2: A\times C \vdash(pr_1x_2, inr(pr_2x_2)): A \times (B+C)$} \BinaryInfC{$x:A\times B + A\times C \vdash ind_+((pr_1x_1, inl(pr_2x_1)), (pr_1x_2, inr(pr_2x_2)), x) : A \times (B+C)$} \UnaryInfC{$\Gamma\ \ ?:A\times B + A\times C \rightarrow A \times (B+C)$} \end{prooftree} $$

Now fill the last hole by introducing a $λ$ and we are done:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$x_1: A\times B \vdash(pr_1x_1, inl(pr_2x_1)): A \times (B+C)$} \AxiomC{$x_2: A\times C \vdash(pr_1x_2, inr(pr_2x_2)): A \times (B+C)$} \BinaryInfC{$x:A\times B + A\times C \vdash ind_+((pr_1x_1, inl(pr_2x_1)), (pr_1x_2, inr(pr_2x_2)), x) : A \times (B+C)$} \UnaryInfC{$\vdash\ \lambda\ x. ind_+((pr_1x_1, inl(pr_2x_1)), (pr_1x_2, inr(pr_2x_2)), x): A\times B + A\times C \rightarrow A \times (B+C)$} \end{prooftree} $$

In agda:

open import Data.Product
open import Data.Sum renaming (__ to _+_)

t :  (A B C : Set) → A × B + A × C A × (B + C)
t A B C (inj₁ (fst , snd)) = fst , injsnd
t A B C (inj₂ (fst , snd)) = fst , injsnd

Dependent Pair Type (Σ type)

In computer science, a tagged union, also called a variant, variant record, choice type, discriminated union, disjoint union, sum type or coproduct, is a data structure used to hold a value that could take on several different, but fixed, types. —— Wikipedia

$$ \Sigma-form: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma, x: P \vdash Q(x)$} \UnaryInfC{$\Gamma \vdash \Sigma_{(x:P)} Q(x)$} \end{prooftree} $$

$$ \Sigma-intro: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma \vdash p:P$} \AxiomC{$\Gamma \vdash q:Q(p)$} \BinaryInfC{$\Gamma \vdash pair(p, q):\Sigma_{(x:P)} Q(x)$} \end{prooftree} $$

$$ \Sigma-elim: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma,z:\Sigma_{(x:P)} Q(x) \vdash D(z)\ type$} \AxiomC{$\Gamma,x:P,y:Q(x) \vdash a: D(pair(x,y))$} \BinaryInfC{$\Gamma,z:\Sigma_{(x:P)} \vdash ind_{\Sigma}(a,z):D(z)$} \end{prooftree} $$

$$ \Sigma-comp: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma,z:\Sigma_{(x:P)} Q(x) \vdash D(z)\ type$} \AxiomC{$\Gamma,x:P,y:Q(x) \vdash a: D(pair(x,y))$} \BinaryInfC{$\Gamma,x:P,y:Q(x) \vdash ind_{\Sigma} (a, pair(x,y)) \doteq a:D(pair(x,y))$} \end{prooftree} $$

How to view Σ type

Assume there's a set named as P and a predicate named as Q, then $\Sigma_{(x:P)}Q(x)$ means there exists an element $x$ in $P$ such that $Q(x)$ holds, ie. we can regard Σ in types as ∃ in logic.

Proving example

Prove: for any $x:P\vdash Q(x)\ type$, there exists a projection function $\pi : \Sigma_{(x:P)} Q(x) \rightarrow P$.

By using $\rightarrow-intro$ and $\Sigma-elim$, we can prove it like this:

$$ \require{bussproofs} \begin{prooftree} \AxiomC{$x:P,y:Q(x) \vdash x:P$} \UnaryInfC{$z:\Sigma_{(x:P)}Q(x)\vdash ind_{\Sigma}(x,z):P$} \UnaryInfC{$\vdash \lambda z.ind_{\Sigma}(x,z):\Sigma_{(x:P)}Q(x)\rightarrow P$} \end{prooftree} $$

In agda:

π :  (A : Set) (B : A Set) → Σ A B A
π A B (fst , snd) = fst

Natural Numbers

$$ \mathbb N-form: \require{bussproofs} \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash \mathbb N\ type$} \end{prooftree} $$

$$ \mathbb N-intro: \require{bussproofs} \begin{prooftree} \AxiomC{} \UnaryInfC{$\Gamma \vdash 0:\mathbb N$} \end{prooftree} \ \ \ \ \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma \vdash n:\mathbb N$} \UnaryInfC{$\Gamma \vdash succ(n):\mathbb N$} \end{prooftree} $$

$$ \mathbb N-elim: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma,x:\mathbb N \vdash D(x)\ type$} \AxiomC{$\Gamma \vdash a:D(0)$} \AxiomC{$\Gamma,x:\mathbb N,y:D(x) \vdash b: D(succ(x))$} \TrinaryInfC{$\Gamma,x:\mathbb N \vdash ind_{\mathbb N}(a,b,x):D(x)$} \end{prooftree} $$

$$ \mathbb N-comp: \require{bussproofs} \begin{prooftree} \AxiomC{$\Gamma,x:\mathbb N \vdash D(x)\ type$} \AxiomC{$\Gamma \vdash a:D(0)$} \AxiomC{$\Gamma,x:\mathbb N,y:D(x) \vdash b: D(succ(x))$} \TrinaryInfC{$\displaylines {\Gamma \vdash ind_{\mathbb N}(a,b,0) \doteq a:D(0)\\ \Gamma,x:\mathbb N \vdash ind_{\mathbb N}(a,b,succ(x)) \doteq b[ind_{\mathbb N}(a,b,x)/y]:D(succ(x))}$} \end{prooftree} $$

Materials

Lecture Note

HoTTEST_Lecture_2.pdf

Record on Youtube

1

It's actually judgmentally equal, ref.