# What is induction-induction?

What is induction-induction?

The resources I found are:

The first two references are too brief for me, and the latter two are too technical. Can anyone explain it in layman's term? It would be better if there's Agda code.

• There's Agda code in your fourth citation. Oct 2 '16 at 18:45
• Sure, but it would be super hard to read through that huge amount of code. And (I guess) super easy just by seeing 1 or 2 examples.
– 盛安安
Oct 2 '16 at 18:49

Supplemental 2016-10-03: I mixed up induction-induction and induction-recursion (not the first time I did that!). My apologies for the mess. I updated the answer to cover both.

I find the explanations in the Forsberg & Setzer's paper A finite axiomatisation of inductive-inductive definitions illuminating.

### Induction-recursion

An inductive-recursive definition is one in which we define a type $$A$$ and a type family $$B : A \to \mathsf{Type}$$ simultaneously in a special way:

1. $$A$$ is defined as an inductive type.
2. $$B$$ is defined by recursion on $$A$$.
3. Crucially, the definition of $$A$$ may use $$B$$.

Without the third requirement, we could first define $$A$$ and then separately $$B$$.

Here is a baby example. Define $$A$$ inductively to have the following constructors:

• $$a : A$$
• $$\ell : \big(\sum_{x : A} B(x)\big) \to A$$

The type family $$B$$ is defined by

• $$B(a) = \mathtt{bool}$$
• $$B(\ell(x, f)) = \mathtt{nat}$$.

So, what is in $$A$$? First of all we have an element $$a : A.$$ Because of that, there is a type $$B(a)$$ which is defined to be $$\mathtt{bool}$$. Therefore, we can form two new elements $$\ell(a, \mathtt{false})$$ and $$\ell(a, \mathtt{true})$$ in $$A$$. Now we have $$B(\ell(a, \mathtt{false})) = B(\ell(a, \mathtt{true})) = \mathtt{nat}$$, so we can also form for every $$n : \mathtt{nat}$$ the elements $$\ell(\ell(a, \mathtt{false}), n) : A$$ and $$\ell(\ell(a, \mathtt{true}), n) : A$$ We can keep going like this. The next stage will be that since $$B(\ell(\ell(a, \mathtt{true}), n)) = \mathtt{nat}$$ there is for every $$m : \mathtt{nat}$$ the element $$\ell(\ell(\ell(a, \mathtt{true}), n), m) : A$$ and the element $$\ell(\ell(\ell(a, \mathtt{false}), n), m) : A$$ We can keep going. A little bit of thinking reveals that $$A$$ is more or less two copies of lists of natural numbers, sharing a common empty list. I will leave it as an exercise to figure out why.

### Induction-induction

An inductive-inductive definition also defines a type $$A$$ and simultaneously a type family $$B : A \to \mathsf{Type}$$:

1. $$A$$ is defined inductively
2. $$B$$ is defined inductively, and it may refer to $$A$$
3. Crucially, $$A$$ may refer to $$B$$.

It is important to understand the difference between induction-recursion and induction-induction. In induction-recursion we define $$B$$ by providing equations of the form $$B(\mathsf{c}(\ldots)) = \cdots$$ where $$\mathsf{c}(\ldots)$$ is a constructor for $$A$$. In an inductive-inductive definition we define $$B$$ by providing constructors for forming the elements of $$B$$.

Let us reformulate our previous example as induction-induction. First we have the inductively given tpye $$A$$:

• $$a : A$$
• $$\ell : \big(\sum_{x : A} B(x)\big) \to A$$

The type family $$B$$ is defined by the following constructors:

• $$\mathsf{Tru} : B(a)$$
• $$\mathsf{Fal} : B(a)$$
• if $$x : A$$ and $$y : B(x)$$ then $$\mathsf{Zer} : B(\ell(x,y))$$
• if $$x : A$$ and $$y : B(x)$$ and $$z : B(\ell(x,y))$$ then $$\mathsf{Suc}(z) : B(\ell(x,y))$$.

As you can see, we gave rules for generating the elements of $$B$$ which amount to saying that $$B(a)$$ is (isomoprhic to) the booleans, and $$B(\ell(x,y))$$ is (isomorphic to) the natural numbers.

• why the hell would someone define such data types D:
– 盛安安
Oct 2 '16 at 19:52
• In order to teach what an inductive-inductive type is. I could give you a real example, namely a type universe, but that would be confusing. Oct 2 '16 at 21:04
• @AndrejBauer This looks more like induction-recursion to me. Induction-induction is when the type family is defined as an inductive type. Oct 3 '16 at 10:24
• Oops, you're absolutely right. I'll fix it. Oct 3 '16 at 14:30
• Is the domain of $\ell$ supposed to be a Sigma type instead of a Pi type? Jan 8 '20 at 20:15