Induction-recursion and initial algebras. (Q1412830): Difference between revisions

Induction-Recursion (IR) is a method of definition in Constructive Type Theory (CTT). One of the first examples is to be found in the work of Martin-Löf in the definition of his universes. Less explicit examples can be found in the theories of Feferman. Martin-Löf's universes are introduced with rules such as the following. \[ \frac{a:U\quad f:E(a)\Rightarrow U}{\sigma(a,f):U}\qquad \frac{a:U\quad f:E(a)\Rightarrow U}{E(\sigma(a,f))=\Sigma(E(a),\lambda x :E(a)\cdot E(f(x)))} \] Here the members of the universe are codes of types and \(E\) is a function that maps the code to the type it denotes. There are two ways of viewing IR. In the first, such definitions are viewed as principles of reflection where the emphasis is placed on the relationship between the types themselves and the codification into the universe: external properties are reflected internally in the universe. In the second, IR is seen as a simultaneous inductive definition of two objects: the universe \(U\) and the decoding function \(E\). These two perspectives are complementary: for certain mathematical purposes one is better than the other. However, the second leads more naturally to implementation. Previously, in the theory known as IR\(_{\text{refl}}\), these authors produced a finite axiomatisation of IR from the first perspective. The present paper provides a formalization of the second one. The new axiomatisation IR\(_{\text{elim}}\) is based upon modelling them as initial algebras in slice categories. The relationship between these two theories is explored in some detail in the paper. The comparisons are carried out in a category-theoretic setting and for this, extensional versions of the two theories are formulated. In addition, to facilitate the comparisons and to act as an intermediary, they provide a third formalization of IR -- the theory IR\(_{\text{init}}^{\text{ext}}\) that is extensional in the standard sense of CTT. Generally, the paper is well written and the technical work clearly motivated. Section 3 provides the new formalization by using algebras in slice categories. Section 4 introduces the theory IR\(_{\text{init}}^{\text{ext}}\) and establishes that IR\(_{\text{elim}}\) can be interpreted in an extension of IR\(_{\text{init}}^{\text{ext}}\) with operator elimination (OP\(_{\text{elim}}\)). Section five displays the correspondence between IR\(_{\text{elim}}\) and IR\(_{\text{refl}}\): the former can be interpreted in the later and IR\(_{\text{elim}}\)+OP\(_{\text{elim}}\) can be interpreted in IR\(_{\text{refl}}\)+SP\(_{\text{elim}}\). Section six changes tack and looks at a specific application of the theory, one of the main conclusions being that the external Mahlo universe is representable as an IR in CTT.