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 resuls 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. 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.
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. Sattler claims to have a generalization of the reduction from indexed W-types to W-types to higher categories/homotopy type theory.