Skip to main content

Induction-recursion allows mutual definition of an inductive type and a recursive function. Induction-recursion is primarily used to inductively define large universes predicatively, thus significantly increasing proof strength of the base theory beyond W-types.

References:

A general formulation of induction-recursion: P. Dybjer: A General Formulation of Simultaneous Inductive-Recursive Definitions in Type Theory

Study towards optimal axiomatizations of induction-recursion: Ghani et al.: Variations on Inductive-Recursive Definitions