202506161406

Tags : Homotopy Type Theory

Inductive Types

---

An inductive type is meant to be a type that is freely generated by a finite collection of functions (which can have 0 inputs) whose codomain is the type. For example

• The Unit Type is generated by a single constructor $\star$.
• The Product Type $A\times B$ is generated by the constructor $(-,-):A\to B\to A\times B$.
• The type of Natural Numbers is created by 2 constructors
  • $0$, which is a value
  • $\text{suc}:\mathbb{N}\to \mathbb{N}$

And so on.

Note

The constructors are allowed to have the inductive type as their domain.

Another such type is $[A]$, which can be defined as

$$\begin{array}{rl}\square & :[A]\\ (-::-)& :A\to [A]\to [A]\end{array}$$

These inductive types are meant to be Freely generated and that is expressed using their elimination rule, or the induction principle.

Example

For example the induction principle for the type $2$:

• When proving a statement $E:2\to \mathcal{U}$, it suffices to prove it for $0$ and $1$.

Thus there is a function ${\text{ind}}_2$, that takes a type family $E:2\to \mathcal{U}$, then $e_0:E(0)$ then $e_1:E(1)$, then we get ${\text{ind}}_2(E,e_0,e_1):{\prod }_{x:2}E(x)$ such that:

$$\begin{array}{r}{\text{ind}}_2(E,e_0,e_1,0):\equiv e_0\\ {\text{ind}}_2(E,e_0,e_1,1):\equiv e_1\end{array}$$

We usually call this case analysis.

---

References

• Similar description of inductive types lead to equal types
• Uniqueness of functions created using induction principle
• Product Type
• Natural Numbers in Type Theory
• Boolean Type
• Sum Types