notes-formal-03.md

---

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

---

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

Inductive Types

Here I mostly want to "explain a little via some examples", referring you to the text [@rijkeIntroductionHomotopyType] for more details and full definitions.

The main point to emphasize is that inductive types share some of the features of the $\Pi$-types -- i.e. types of (dependent or ordinary) functions.

Inductive types are specified by:

• constructors AKA introduction rules

• an induction principle AKA elimination rules

• computation rules

Natural numbers $\mathbf{N}$

• formation rule

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

• introduction rules (constructors)

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

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

• induction principle

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

List A

Let's describe the inductive type of Lists. More precisely, for a type $A$, let's describe the type whose elements are lists of elements of $A$.

• 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…

• introduction rules; ie. the constructors.

  There are two introduction rules for lists. The first one forms the empty list:

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

  The second one constructs ("cons") a list from a term of type $A$ and an existing ParseError: KaTeX parse error: Undefined control sequence: \List at position 1: \̲L̲i̲s̲t̲ ̲A.

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

• the induction principle or elimination rule

  We must stipulate what is needed to construct a section of a type family over the inductive type -- i.e. a dependent function.

  The idea is this: for our inductive type $A$, in order to define a dependent function ParseError: KaTeX parse error: Undefined control sequence: \prd at position 3: f:\̲p̲r̲d̲{x:A}B(x) one must specify the behavior of $f$ at the constructors of $A$.

  Here is our induction principle for ParseError: KaTeX parse error: Undefined control sequence: \List at position 1: \̲L̲i̲s̲t̲ ̲A:

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

(iii) The computation rules assert that the inductively defined section agrees on the constructors with the data that was used to define the section. Thus, there is a computation rule for every constructor

Bibliography

::: {.refs} :::