Contents

# Contents

## Idea

In type theory, induction-recursion is a principle for mutually defining types of the form

$A \; \mathrm{type} \qquad a:A \vdash B(a) \; \mathrm{type}$

where $A$ is defined as an inductive type and $B$ is defined by recursion on $A$. Crucially, the definition of $A$ may use $B$. Without this last requirement, we could first define $A$ and then separately $B$.

In type theory, higher induction-reduction is the principle that one could also have identity constructors and identity section constructors in addition to the element and section constructors.

## Example

A Tarski universe is an example of an inductive-recursive definition, where a type $U$ is defined inductively together with a type family $a:U \vdash T(a) \; \mathrm{type}$. The constructors for $U$ may depend negatively on $T$ applied to elements of $U$. This is the case if $U$, for example, is closed under dependent product types, where it has constructors of

• a dependent type $\Pi(a, b):U$ for each $a:U$ and $b:T(a) \to U$,
• a function $E_\Pi(a, b):\left(\prod_{x:T(a)} T(b(x))\right) \to T(\Pi(a, b))$ for each $a:U$ and $b:T(a) \to U$.

If the Tarski universe is strictly closed under dependent product types, then the last condition is replaced by

• a judgmental equality $T(\Pi(a, b)) \equiv \prod_{x:T(a)} T(b(x))$ for each $a:U$ and $b:T(a) \to U$.

Here, the type family $T$ is defined recursively. Sometimes, however, one might not want to give $T(u)$ completely as soon as $u:U$ is introduced, but instead define $T$ inductively as well. This is the principle of induction-induction.

### History of inductive types

Historical references on the definition of inductive types.

#### Precursors

A first type theoretic formulation of general inductive definitions:

• Per Martin-Löf, Hauptsatz for the Intuitionistic Theory of Iterated Inductive Definitions, Studies in Logic and the Foundations of Mathematics 63 (1971) 179-216 $[$doi:10.1016/S0049-237X(08)70847-4$]$

The induction principle for identity types (also known as “path induction” or the “J-rule”) is first stated in:

• Per Martin-Löf, §1.7 and p. 94 of: An intuitionistic theory of types: predicative part, in: H. E. Rose, J. C. Shepherdson (eds.), Logic Colloquium ‘73, Proceedings of the Logic Colloquium, Studies in Logic and the Foundations of Mathematics 80 (1975) 73-118 (doi:10.1016/S0049-237X(08)71945-1, CiteSeer)

and in the modern form of inference rules in:

• Bengt Nordström, Kent Petersson, Jan M. Smith, §8.1 of: Programming in Martin-Löf’s Type Theory, Oxford University Press (1990) $[$webpage, pdf, pdf$]$

The special case of inductive types now known as $\mathcal{W}$-types is first formulated in:

• Per Martin-Löf, pp. 171 of: Constructive Mathematics and Computer Programming, in: Proceedings of the Sixth International Congress of Logic, Methodology and Philosophy of Science (1979), Studies in Logic and the Foundations of Mathematics 104 (1982) 153-175 $[$doi:10.1016/S0049-237X(09)70189-2, ISBN:978-0-444-85423-0$]$

• Per Martin-Löf (notes by Giovanni Sambin), Intuitionistic type theory, Lecture notes Padua 1984, Bibliopolis, Napoli (1984) $[$pdf, pdf$]$

Early proposals for a general formal definition of inductive types:

#### Modern definition

The modern notion of inductive types and inductive families in intensional type theory is independently due to

and due to

which became the basis of the calculus of inductive constructions used in the Coq-proof assistant:

• Frank Pfenning, Christine Paulin-Mohring, Inductively defined types in the Calculus of Constructions, in: Mathematical Foundations of Programming Semantics MFPS 1989, Lecture Notes in Computer Science 442, Springer (1990) $[$doi:10.1007/BFb0040259$]$

• Christine Paulin-Mohring, Inductive definitions in the system Coq – Rules and Properties, in: Typed Lambda Calculi and Applications TLCA 1993, Lecture Notes in Computer Science 664 Springer (1993) $[$doi:10.1007/BFb0037116$]$

reviewed in

• Zhaohui Luo, §9.2.2 in: Computation and Reasoning – A Type Theory for Computer Science, Clarendon Press (1994) $[$ISBN:9780198538356, pdf$]$

• Christine Paulin-Mohring, §2.2. in: Introduction to the Calculus of Inductive Constructions, contribution to: Vienna Summer of Logic (2014) $[$hal:01094195, pdf, pdf slides$]$

with streamlined exposition in:

The generalization to inductive-recursive types is due to

• Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, The Journal of Symbolic Logic 65 2 (2000) 525-549 $[$doi:10.2307/2586554, pdf$]$

• Peter Dybjer, Anton Setzer, Indexed induction-recursion, in Proof Theory in Computer Science PTCS 2001. Lecture Notes in Computer Science2183 Springer (2001) $[$doi:10.1007/3-540-45504-3_7, pdf$]$