## 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-form: \require{bussproofs} \begin{prooftree} \AxiomC{} \UnaryInfC{\Gamma \vdash bool\ type} \end{prooftree}$$

$$bool-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-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-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

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

$$+-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}$$

$$+-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}$$

$$+-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 , inj₁ snd
t A B C (inj₂ (fst , snd)) = fst , inj₂ snd


#### 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.