Homotopy Type Theory inductive-inductive type > history (Rev #5, changes)

Showing changes from revision #4 to #5: Added | Removed | Changed

<inductive-inductive type

Idea

Induction-induction is a principle for mutually defining data types A:SetA : Set and B:ASetB: A \to Set. Both AA and BB are defined inductively, and the constructors for AA can refer to BB and vice versa. In addition, the constructor for BB can refer to the constructor for AA. Induction-induction occurs in a natural way when formalising dependent type theory in type theory.

See also inductive-inductive type.

Results

Inductive-inductive types are related to inductive-recursive types. Importantly, inductive-inductive types can be reduced to indexed inductive types.

The consistency of the framework used for the elimination (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 ForsbergSetzer.

Higher inductive inductive types

Experiments with higher inductive inductive types can be found in the book: Cauchy reals (11.3) and Conway surreals (11.6).

References

Fredrik Nordvall Forsberg and Anton Setzer, A finite axiomatisation of inductive-inductive definitions PDF

Fredrik Nordvall Forsberg and 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

Revision on June 9, 2022 at 19:46:03 by Anonymous?. See the history of this page for a list of all contributions to it.