A general formulation of simultaneous inductive-recursive definitions in type theory
P Dybjer - The journal of symbolic logic, 2000 - cambridge.org
The journal of symbolic logic, 2000•cambridge.org
The first example of a simultaneous inductive-recursive definition in intuitionistic type theory
is Martin-Löfs universe à la Tarski. A set U0 of codes for small sets is generated inductively
at the same time as a function T0, which maps a code to the corresponding small set, is
defined by recursion on the way the elements of U0 are generated. In this paper we argue
that there is an underlying general notion of simultaneous inductive-recursive definition
which is implicit in Martin-Löf's intuitionistic type theory. We extend previously given …
is Martin-Löfs universe à la Tarski. A set U0 of codes for small sets is generated inductively
at the same time as a function T0, which maps a code to the corresponding small set, is
defined by recursion on the way the elements of U0 are generated. In this paper we argue
that there is an underlying general notion of simultaneous inductive-recursive definition
which is implicit in Martin-Löf's intuitionistic type theory. We extend previously given …
The first example of a simultaneous inductive-recursive definition in intuitionistic type theory is Martin-Löfs universe à la Tarski. A set U0 of codes for small sets is generated inductively at the same time as a function T0, which maps a code to the corresponding small set, is defined by recursion on the way the elements of U0 are generated.In this paper we argue that there is an underlying general notion of simultaneous inductive-recursive definition which is implicit in Martin-Löf's intuitionistic type theory. We extend previously given schematic formulations of inductive definitions in type theory to encompass a general notion of simultaneous induction-recursion. This enables us to give a unified treatment of several interesting constructions including various universe constructions by Palmgren, Griffor, Rathjen, and Setzer and a constructive version of Aczel's Frege structures. Consistency of a restricted version of the extension is shown by constructing a realisability model in the style of Allen.
