Inductive-recursive types

Within the context of dependent type theory, inductive-recursive types are types in which

• the inductive type itself, and
• a function inducting on that type

are mutually defined at the same time.

One of the key motivating examples of inductive-recursive types are inductive-recursive universes.

Inductive-recursive universe

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 \Pi(A, B) : \mathcal{U} for a dependent type, we could extract the component A : \mathcal{U}.

There are at the very least two reasons we might want to avoid that:

• We would prefer an "open" type theory, to which we may add further type formers in the future.
• It contradicts univalence. If \mathcal{U} is univalent, we can prove equivalences which equate a \Sigma-type with a \Pi-type, such as the type-theoretic axiom of choice. In that case, pattern-matching on \Pi and \Sigma-types, would allow one to violate equality.

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" \mathcal{U} as well as a function \textsf{El} : \mathcal{U} \to \textsf{Type} from \mathcal{U} to the "real" universe \textsf{Type} 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 \Pi-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.

References

• A finitary schema for inductive-recursive types was given in

@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}
}