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 and are defined inductively, such that the constructors for can refer to and vice versa. In addition, the constructor for can refer to the constructor for .
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 (cf. the HoTT book real numbers). 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.
Another example of a higher inductive-inductive type is a univalent Tarski universe, where the where a type is defined inductively together with a type family and has constructors
where is the transport function for all and and
This means that is the center of contraction of the fiber of transport across at the equivalence .
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:1612.02346]
Marcelo P. Fiore, Andrew M. Pitts, S. C. Steenkamp, Quotients, inductive types, and quotient inductive types, Logical Methods in Computer Science 18 2 (2022) lmcs:7076 [arXiv:2101.02994, doi:10.46298/lmcs-18(2:15)2022]
For the example of constructing the real numbers (cf. HoTT book real number)
Approaches to a general definition:
Ambrus Kaposi, András Kovács, A Syntax for Higher Inductive-Inductive Types, at 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018) (2018) 20:1-20:18 [pdf, doi:10.4230/LIPIcs.FSCD.2018.20]
Ambrus Kaposi, András Kovács, Signatures and Induction Principles for Higher Inductive-Inductive Types, Logical Methods in Computer Science 16 1 (2020) lmcs:6100 [arXiv:1902.00297, doi:10.23638/LMCS-16(1:10)2020]
Discussion of examples in cubical type theory (cubical Agda):
Last revised on February 10, 2023 at 08:09:36. See the history of this page for a list of all contributions to it.