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.

  • $\begingroup$ There's Agda code in your fourth citation. $\endgroup$ Oct 2, 2016 at 18:45
  • $\begingroup$ 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. $\endgroup$
    – 盛安安
    Oct 2, 2016 at 18:49

1 Answer 1


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.


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.


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.

  • $\begingroup$ why the hell would someone define such data types D: $\endgroup$
    – 盛安安
    Oct 2, 2016 at 19:52
  • 7
    $\begingroup$ 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. $\endgroup$ Oct 2, 2016 at 21:04
  • 3
    $\begingroup$ @AndrejBauer This looks more like induction-recursion to me. Induction-induction is when the type family is defined as an inductive type. $\endgroup$
    – gallais
    Oct 3, 2016 at 10:24
  • 2
    $\begingroup$ Oops, you're absolutely right. I'll fix it. $\endgroup$ Oct 3, 2016 at 14:30
  • $\begingroup$ Is the domain of $\ell$ supposed to be a Sigma type instead of a Pi type? $\endgroup$ Jan 8, 2020 at 20:15

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.