natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In type theory, induction-induction is a principle for mutually defining types of the form
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.
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.
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.
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
Univalent Foundations Project, section 11 of Homotopy Type Theory – Univalent Foundations of Mathematics (2013)
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.