dybjer1999-inductive-recursive

Abstract

Induction-recursion is a schema which formalizes the principles for introducing new sets in Martin Lof Type Theory. It states that we may inductively define a set while simultaneously defining a function from this set into an arbitrary type by structural recursive. This extends the notion of an inductively defined set substantially and allows us to introduce universes and higher order universes (but not a Mahlo universe). In this article we give a finite axiomatization of inductive-recursive definitions. We prove consistency by constructing a Set-Theoretic Model which makes use of one Mahlo cardinal.

Outline

1. Introduction

2. An Extension of the Logical Framework

3. Inductive Types as Initial Algebras

4. Inductive-Recursive Definitions

Tarski universes are used to

1. Syntax ($U$): They define an inductive type $U$ representing the “codes” of all valid inductive-recursive definitions (SP, “Strict Positivity”).
2. Semantics ($T$): They define a decoding function $T$ recursively, which maps a code $u\in U$ to the actual type-theoretic structure (the endofunctor on $\text{Type}\times \text{Fam}$ needed to form the IR type).

By using a Tarski universe, they treat the concept of Inductive-Recursive definitions as an object language object ($u:U$) that can be manipulated and quantified over within the meta-language (Agda/MLTT), before “running” it via $T$ to get the actual types.

GIven a set of polynomial functors, $\vec{\Phi }=[n]\to \mathcal{U}\Rightarrow \mathcal{U}$ Then the inductive type generated by $\vec{\Phi }$ is a joint Initial Algebras for all $i\in [n]$

$${\mathrm{intro}}_i:{\Phi }_i(U)\to U$$

This can be written as a single functor:

$$\Phi (D)=\sum _{i:I}{\Phi }_i(D)$$

For some suitable indexing set $I$. Consider $\mathcal{U}$ to be the first Tarski Universe, which is defined inductively simmultaneously with the decoding function $T:\mathcal{U}\to \mathrm{Set}$

4.2. A Finite Axiomatization

Define a type for strictly positive functors over each type:

$$\begin{array}{rl}D:\mathcal{U}& ⊢S{P}_D:\mathcal{U}\\ D:\mathcal{U};\varphi :S{P}_D& ⊢{\mathrm{Arg}}_{D,\varphi }:\mathcal{U}\\ \varphi :S{P}_D;U:Set;T:U\to D& ⊢{\arg }_{\varphi }(U,T)\end{array}$$

See the remainder in the paper.

5. Examples

6. Set-Theoretic Model

7. Related and Future Work

Paper