Within the context of dependent type theory, inductive-recursive types are types in which
are mutually defined at the same time.
One of the key motivating examples of inductive-recursive types are inductive-recursive universes.
It is well-known that type-theoretic universes do not come with an elimination rule. Such a construct would allow us to pattern-match on elements of the universe. For example, given a code for a dependent type, we could extract the component .
There are at the very least two reasons we might want to avoid that:
However, there are cases where we would like a "universe" of sorts, which is limited, closed, and on which we can pattern-match. We can define such a universe by induction-recursion.
Quoting from Shulman's blog post (link below), we can define a "universe" as well as a function from to the "real" universe in "fake Agda" notation as follows:
mutual
data U : Type where
sig : (A : U) → (El A → U) → U
pi : (A : U) → (El A → U) → U
El : U → Type
El (sig A B) = Σ (El A) (λ a → El (B a))
El (pi A B) = Π (El A) (λ a → El (B a))
This way, we define both a "closed" universe U, as well as a function El : U → Type that interprets every element of U as an actual type in our ambient type theory.
For example, to construct the code of a -type in U, we must not only give the code A : U of its domain, but also a family B : El A → U of codes, which is indexed in _the interpretation El A of A as a type.
Thus, we obtain both a "universe U on which we can pattern-match, as well as an interpretation El of its elements as actual, honest types.
Dybjer, Peter, and Anton Setzer. 1999. ‘A Finite Axiomatization of Inductive-Recursive Definitions’. In Typed Lambda Calculi and Applications, edited by Jean-Yves Girard, 1581:129–46. Lecture Notes in Computer Science. Springer Berlin Heidelberg. https://doi.org/10.1007/3-540-48959-2_11.
@inproceedings{dybjer_1999,
series = {Lecture {Notes} in {Computer} {Science}},
title = {A {Finite} {Axiomatization} of {Inductive}-{Recursive} {Definitions}},
volume = {1581},
doi = {10.1007/3-540-48959-2_11},
booktitle = {Typed {Lambda} {Calculi} and {Applications}},
publisher = {Springer Berlin Heidelberg},
author = {Dybjer, Peter and Setzer, Anton},
editor = {Girard, Jean-Yves},
year = {1999},
pages = {129--146}
}