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
Inductive families generalize inductive types. Instead of defining a single type inductively, one simultaneously defines a whole family of types. An alternative term is “indexed inductive definition”.
A simple example of an inductive family is the type of vectors Vect n indexed by the dimension n. This is defined by two constructors: one for the empty vector of dimension 0, and another for the operation which constructs a vector of dimension n+1 by adding a component to a vector of dimension n. The family of finite types Fin n (indexed by n) can also be defined as an inductive family: the constructor 0 is in any Fin n, and there is a successor operation which constructs an element in Fin (n+1) from an element in Fin n.
By the identification of propositions as types, inductive families correspond to inductively defined predicates. For example, the identity type on a type A can be defined inductively by the reflexivity rule stipulating that a is identical to a for any a : A, that is, identity is the least reflexive relation. The identity family of types in intuitionistic type theory results from the identification of this relation with a family of types.
The inductively defined identity type was introduced by Martin-Löf 1973 in his first published paper on Intuitionistic Type Theory.
A general schema for inductive families in Intuitionistic Type Theory was defined in Dybjer91, Dybjer94. This general schema was based on Martin-Löf’s 1971 schema for inductive definitions in predicate logic. Simultaneously, Coquand and Paulin extended the Calculus of Constructions with a similar schema for inductive families. This resulted in the calculus of inductive constructions.
Dybjer and Dybjer and Setzer generalized this schema to inductive-recursive definitions, resulting in “indexed induction-recursion”.
Dybjer and Setzer also distinguish two kinds of inductive (and inductive-recursive) families, restricted (due to Coquand) and general ones. The identity type is an example of the latter, but not of the former.
Inductive families are part of the axiomatic foundation in Coq and agda. However, Lean does not have fix-point expressions, match expressions, or a termination checker in the kernel. Instead, recursive definitions and pattern matching are compiled into eliminators outside of the kernel.
Standard inductive types, W-types can be interpreted in any topos with natural numbers object (Moerdijk-Palmgren). Gambino and Hyland construct initial algebras for dependent polynomial functors. Indexed containers are the same as dependent polynomial functors. Indexed containers are claimed to form a foundation for inductive families.
van den Berg and Moerdijk show that (standard) W-types can be interpreted in certain model categories.
In homotopy type theory with universes, one can reduce indexed W-types to W-types. This has been formalized here, here and here. Sattler outlines a generalization of the reduction to homotopy type theory without the need of universes.
The identity types of an indexed W-type are another indexed W-type. This has been formalized by Huginin.
Per Martin-Löf, Hauptsatz for the intuitionistic theory of iterated inductive definitions, 1971, Studies in Logic and the Foundations of Mathematics - Elsevier
Per Martin-Löf, An Intuitionistic Theory of Types: Predicative Part, 1975, in Logic Colloquium 1973.
Peter Dybjer, Inductive Families Formal aspects of computing 6 (4), 440-465 PS
Peter Dybjer, Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics, 1991 Logical frameworks 2, 6
Peter Dybjer, A general formulation of simultaneous inductive-recursive definitions in type theory, 2000, The Journal of Symbolic Logic 65 (02), 525-549 Peter Dybjer, Anton Setzer, Indexed induction-recursion, 2001 Proof Theory in Computer Science, 93-113
Christine Paulin-Mohring, Inductive definitions in the system Coq rules and properties, 1993 Typed lambda calculi and applications, 328-345.
Thierry Coquand, Christine Paulin, Inductively defined types, COLOG-88 Volume 417 of the series Lecture Notes in Computer Science pp 50-66 Springer G books
Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor McBride, and Peter Morris, Indexed containers PDF
Peter Dybjer and Anton Setzer, Indexed induction-recursion, Journal of Logic and Algebraic Programming, volume 66, Issue 1, January 2006, Pages 1-49. PDF
Nicola Gambino and Martin Hyland, Wellfounded Trees and Dependent Polynomial Functors. PDF
Benno van den Berg, Ieke Moerdijk, W-types in Homotopy Type Theory (arXiv:1307.2765)
Christian Sattler, slides slides
Jasper Hugunin, IWTypes, https://github.com/jashug/IWTypes
Last revised on June 16, 2021 at 08:15:52. See the history of this page for a list of all contributions to it.