Contents

# Contents

## Idea

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

$A \colon Type\,,\;\;\; and \;\;\; B \colon A \to Type \,,$

where both $A$ and $B$ are defined inductively, such that the constructors for $A$ can refer to $B$ and vice versa. In addition, the constructor for $B$ can refer to the constructor for $A$.

Such induction-induction occurs for instance when formalising dependent type theory in type theory.

## Results

Inductive-inductive types are related to inductive-recursive types. Importantly, inductive-inductive types have an initial algebra semantics with respect to dialgebras. In Forsberg’s thesis inductive-inductive types are reduced to indexed inductive types in the setting of extensional type theory. This reduction however only provides “simple” elimination rules (not to be confused with simply typed). Indexed inductive types in turn can be reduced to W-types in extensional type theory. See inductive families.

The consistency of the framework used for the elimination (e.g. in the theorem prover Agda) is not so clear, as it allows the definition of a universe containing a code for itself. There is an axiomatisation of the new principle in such a way that the resulting type theory is consistent, as proved by constructing a set-theoretic model; see Forsberg-Setzer 10.

Hugunin provides a reduction of an inductive-inductive type to an inductive type. This construction is conjectured to generalize to all inductive-inductive types. The construction is done in cubical type theory and hence is consistent with homotopy type theory.

## Higher inductive inductive types

Experiments with higher inductive inductive types (elaborate versions of higher inductive types) are sections 11.3 “Cauchy reals” and section 11.6 “Conway surreals” of the HoTT book. As they are at the set level, these are instances of quotient inductive-inductive types; see QIIT. An experimental syntax for HIITs by Kaposi and Kovacs.

## References

• Fredrik Nordvall Forsberg, Anton Setzer, A finite axiomatisation of inductive-inductive definitions PDF

• Fredrik Nordvall Forsberg, Anton Setzer, Inductive-Inductive Definitions, Computer Science Logic, Lecture Notes in Computer Science Volume 6247, 2010, pp 454-468 Paper.

• Fredrik Nordvall Forsberg, Inductive-inductive definitions, PhD thesis

Swansea University, 2013. PDF

• Thorsten Altenkirch, Peter Morris, Fredrik Nordvall Forsberg, Anton Setzer, A Categorical Semantics for Inductive-Inductive Definitions, CALCO, 2011 link

• Thorsten Altenkirch, Paolo Capriotti, Gabe Dijkstra, Fredrik Nordvall Forsberg, Quotient inductive-inductive types, arXiv, 2016

• Ambrus Kaposi and András Kovács, A Syntax for Higher Inductive-Inductive Types, PDF, 2018

• Jasper Hugunin, Constructing Inductive-Inductive Types in Cubical Type Theory, PDF

Parts of the above text are taken from

Last revised on May 30, 2021 at 15:05:54. See the history of this page for a list of all contributions to it.