nLab
inductive family

Context

Deduction and Induction

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Induction

Contents

Idea

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 resuls from the identification of this relation with a family of types.

History

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. Instead, 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.

Semantics

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.

Higher categorical version/ homotopy type theory

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.

References

  • 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

Revised on September 22, 2017 08:00:29 by Bas Spitters (192.38.33.16)