Example use cases for induction-recursion

Question

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.

Answer 1

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.