I know of only two uses of induction-recursion:
- Encoding universes as a type, as shown in the Agda docs for recursion
- 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.