Inductive Types

These notes are based on Kevin Buzzard’s excellent notes and Chapter 7 of the theorem proving book.

What happens when we define an inductive type?#

inductive X: Type
| p : X 

When proving theorems from a set theory perspective, the above code is can be (most of the time I’m told) interpreted as: we have defined a set $X = \{p\}$ with one element. In the language of type theory, I think the proper phrasing is we created a new type X with one term X.p.

Another thing that happens when we write above code excerpt is that Lean automatically under the hood defines something like called the recursor.

@X.rec : {motive : X → Sort u_1} → motive X.p → (t : X) → motive t

The goal of this post is to somewhat demystify this recursor. Kevin Buzzard’s post already does this, but I often find it helpful to re-write things in my own words to enhance my own understanding. So there’s a high probability that this post just poorly re-expresses what the linked articles already do.

I believe in earlier versions of Lean motive was called C. We will use C from henceforth as it is shorter to write. Quoting Kevins post, what X.rec is saying is that

In my words, as Lean is based on “dependent” type theory, the co-domain of a function from $X$ to some other set could depend on the input value $x \in X$. This is why we have this set $C$ parameterised by $x$, but for the purpose of intuition let’s bin this and say, we want to define a function $f: X \to S$ i.e. no matter what the input $x : X$ is the co-domain is always the set $S$.

So we are given

• a set $S$
• some element $a \in S$ and
• any $t \in X$.

and because we possess the recursor, X.rec, we can use it to get an element of $C(p)$