# Example use cases for induction-recursion

I know of only two uses of induction-recursion:

1. Encoding universes as a type, as shown in the Agda docs for recursion
2. Encoding Finite sets as shown in Conor Mc'Bride's "datatypes of datatypes", Chapter 6, Induction-Recursion. I don't understand the point of this example, so I feel like I'm missing something.

I'd like answers to be examples of where induction-recursion is used. To quote Halmos:

A good stack of examples, as large as possible, is indispensable for a thorough understanding of any concept,and when I want to learn something new, I make it my first job to build one.

Here is one article that discussed induction-recursion. Here's their code:

  data Lang : Set
⟦_⟧ : Lang → Set

data Lang where
Zero One Two : Lang
Pair Fun Tree : (A : Lang) (B : ⟦ A ⟧ → Lang) → Lang

⟦ Zero ⟧ = ⊥
⟦ One ⟧ = ⊤
⟦ Two ⟧ = Bool
⟦ Pair A B ⟧ = Σ ⟦ A ⟧ λ a → ⟦ B a ⟧
⟦ Fun A B ⟧ = (a : ⟦ A ⟧) → ⟦ B a ⟧
⟦ Tree A B ⟧ = W ⟦ A ⟧ λ a → ⟦ B a ⟧


There is a related feature in Agda called interleaved mutual definition which is an even stronger variant of induction-recursion. You can look at their examples.

Here is one indirect example (which is actually induction-induction): the definition of a dependent type theory. The definitions of context, type, and term are mutually recursive as terms are only defined in a context (so the definition of term requires context), while context contains types, and in a dependent type systems types are just terms. So here we have an inductive-inductive definition if term and context are defined as inductive types. This is similar to induction-recursion to some extent.