Induction-Recursion and Initial Algebras

Peter Dybjer^{∗}and Anton Setzer^{†}

Abstract

Induction-recursion is a powerful definition method in intuitionistic type theory. It extends (generalized) inductive definitions and allows us to define all standard sets of Martin-Löf type theory as well as a large collection of commonly occurring inductive data structures. It also includes a variety of universes which are constructive analogues of inaccessibles and other large cardinals below the first Mahlo cardinal. In this article we give a new compact formalization of inductive-recursive definitions by modeling them as initial algebras in slice categories. We give generic formation, introduction, elimination, and equality rules generalizing the usual rules of type theory. Moreover, we prove that the elimination and equality rules are equivalent to the principle of the existence of initial algebras for certain endofunctors. We also show the equivalence of the current formulation with the formulation of induction-recursion as a reflection principle given in [12]. Finally, we discuss two type-theoretic analogues of Mahlo cardinals in set theory: an external Mahlo universe which is defined by induction-recursion and captured by our formalization, and an internal Mahlo universe, which goes beyond inductionrecursion. We show that the external Mahlo universe, and therefore also the theory of inductive-recursive definitions, have proof-theoretical strength of at least Rathjen’s theory KPM.

1 Introduction

Induction-recursion is a powerful definition method in intuitionistic type theory in the sense of Scott (“Constructive Validity”) [31] and Martin-Löf [17, 18, 19].

The first occurrence of formal induction-recursion is Martin-Löf’s definition of a universe à la Tarski [19], which consists of a set U_{0} of codes for small sets together with a decoding function T_{0} which maps a code to the small set it denotes. U_{0} is inductively generated at the same time as T_{0} is defined by recursion on the elements of U_{0}, and the introduction rules for U_{0} refer to T_{0}. It is called universe “à la Tarski” because of the similarity with Tarski’s truth definition: U_{0} is a generalized syntax of “formulas” and T_{0} maps each formula to its “meaning”. In earlier formulations of Martin-Löf type theory [17, 18] universes are formulated “à la Russell”, where there is no syntactic distinction between an element of U_{0} and the set it denotes. Therefore there is no need for a decoding function and hence there is no (explicit) induction-recursion.

Intuitionistic type theory with inductive-recursive definitions is also a suitable metalanguage for intuitionistic metamathematics. For example, in Martin-Löf’s proof of normalization of an early version of his type theory [20] he introduces Taitstyle computability predicates for dependent types. Whereas Tait defines a family of computability predicates indexed by the types of the simply typed lambda calculus, Martin-Löf’s computability predicates are indexed by those types which themselves are computable. This gives rise to a situation where the computable types are inductively generated at the same time as the computability predicate on terms of such a type is defined, and where the definition of a computable type refers to the notion of a computable term. Martin-Löf presumably considered this definition intuitionistically valid, but did not provide an explicit discussion of why this is so.

∗Department of Computing Science, Chalmers University of Technology, SE-412 96 Gteborg, Sweden. Email: peterd@cs.chalmers.se

†Supported by the Nuffield Foundation, grant No. NAL/00303/G; Department of Computer Science, University of Wales Swansea, Singleton Park, Swansea SA2 8PP, UK, Email:

a.g.setzer@swan.ac.uk

It is a non-trivial problem to give classical mathematical meaning to Martin-Löf’s computability predicates. One approach is due to Aczel [1] for the closely related construction of a Frege structure. Other approaches have been proposed by Allen [2] and by Löfwall and Sjödin [16].

Although Martin-Löf’s computability predicates nowadays can be regarded as an informal example of an inductive-recursive definition and therefore as a precursor of the concept of induction-recursion, its inductive-recursive nature is not explicit: instead of “computable type” Martin-Löf states when the notion of computability for a certain type “has been defined” and there is no explicit notion of proof for the fact that computability has been defined. In order to obtain an explicit inductiverecursive definition one has to formalize the metalanguage. It is an example of indexed induction-recursion [11, 13], since we are defining computability predicates and thus by Curry-Howard indexed families of sets.

More examples of formal induction-recursion occur in recent work on large universes in type theory. These are constructive analogues of large cardinals in set theory. For example, Martin-Löf’s universes are analogues of inaccessible cardinals; Palmgren’s superuniverse [23] is an analogue of a hyperinaccessible cardinal. Rathjen, Griffor and Palmgren’s quantifier universes [30] are analogues of Mahlo’s π-numbers; Palmgren’s higher order universes [25] go even further and are generally conjectured to reach the strength of Rathjen’s theory KPM; in Section 6 we will describe a weak version of Setzer’s Mahlo universe [36, 34, 35], which is still inductive-recursive, and show that it has at least the strength of Rathjen’s theory KPM [28]. Setzer’s original Mahlo universe is an example of a universe which goes beyond induction-recursion.

Induction-recursion as a general unifying principle for definitions of this kind was identified by Dybjer [8, 11], who presents an external schema for their syntactic form. This schema extends earlier schemata for inductive definitions in type theory [6, 7, 9, 26]. Dybjer and Setzer [12] give a finite axiomatization of inductionrecursion as a very general reflection principle. They also show the consistency of their axiomatization by building a model in classical set theory extended by a Mahlo cardinal. In this model function spaces are interpreted as full classical function spaces.

Models for inductive-recursive definitions of a set U with decoding function T are obtained as inductive definitions of the graph of T and captured formally as the least fixed point of a monotone operator on the lattice of subsets of a sufficiently large base set, see Dybjer [11] and the above-mentioned model by Dybjer and Setzer [12]. This should explain why it has not been natural to isolate the concept of induction-recursion in set theory. It also makes it difficult to trace the history of the concept.

In this paper we give a new compact finite axiomatization IR_{elim} of inductiverecursive definitions based on the idea of modeling them as initial algebras in slice categories. Such a categorical model is an abstraction of the above-mentioned set theoretic semantics. It thus provides an alternative view of inductive-recursive definitions to the axiomatization IR_{refl} given by Dybjer and Setzer [12].

The two axiomatizations highlight different aspects of inductive-recursive definitions. IR_{refl} is based on the idea that induction-recursion is a reflection principle. In the paradigmatic example operations on sets, such as Π and Σ, are reflected as operations Π̂ and Σ̂ on a particular set, the first universe U_{0}. Induction-recursion generalizes this idea to operations on arbitrary types. Moreover, IR_{refl} is based on a commuting square generalizing the usual initial algebra diagram used for modelling inductive definitions with the following correspondences:

inductively defined set  initial algebra
recursively defined function initial arrow

IR_{elim} on the other hand coincides with a natural understanding of inductionrecursion: elements of a set U are introduced by a constructor, and for every such element the value of the decoding function T is determined. Therefore it is closer to the standard set theoretic model. It also leads in a natural way to the functors on slice categories associated with the codes for inductive-recursive definition. (We show that the introduction/elimination rules in IR_{elim} are equivalent to the principle that these functors have initial algebras.) The theory IR_{elim} is shorter than IR_{refl}; it has fewer rules and concepts. Moreover, it is easier to construct codes for inductive-recursive definitions in IR_{elim}. As a consequence it is more suitable as a basis for an implementation of induction-recursion. However, each of the formulations has conceptual advantages and is of importance for metamathematical investigations.

Plan of the paper. In Section 2 we introduce the logical framework for intuitionistic type theory. In Section 3 we introduce IR_{elim}. In Section 4 we introduce IR_{init}^{ext}, which axiomatizes closure under certain initial algebras in slice categories, and prove the equivalence of IR_{init}^{ext} and IR_{elim}^{ext} (the extensional version of IR_{elim}). In Section 5 we recall the theory IR_{refl} from Dybjer and Setzer [12] and show that it is equivalent to the two other theories under certain assumptions. Finally, in Section 6 we discuss Setzer’s Mahlo universes which are type-theoretic analogues of Mahlo cardinals in set theory. There are two versions. One is an external Mahlo universe which is defined by induction-recursion and can be formalized in IR_{elim}. We also determine a lower bound for its strength and therefore for IR_{elim}, IR_{init}^{ext} and IR_{refl}. The other version is Setzer’s original internal Mahlo universe, which goes beyond induction-recursion.

2 A Logical Framework for Type Theory

2.1 Basic Rules

In the most recent versions, Martin-Löf type theory is presented in two stages:

• The first stage contains the most basic rules for dependent types. This is often referred to as the “logical framework” or “theory of types”.

• The second stage contains the formation, introduction, elimination, and equality rules for a number of set formers such as N_{n}, N, +, Σ, . . .. This is sometimes referred to as the “theory of sets” and is about the basic notion of set in Martin-Löf type theory, that is, sets as inductively defined data types. It is important to distinguish between this notion of set and the notion of iterative set in the sense of set theory.

All sets introduced at the second stage can be defined by induction-recursion and the remaining sections of this paper provide a complete definition of this “theory of sets”.

In this section we will define the “theory of types”. This will contain the rules for such a theory in Nordström et al [22], but also some new rules. We shall here give an informal introduction and refer the reader to Appendix A for the complete collection of rules.

The logical framework has four forms of judgement:

• A : type,

• A = B : type,

• a : A,

• a = b : A.

Each of these judgements can be hypothetical, that is, depend on a context Γ of the form x_{1} : A_{1}, …, x_{n} : A_{n}, which specifies the types of the free variables x_{i} of the judgement. The empty context (n = 0) is denoted by ∅.

For the treatment of contexts we need a fifth judgement

• Γ context.

A hypothetical judgement is written Γ ⇒ A : type, etc. When presenting inference rules we shall often simplify rules by omitting uniformly appearing contexts (see Appendix A for details).

As usual, we have a type set, but we also add a new type stype of “small types”. This contains all sets and is closed under 0, 1, 2, dependent product and dependent function space. (All these constructions are introduced below. Synonyms of “dependent product type” are “disjoint union of a family of types” and “Σ-type”, and synonyms of “dependent function space” are “Cartesian products of a family of types” and “Π-type”). However set itself is not an element of stype. The reason for the need for stype is discussed in Section 3.2 and [11]. ^{1}

We have the following rules:

set : type  stype : type
\frac{A : set}{A : stype}  \frac{A : stype}{A : type}

\frac{A = B : set}{A = B : stype}  \frac{A = B : stype}{A = B : type}

0, 1 and 2 are stypes with 0, 1, 2 elements respectively. In the case of 1 we add the η-rule. This has the effect that for any set A, the functions f_{0} := (x, y)x : A → (1 → A) and f_{1} := (x)x(∗) : (1 → A) → A are inverses with respect to definitional equality, that is, we have definitionally f_{0}∘f_{1} = id and f_{1}∘f_{0} = id (with id := (x)x). The same holds for g_{0} := (x)⟨x, ∗⟩ : A → (A × 1) and g_{1} := (x)π_{0}(x) : (A × 1) → A (where π_{0} is left projection). The stype 0 is added for systematic reasons. If we omitted it we could still define the empty set as the set N_{0} with only one constructor of type N_{0} → N_{0}, see p. 13.

1In the proof assistant Agda for type theory (developed by C. Coquand and T. Coquand [5])

the logical framework has been modified so that the type set is closed under the dependent product and dependent function space of the logical framework. If we formulated induction-recursion based on that version of the logical framework there would be no need to distinguish between stype and set.

The rules for 0, 1, 2 are:

0 : stype  \frac{a : 0  x : 0 ⇒ A : type}{case_{0}(a) : A}

1 : stype  ∗ : 1  \frac{a : 1}{a = ∗ : 1}

2 : stype  ∗_{0} : 2  ∗_{1} : 2

\frac{x : 2 ⇒ A : type  a : 2  b : A[x := ∗_{0}]  c : A[x := ∗_{1}]}{case_{2}((x)A, a, b, c) : A[x := a]}

\frac{x : 2 ⇒ A : type  b : A[x := ∗_{0}]  c : A[x := ∗_{1}]}{case_{2}((x)A, ∗_{0}, b, c) = b : A[x := ∗_{0}]}

\frac{x : 2 ⇒ A : type  b : A[x := ∗_{0}]  c : A[x := ∗_{1}]}{case_{2}((x)A, ∗_{1}, b, c) = c : A[x := ∗_{1}]}

Both type and stype are closed under dependent function types written as (x : A) → B. Function abstraction is written as (x : A)a and application as a(b). They are related by both the β- and the η-rule. Further type and stype are closed under dependent products written as (x : A) × B. Pairs are written as ⟨a, b⟩ and the left and right projection of a is written as π_{0}(a) and π_{1}(a). Again, we have analogues of β and η (surjective pairing).

We also use some abbreviations. We omit the type in an abstraction, that is, write (x)a instead of (x : A)a. We sometimes write curried function types as (x_{1} : A_{1}, …, x_{n} : A_{n}) → A instead of (x_{1} : A_{1}) → … → (x_{n} : A_{n}) → A, and omit variables which are not used. A → B := (A) → B. We write repeated application as a(b_{1}, …, b_{n}) instead of a(b_{1}) ⋯ (b_{n}), and repeated abstraction as (x_{1}, …, x_{n})a instead of (x_{1}) ⋯ (x_{n})a. Furthermore, if we apply an expression f(a_{1}, …, a_{n}) introduced in this form by a rule to arguments b_{1}, …, b_{k}, we write f(a_{1}, …, a_{n}, b_{1}, …, b_{k}) instead of f(a_{1}, …, a_{n})(b_{1}, …, b_{k}).

We will in the following not mention equality versions of the rules. Moreover, we will omit types and premises in equality judgements and use “bracket notations” like E[t] as usual, see General Assumption A.0.3 in Appendix A for details.

We introduce furthermore the following notation for the definition of a function from one type into a product type from its two projections: Assume Assume the following: A : type; x : A ⇒ B[x] : type; x : A, y : B[x] ⇒ C[x, y] : type; f : A → B[x] and g : (x : A) → C[x, f(x)]. Then

⟨f, g⟩^{fun} := (x)⟨f(x), g(x)⟩ : A → ((y : B[x]) × C[x, y]) .

2.2 Extensions of the Logical Framework

In the subsequent three sections we shall give three different formalizations of inductive-recursive definitions in type theory: IR_{elim} (Section 3), IR_{init}^{ext} (Section 4) and IR_{refl} (Section 5). We shall also prove the equivalence of these three theories extended by further rules and will therefore introduce additional theories.

Each of these theories consists of the rules of the logical framework together with some (yet to be specified) rules for inductive-recursive definitions. A rule r is here an n + 1-tuple Γ_{1} ⇒ θ_{1}, …, Γ_{n+1} ⇒ θ_{n+1} of dependent judgements in the language of type theory with respect to a certain collection of constructors (for a full formalization of the language of type theory see for instance Setzer [33], chapter 2). If R is a collection of rules we introduce the type theory TT(R). We use the notation R ⊢ Γ ⇒ θ to make explicit that the judgement θ is derivable in the context Γ by using the rules of the logical framework (without extensionality) and by applying rules in R: If r is as above and R ⊢ Γ_{i} ⇒ θ_{i} (i = 1, …, n), then R ⊢ Γ_{n+1} ⇒ θ_{n+1}. We will as usual suppress R when writing down the judgements of type theory and often also keep the context Γ implicit.

2.3 Extensional Equality

Some of the rules of the theory IR_{init}^{ext} will only be typeable if we assume certain rules of extensional equality. These rules are similar to those of Martin-Löf’s extensional type theory [18, 19] but are here formulated for the types and stypes of the logical framework. (Martin-Löf’s extensional type theory was formulated without a logical framework.)

\frac{A : type  a : A  b : A}{a =_{A} b : type}  \frac{A : stype  a : A  b : A}{a =_{A} b : stype}

\frac{A : type a : A}{ref : a =_{A} a}

\frac{A : type  a : A  b : A  r : a =_{A} b}{a = b : A}

\frac{A : type  a : A  b : A  r : a =_{A} b}{r = ref : a =_{A} b}

We define for A : type, x : A ⇒ B[x] : type

(f =_{(x:A)→B[x]}^{fun} g) := (x : A) → (f(x) =_{B[x]} g(x)) ,

which is equivalent to f =_{(x:A)→B} g, but has proof objects which can be used more directly.

We will also need to add the extensionality rules to IR_{elim} and IR_{refl} (yielding IR_{elim}^{ext} and IR_{refl}^{ext}) in order to prove their equivalence to IR_{init}^{ext}.

We want to emphasize that the rules for extensional equality are not needed when formulating IR_{elim} and IR_{refl}: the formation, introduction, elimination, and equality rules are all typeable in intensional type theory, and it is therefore possible to consider them in that setting as well. However, our experience suggests that some constructions in intuitionistic metamathematics are difficult and perhaps even impossible to perform in intensional type theory, and that intensional type theory is sometimes counterintuitive – proofs which one informally believes are correct turn out to be incorrect when type checking them formally. It seems therefore that the extensional versions IR_{elim}^{ext} or IR_{refl}^{ext} are closer to our mathematical intuition and therefore more natural. On the other hand it is possible to construct nonnormalizing terms in extensional type theory so decidability of type-checking is lost. It is this property that is used crucially in the elegant implementations of proof assistants for intensional type theory.

2.4 The Category of Types

All three formalizations are based to a lesser or greater extent on category-theoretic ideas. However the definitions in the category theoretical part can be done only in the presence of extensional equality. We shall introduce for each collection of rules R, which contains the rules of extensionality, and each context Γ the category Type_{R}(Γ). Its objects are A such that R ⊢ Γ ⇒ A : type and we identify objects A, B such that R ⊢ Γ ⇒ A = B : type. Arrows from A to B are functions f for which we can prove R ⊢ Γ ⇒ f : A → B (and again we identify f, g such that R ⊢ Γ ⇒ f = g : A → B).

We shall also usually suppress R and Γ in Type_{R}(Γ) and simply write Type. It is only IR_{init}^{ext} which pursues the categorical approach fully. This theory

is obtained by postulating, in the language of type theory, that for each type D and each code γ (for an inductive-recursive definition with decoding into D) there exists a certain endofunctor 𝔽_{γ} on the slice category Type/D (more precisely Type_{IR_{init}^{ext}}(Γ)/D) and that this endofunctor has an initial algebra.

Here we recall that the objects of the slice category Type/D are pairs ⟨U, T ⟩ such that U is an object and T : U → D in Type. Arrows from ⟨U, T ⟩ to ⟨U′, T′⟩ are pairs ⟨f_{0}, f_{1}⟩ of reindexing functions functions f_{0} : U → U′ and proofs f_{1} : T′∘f_{0} =_{U→D}^{fun} T (in R under assumption Γ). f_{1} is therefore a proof that a certain diagram commutes, a fact indicated as follows:

U  \overline{f_{0}} U′

[figure: T; f_{1}; T′]

D

Again we identify ⟨f_{0}, f_{1}⟩ and ⟨f′_{0}, f′_{1}⟩, such that f_{0} and f′_{0} are equal as arrows in Type/D (which implies by uniqueness of equality proofs that we can prove in R and under assumption Γ f_{1} = f′_{1}.)

Both IR_{elim} and IR_{refl} also use categorical ideas to some extent, but in both cases the main guideline has been to formulate the rules in a way which is natural from a type-theoretic perspective and which recovers the usual rules of type theory without undue coding. So it will not be appropriate to investigate the categorical properties of Type_{IR_{elim}} and Type_{IR_{refl}} – in fact one needs to modify the definition of Type first in order to obtain categories at all, which then still lack many of the expected properties. However, in the presence of extensional equality and induction on the collection of strictly positive functors these theories will be equivalent to IR_{init}^{ext}.

3 A New Formalization of Induction-Recursion

In this section we shall give the formal rules of the theory IR_{elim}. To motivate these rules we shall begin with some informal discussion. There are two issues:

• the correspondence between certain endofunctors on slice categories and the rules for inductive-recursive definitions;

• which endofunctors arise in this way.

3.1 Algebras in Slice Categories

Consider again the first universe à la Tarski U_{0} with decoding T_{0} : U_{0} → set. This universe is closed under the formation of Σ-types, so there is a constructor^{2}

Σ̂ : ((a : U_{0}) × (T_{0}(a) → U_{0})) → U_{0} ,

2Note that we here use the uncurried version of the constructor, whereas the usual logical framework based version of type theory employs the curried version.

which is decoded as

T_{0}(Σ̂(⟨a, b⟩)) = Σ(T_{0}(a), T_{0} ∘ b) .

Observe the occurrence of T_{0} in the introduction rule for U_{0}.

We can draw the defining equation for T_{0} as a commuting diagram

(a : U_{0}) × (T_{0}(a) → U_{0})  \overline{Σ̂} U_{0}

[figure: ⟨a, b⟩ ↦ Σ(T_{0}(a), T_{0} ∘ b); T_{0}]

set

Consider now the above under the additional assumption of extensionality in the slice category Type/set. We note that the above diagram expresses that we have an 𝔽_{0}-algebra for a certain endofunctor 𝔽_{0} on Type/set the object part of which has the following two components:

𝔽 _{0}^{U}(U, T) = (a : U) × (T (a) → U) ,
𝔽 _{0}^{T}(U, T, ⟨a, b⟩) = Σ(T (a), T ∘ b) .

(To avoid confusion, note that U in italic font is a variable ranging over arbitrary sets, whereas U_{0} (and later U) in Roman font are constant sets defined by inductionrecursion, and similarly for italic T and Roman T_{0} and T.) When formalized in type theory, this 𝔽_{0}-algebra becomes a quadruple

⟨U_{0}, T_{0}, Σ̂, eq_{0}⟩

(where eq_{0} is a proof of the commutativity of the above mentioned diagram).

In IR_{elim} we will also have a principle of universe-elimination for U_{0} motivated by syntactic considerations. In IR_{init}^{ext} however, universe-elimination is replaced by the principle that ⟨U_{0}, T_{0}, Σ̂, eq_{0}⟩ is an initial 𝔽_{0}-algebra. Furthermore we shall show in 4.4 that these principles are equivalent assuming rules of extensionality.

3.2 Inductive and Non-inductive Arguments

To get a complete formalization we must specify which endofunctors give rise to type-theoretically justifiable constructions. To motivate this specification we shall analyze the structure of a number of constructors (or introduction rules) for sets in type theory, and in particular emphasize the distinction between inductive and non-inductive arguments of a constructor (or premises of an introduction rule).

We shall first look at the case of inductive definitions, that is, the special case of inductive-recursive definitions where a recursively defined function does not participate in the inductive generation process.

The simplest inductive definition is that of a finite set N_{k} with constructors i_{k} : N_{k}^{3} (i = 0, …, k − 1). The constructors have no arguments at all.

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} N_{k} 0^{k}  (k − 1)^{k}

3Note that i_{k} is the ith element of the set N_{k} and should not be confused with the notation for sequences as used in mathematics.

In this diagram, the arrow represents the constructor.

The next example is the disjoint union of two sets A + B with constructors i : A → A + B and j : B → A + B. A and B are arbitrary previously defined sets, which we refer to as parameters of the definition.

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} A + B^{i(a)}  ^{j(b)}^{a}  ^{b} A  B

The next example is the set Σ(A, B) with constructor p : (x : A, B(x)) → Σ(A, B): it has two arguments, where the index set B(x) of the second one depends on the first argument A. Again this can be parameterized by A : set and B : (x : A) → set.

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}_{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} Σ(A,B) A  B(a) a b  p(a,b)

In this diagram, the dotted arrows denote dependencies of later arguments of the constructor on previous arguments.

The set N of natural numbers has constructors 0 : N and S : N → N. Here, the type of the argument of S is N itself. We call such an argument “inductive”.^{4} In contrast, all previous arguments are “non-inductive”, since their types only refer to previously defined sets.

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} N S 0

If we look at the set W(A, B) with constructor sup : (r : A, s : B(r) → W(A, B)) → W(A, B) we see that we have one non-inductive argument r and a family of inductive arguments s indexed by the set B(r):

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} W(A,B)  sup(r,s) B(r) A  r s(x)

The primary example of proper induction-recursion is the definition of the universe à la Tarski. We note that U_{0} is defined inductively, and while defining it, we simultaneously define recursively for every element a : U_{0} a set T_{0}(a) : set. Consider the constructor Σ̂ : (a : U_{0}, b : T(a) → U_{0}) → U_{0} with T_{0}(Σ̂(a, b))= Σ(T_{0}(a), (x)T_{0}(b(x))) : set. Σ̂ has two inductive arguments, where the second depends on the first. This dependence is not direct (since U_{0} is not defined yet), but indirect via T_{0}, that is, using the recursion-hypothesis for T_{0}. Finally, the definition of T_{0}(Σ̂(a, b)) refers to the value of T_{0} for all inductive arguments:

4In [11] the terminology “recursive argument” was used, but “inductive argument” seems to be better in connection with induction-recursion, since it primarily has to do with the inductively defined set and only indirectly with the recursively defined function.

.^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}  ^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.}^{.} U^{a}  ^{Σ̂(a,b)}^{T(a)}  ^{T(a)}^{b(x)}  ^{b(y)}  ^{b(z)}^{T(b(x))}  ^{Σ (T(a),T∘b)}

In this diagram ↦ represents the function mapping the constructed element to the recursively defined result. The dotted arrows express dependencies of later arguments of the constructor and of the recursively defined result of the constructor on previous arguments.

We shall analyze the common structure of the examples above. First the arguments are classified as either inductive or non-inductive.

The type of a non-inductive argument is an stype. The typical case is that it is a set, for instance the two arguments of the constructor p for Σ(A, B) are elements of the sets A and B(a). In the case of Π(A, B) we have one constructor λ : (f : (x : A) → B) → Π(A, B) and the non-inductive argument f is indexed over the stype (x : A) → B. This type is not a set. In fact, this is why we cannot simply require that the type of a non-inductive argument is a set: we want to follow Martin-Löf and define Π-sets as inductively generated by λ.

An inductive argument is indexed by an stype. It can be a set, for example the second argument of W(A, B) is indexed by the set B(a), or it can be an stype, for example the argument of the successor in N is indexed by 1. Note that because of the η-rule for 1 there are bijections between 1 → A and A and an argument indexed over 1 is nothing but a single argument.

The type of later arguments may depend on earlier arguments. The dependency on a non-inductive argument is direct. However, a direct dependency on an inductive argument is not possible, because we cannot make use of the set we are currently defining. However an indirect dependency is possible, namely on the result of the recursively defined function T applied to the elements of the inductively defined set U indexed by the argument.

The result of T for an element introduced by a constructor depends on the arguments of the constructor in the same way as later arguments depend on previous ones.

If a set has several constructors it will be convenient to code them as one constructor with an extra argument indexed by a finite set which selects the chosen constructor. As we show below, the finite sets N_{k} can be built up successively from 0, 1, and 2 by using inductive definitions.

3.3 The Type OP_{D} of Operators on Families of D

We want to define a type OP_{D} of codes γ for all inductive-recursive definitions of sets U_{γ} : set, T_{γ} : U_{γ} → D. U_{γ} will have one constructor, the arguments of which are elements of an stype which depends on U_{γ}, T_{γ}. Further the result of T_{γ} for an element introduced by a constructor will depend on U_{γ}, T_{γ} and the arguments of that constructor. So we will associate with every γ a function

𝔽_{γ} : ((X : set) × (X → D)) → ((X : stype) × (X → D)) ,

and ⟨U_{γ}, T_{γ}⟩ is the least set “closed under 𝔽_{γ}”, i.e. such that every a : π_{0}(𝔽_{γ}(⟨U_{γ}, T_{γ}⟩)) is represented as a canonical element intro_{γ}(a) in U_{γ} with T_{γ}(intro_{γ}(a)) = π_{1}(𝔽_{γ}(⟨U_{γ}, T_{γ}⟩))(a).

The above definition cannot be simplified by defining by induction on γ directly the type of the arguments of the constructor of U_{γ}: we cannot make use of the induction hypothesis relative to U_{γ′}, T_{γ′}.

So elements of OP_{D} represent primarily functions from set-indexed to stypeindexed families of D. The inductive-recursively defined sets are obtained as the least set-indexed family of D which is “closed under this function”. In the theory IR_{init}^{ext}, this picture becomes more clear: there OP_{D} is a type of codes of endofunctors in the slice category Type/D and U_{γ}, T_{γ} together with the constructor and an equality proof form an initial algebra with respect to this functor.

In the following D will be a global parameter. Thus in the rest of the article we shorten our notations as follows:

General assumption 3.3.1 (a) We assume Γ ⇒ D : type (but will usually suppress Γ).

(b) We suppress a first premise D : type, which has to be added to each rule referring to D.

(c) We write, if some γ : OP_{D} occurs as a parameter, γ instead of D, γ.

The formation rule for OP is

OP_{D} : type .

To each code γ we associate the two components of 𝔽_{γ} above (note however that OP is an inductive definition, not an inductive-recursive definition on type level, and the inductive definition of OP_{D} does not refer to 𝔽^{U}, 𝔽^{T}).

\frac{γ : OP_{D}  U : set  T : U → D}{𝔽 _{γ}^{U}(U, T) : stype}

\frac{γ : OP_{D}  U : set  T : U → D}{𝔽 _{γ}^{T}(U, T) : 𝔽 _{γ}^{U}(U, T) → D}

We have the following rules for generating elements of OP_{D}:

• Addition of a non-inductive argument:

\frac{A : stype γ : A → OP_{D}}{σ(A, γ) : OP_{D}}

σ(A, γ) (where σ stands for the Σ-type) is a code for an inductive-recursive definition the constructor of which has one non-inductive argument a : A and depending on it other arguments given by γ(a). The result of T for an element introduced by a constructor with argument starting with a : A is the result obtained for the remaining arguments with respect to γ(a):

– 𝔽 _{σ(A,γ)}^{U}(U, T) = (a : A) × 𝔽 _{γ(a)}^{U}(U, T),

– 𝔽 _{σ(A,γ)}^{T}(U, T, ⟨a, b⟩) = 𝔽 _{γ(a)}^{T}(U, T, b).

• Addition of an inductive argument:

\frac{A : stype γ : (A → D) → OP_{D}}{δ(A, γ) : OP_{D}}

δ(A, γ) (where δ stands for dependent Σ) is a code for an inductive-recursive definition the constructor of which has one inductive argument indexed over A and, if this argument is f : A → U, the other arguments determined by γ(T ∘ f). The result of T for an element introduced by a constructor with such an argument is the result of it for the remaining arguments with respect to γ(T ∘ f):

– 𝔽 _{δ(A,γ)}^{U}(U, T) = (f : A → U) × 𝔽 _{γ(T ∘f)}^{U}(U, T),

– 𝔽 _{δ(A,γ)}^{T}(U, T, ⟨f, b⟩) = 𝔽 _{γ(T ∘f)}^{T}(U, T, b).

• Base case:

\frac{ψ : D}{ι(ψ) : OP_{D}}

ι(ψ) is an inductive-recursive definition with no arguments of the constructor and ψ as the result of T for an element introduced by it:

– 𝔽 _{ι(ψ)}^{U}(U, T) = 1,

– 𝔽 _{ι(ψ)}^{T}(U, T, ∗) = ψ.

Definition 3.3.2 The formation and introduction rules for OP are the rules in this subsection.

3.4 Formation and Introduction Rules for U, T

Definition 3.4.1 Assume γ : OP_{D}. The formation rules for U_{γ}, T_{γ} are the following:

U_{γ} : set T_{γ} : U_{γ} → D

The introduction rules for U_{γ} and equality rules for T_{γ} are

\frac{a : 𝔽 _{γ}^{U}(U_{γ}, T_{γ})}{intro_{γ}(a) : U_{γ}}  \frac{a : 𝔽 _{γ}^{U}(U_{γ}, T_{γ})}{T_{γ}(intro_{γ}(a)) = 𝔽 _{γ}^{T}(U_{γ}, T_{γ}, a) : D}

The formation/introduction rules for U, T are the rules above.

3.5 Elimination and Equality Rules for U, T

We are going to define elimination rules for U_{γ}. Inductively defined sets like the set of natural numbers or the W-type are special cases of inductive-recursive definitions, so we obtain elimination rules for these sets as well as we do for universes (as introduced by Palmgren [24]).

We have to collect the induction hypotheses with respect to an argument of intro_{γ}, that is, with respect to an element u of 𝔽 _{γ}^{U}(U_{γ}, T_{γ}). The induction hypothesis consists of the value of the function to be defined for all references to U_{γ} by inductive arguments in u, and will be an element of type 𝔽 _{γ}^{IH}(U_{γ}, T_{γ}, E, u) with the following formation and equality rules:

\frac{γ : OP_{D}  U : set  T : U → D u : 𝔽 _{γ}^{U}(U, T)  x : U ⇒ E[x] : type}{𝔽 _{γ}^{IH}(U, T, E, u) : type}

𝔽 _{ι(ψ)}^{IH}(U, T, E, u) = 1 ,
𝔽 _{σ(A,γ)}^{IH}(U, T, E, ⟨a, b⟩) = 𝔽 _{γ(a)}^{IH}(U, T, E, b) ,
𝔽 _{δ(A,γ)}^{IH}(U, T, E, ⟨f, b⟩) = ((x : A) → E[f(x)]) × 𝔽 _{γ(T ∘f)}^{IH}(U, T, E, b) .

Note that we allow E[x] to be an arbitrary type, that is, it does not need to be a set as in ordinary elimination rules. See [11] for a discussion of the need for such a large elimination schema in induction-recursion.

For the equality rules we need to define elements of 𝔽 _{γ}^{IH}(U_{γ}, T_{γ}, E, u) from the values of recursively defined functions on the inductive arguments of u. This is the purpose of the operation 𝔽 _{γ}^{map}:

\frac{γ : OP_{D}  U : set  T : U → set x : U ⇒ E[x] : type  h : (x : U) → E[x]}{𝔽 _{γ}^{map}(U, T, E, h) : (u : 𝔽 _{γ}^{U}(U, T)) → 𝔽 _{γ}^{IH}(U, T, E, u)}

𝔽 _{ι(ψ)}^{map}(U, T, E, h, ∗) = ∗ ,
𝔽 _{σ(A,γ)}^{map}(U, T, E, h, ⟨a, b⟩) = 𝔽 _{γ(a)}^{map}(U, T, E, h, b) ,
𝔽 _{δ(A,γ)}^{map}(U, T, E, h, ⟨f, b⟩) = ⟨h ∘ f, 𝔽 _{γ(T ∘f)}^{map}(U, T, E, h, b)⟩ .

Definition 3.5.1 Assume γ : OP_{D}. The elimination rule for U_{γ}, T_{γ} is the following:

\frac{x : U_{γ} ⇒ E[x] : type g : (u : 𝔽 _{γ}^{U}(U_{γ}, T_{γ}), 𝔽 _{γ}^{IH}(U_{γ}, T_{γ}, E, u)) → E[intro_{γ}(u)]}{R_{γ,E}(g) : (u : U_{γ}) → E[u]}

The equality rule is

\frac{x : U_{γ} ⇒ E[x] : type g : (u : 𝔽 _{γ}^{U}(U_{γ}, T_{γ}), 𝔽 _{γ}^{IH}(U_{γ}, T_{γ}, E, u)) → E[intro_{γ}(u)] u : 𝔽 _{γ}^{U}(U_{γ}, T_{γ})}{R_{γ,E}(g, intro_{γ}(u)) = g(u, 𝔽 _{γ}^{map}(U_{γ}, T_{γ}, E, R_{γ,E}(g), u)) : E[intro_{γ}(u)]}

Note that these rules presuppose the formation and introduction rules for OP and for U, T.

Definition 3.5.2 IR_{elim} is the extension of the logical framework by the formation and introduction rules for OP and the formation, introduction, elimination, and equality rules for U, T. IR_{elim}^{ext} is the extension of IR_{elim} by the rules of extensionality.

3.6 OP_{D}-Codes for Some Standard Sets

Let us briefly review the examples of inductive and inductive-recursive definitions in Section 3.2 and assign codes in OP_{D} to them.

In the first examples, we just have inductive definitions - there is no recursively defined T_{γ} participating in the generation of U_{γ}. In this case we introduce a dummy function T_{γ} : U_{γ} → 1 so that the code for the inductive definition is an element γ : OP_{1}. We will only define the corresponding γ : OP_{1}, the sets defined are then U_{γ}. Let ι_{∗} := ι(∗) : OP_{1}.

The empty stype 0 is part of our logical framework and we can code the set N_{0} as

γ_{N_{0}} := σ(0, (x)ι_{∗}) : OP_{1} .

But it is possible to define N_{0} without 0, since it can be defined as the set with only one constructor with type N_{0} → N_{0}. This definition has code

γ′_{N_{0}} := δ(1, (f)ι_{∗}) : OP_{1} .

In Appendix B we prove that for the second definition of N_{0} we can define ex falsum quodlibet.

The other finite sets have codes

γ_{N_{1}} := ι_{∗} : OP_{1} ,
γ_{N_{n+2}} := σ(2, (x)case_{2}(x, γ_{N_{n+1}}, ι_{∗})) : OP_{1} .

A + B and Σ(A, B) have codes

γ_{A+B} := σ(2, (x)case_{2}(x, σ(A, (x)ι_{∗}), σ(B, (x)ι_{∗}))) ,
γ_{Σ(A,B)} := σ(A, (x)σ(B(x), (y)ι_{∗})) .

With this definition the constructor of Σ has two arguments. An alternative is to have one argument having as type the dependent product of the logical framework:

γ′_{Σ(A,B)} := σ((x : A) × B, (y)ι_{∗}) .

N has code

γ_{N} := σ(2, (x)case_{2}(x, ι_{∗}, δ(1, (y)ι_{∗}))) .

Zero is here intro_{γ_{N}}(⟨∗_{0}, ∗⟩), and the successor of n is intro_{γ_{N}}(⟨∗_{1}, ⟨n, ∗⟩⟩). W(A, B) has code

γ_{W(A,B)} := σ(A, (x)δ(B(x), (y)ι_{∗})) .

Finally, the first universe (consisting of U_{0} : set and T_{0} : U_{0} → set and for simplicity closed under N and Σ only) has code

γ_{U_{0},T_{0}} := σ(2, (x)case_{2}(x, ι(N), δ(1, (A)δ(A(∗), (B)ι(Σ(A(∗), B)))))) : OP_{set} .

4 Initial Algebras in Slice Categories

In this section we pursue the categorical point of view and introduce the theory IR_{init}^{ext} which expresses closure under initial 𝔽_{γ}-algebras. The ext in IR_{init}^{ext} indicates that we here assume the rules of extensional equality.

We will also introduce the principle of OP-elimination and prove that this principle entails the equivalence of IR_{init}^{ext} and IR_{elim}^{ext}. This can be viewed as yet another theorem showing the correspondence between syntactic theories and categorical models, such as the correspondence between the typed lambda calculus and Cartesian closed categories, between (impredicative) intuitionistic type theory in the sense of Lambek and Scott [15] and toposes, etc. Note however, that we here only treat the categorical semantics of induction-recursion and not of the logical framework. The reader is referred to the literature on categorical semantics of dependent types for the latter, see for example Cartmell [4], Seely [32], Dybjer [10] or Hofmann [14].

The categorical semantics of universes has previously been investigated by Mendler [21]. There he considers various universes which are all inductive-recursive definitions with D = set. Our approach goes further since we consider inductive-recursive definitions with arbitrary D and characterize the collection of endofunctors which have initial algebras.

4.1 Strictly Positive Endofunctors on Type/D

First we shall show how to define an endofunctor 𝔽_{γ} in the category Type/D. For arguments U, T with U : set the object part of this functor coincides with 𝔽 _{γ}^{U} and 𝔽 _{γ}^{T} in IR_{elim}. In order to obtain a functor in Type/D, we have to allow the argument U to be a type as well. So we have the new rules:

\frac{γ : OP_{D}  U : type  T : U → D}{𝔽 _{γ}^{U}(U, D) : type}

\frac{γ : OP_{D}  U : type  T : U → D}{𝔽 _{γ}^{T}(U, D) : 𝔽 _{γ}^{U}(U, T) → D}

and the equality rules extended to U : type.

We shall now define the arrow part 𝔽 \overrightarrow{γ} of the functor:

[figure: U; f_{0}; U′; 𝔽 _{γ}^{U}(U, T); 𝔽 \overrightarrow{γ}(f_{0}, f_{1}); 𝔽 _{γ}^{U}(U′, T′)]

[figure: T; f_{1}; T′; ↦; 𝔽 _{γ}^{T}(U, T); (x)ref; 𝔽 _{γ}^{T}(U′, T′)]

D  D

Note that in this type-theoretic formalization 𝔽 \overrightarrow{γ}(f_{0}, f_{1}) has two main arguments: the arrow f_{0} and the proof f_{1} that the triangle commutes. The rules are:

\frac{γ : OP_{D} U : set  T : U → D U′ : set  T′ : U′ → D f_{0} : U → U′ f_{1} : T =_{U→D}^{fun} T′ ∘ f_{0}}{𝔽 \overrightarrow{γ}(f_{0}, f_{1}) : 𝔽 _{γ}^{U}(U, T) → 𝔽 _{γ}^{U}(U′, T′)}

(We have suppressed the arguments U, T, U′, T′ of 𝔽 \overrightarrow{γ}, which are implicitly contained in f_{0}, f_{1}.)

𝔽 \overrightarrow{ι(ψ)}(f_{0}, f_{1}, ∗) = ∗ ,
𝔽 \overrightarrow{σ(A,γ)}(f_{0}, f_{1}, ⟨a, b⟩) = ⟨a, 𝔽 \overrightarrow{γ(a)}(f_{0}, f_{1}, b)⟩ ,
𝔽 \overrightarrow{δ(A,γ)}(f_{0}, f_{1}, ⟨g, b⟩) = ⟨f_{0} ∘ g, 𝔽 \overrightarrow{γ(T ∘g)}(f_{0}, f_{1}, b)⟩ .

Note that in the last equality we use that T′ ∘ f_{0} ∘ g = T ∘ g by f_{1} and extensionality.

The commutativity of the right triangle in the diagram above is expressed by the following rule:

\frac{γ : OP_{D} U : set  T : U → D U′ : set  T′ : U′ → D f_{0} : U → U′ f_{1} : T =_{U→D}^{fun} T′ ∘ f_{0}}{𝔽 _{γ}^{T}(U′, T′) ∘ 𝔽 \overrightarrow{γ}(f_{0}, f_{1}) = 𝔽 _{γ}^{T}(U, T) : 𝔽 _{γ}^{U}(U, T) → D}

(In extensional type theory the proof object of an equality type is irrelevant, since it is equal to ref. Therefore, when stating rules which generate elements of equality types, we will not introduce a new constant which generates a proof object, but instead write the conclusion of such a rule in the form of a judgement r = s : A, as in the rule above).

Further we have rules expressing the functor laws:

𝔽 \overrightarrow{γ}(id, (x)ref) = id : 𝔽 _{γ}^{U}(U, T) → 𝔽 _{γ}^{U}(U, T) ,
𝔽 \overrightarrow{γ}(f_{0} ∘ f_{1}, (x)ref) = 𝔽 \overrightarrow{γ}(f_{0}, (x)ref) ∘ 𝔽 \overrightarrow{γ}(f_{1}, (x)ref) ,

: 𝔽 _{γ}^{U}(U, T) → 𝔽 _{γ}^{U}(U′′, T′′) .

Definition 4.1.1 The rules for 𝔽^{→} are the rules above in this subsection. (They presuppose the formation/introduction rules for OP and for U, T and the rules of extensionality).

Remark 4.1.2 In the presence of elimination rules for OP (see below) the rules expressing the functor laws and the equality 𝔽 _{γ}^{T}(U′, T′)∘𝔽 \overrightarrow{γ}(f_{0}, f_{1}) = 𝔽 _{γ}^{T}(U, T) can be proved by induction on γ and therefore be omitted in the formal theory.

The object part of the functors 𝔽_{γ} refers to the argument U only strictly positively, but to T applied to these arguments both positively and negatively. This motivates part (b) of the following definition:

Definition 4.1.3 (a) Let for γ : OP_{D} be 𝔽_{γ} the endofunctor on Type/D (with respect to rules R which contain the rules introduced in this section and those presupposed by it) with

• object part 𝔽_{γ}(⟨U, T ⟩) := ⟨𝔽 _{γ}^{U}(U, T), 𝔽 _{γ}^{T}(U, T)⟩ and

• arrow part 𝔽_{γ}(⟨h_{0}, h_{1}⟩) := ⟨𝔽 \overrightarrow{γ}(h_{0}, h_{1}), (x)ref⟩.

(b) The strictly positive endofunctors on Type/D are the functors 𝔽_{γ} for γ : OP_{D}.

We can give the following names to strictly positive endofunctors on Type/D:

• 𝔽_{ι(ψ)} is the “constant functor”, the result of which does not depend on the arguments.

• 𝔽_{σ(A,γ)} is the “disjoint union of functors”: the first component of the object part is a disjoint union of the first components of the object parts of 𝔽_{γ(a)} (a : A), and the other parts are defined accordingly.

• 𝔽_{δ(A,γ)} is the “dependent disjoint union of functors”: the first component of the object part is the disjoint union of the first components of the object parts of 𝔽_{γ(T ∘f)} for f : A → U, referring to the arguments of the functor, and the other parts are again defined accordingly.

The introduction rules for U_{γ} and equality rules for T_{γ} express that with

eq_{γ} := (x)ref : T_{γ} ∘ intro_{γ} =_{𝔽 _{γ}^{U}(U_{γ},T_{γ})→D}^{fun} 𝔽 _{γ}^{T}(U_{γ}, T_{γ})

⟨U_{γ}, T_{γ}, intro_{γ}, eq_{γ}⟩ is an 𝔽_{γ}-algebra:

Definition 4.1.4 An 𝔽_{γ}-algebra is a quadruple ⟨U, T, f_{0}, f_{1}⟩, s.t.

U : type ,  T : U → D ,
f_{0} : 𝔽 _{γ}^{U}(U, T) → U , f_{1} : T ∘ f_{0} =_{𝔽 _{γ}^{U}(U,T)→D}^{fun} 𝔽 _{γ}^{T}(U, T) ,

as expressed by the diagram

𝔽 _{γ}^{U}(U, T)  \overline{f_{0}} U

[figure: 𝔽 _{γ}^{T}(U, T); f_{1}; T]

D

In the following we will define the rules expressing that ⟨U_{γ}, T_{γ}, intro_{γ}, eq_{γ}⟩ is an initial algebra and show that these rules are extensionally equivalent to the standard elimination and equality rules for U_{γ} and T_{γ}.

4.2 Rules for Initial Algebras in Slice Categories

We presuppose in this subsection the rules of extensionality, formation/introduction rules for OP and for U, T (which express that ⟨U_{γ}, T_{γ}, intro_{γ}, eq_{γ}⟩ is an 𝔽_{γ}-algebra), and the rules for 𝔽^{→}.

Initiality of ⟨U_{γ}, T_{γ}, intro_{γ}, eq_{γ}⟩ means that for any other 𝔽_{γ}-algebra ⟨U′, T′, f_{0}, f_{1}⟩ there is a unique mediating arrow ⟨h_{0}, h_{1}⟩, such that the following diagram commutes:

𝔽 _{γ}^{U}(U_{γ}, T_{γ})  \overline{^{intro_{γ}}} U_{γ}

[figure: 𝔽 _{γ}^{T}(U_{γ}, T_{γ}); eq_{γ}; T_{γ}]

(x)ref  D  h_{1}  (∗)

[figure: 𝔽 _{γ}^{T}(U′, T′); f_{1}; T′]

[figure: 𝔽 _{γ}^{U}(U′, T′); 𝔽 \overrightarrow{γ}(h_{0}, h_{1}); f_{0}; U′; h_{0}]

The rules are (under additional assumption γ : OP_{D})

\frac{U′ : type T′ : U′ → D f_{0} : 𝔽 _{γ}^{U}(U′, T′) → U′ f_{1} : T′ ∘ f_{0} =_{𝔽 _{γ}^{U}(U′,T′)→D}^{fun} 𝔽 _{γ}^{T}(U′, T′)}{initmap_{γ}(U′, T′, f_{0}, f_{1}) : U_{γ} → U′}

and, under the assumptions of the last rule,

T′ ∘ initmap_{γ}(U′, T′, f_{0}, f_{1}) = T_{γ} : U_{γ} → D

initmap_{γ}(U′, T′, f_{0}, f_{1}) ∘ intro_{γ}= f_{0} ∘ 𝔽 \overrightarrow{γ}(initmap_{γ}(U′, T′, f_{0}, f_{1}), (x)ref)
: 𝔽 _{γ}^{U}(U_{γ}, T_{γ}) → U′

\frac{h′_{0} : U_{γ} → U′ h′_{1} : T′ ∘ h′_{0} =_{U_{γ}→D}^{fun} T_{γ} q : h′_{0} ∘ intro_{γ} =_{𝔽 _{γ}^{U}(U_{γ},T_{γ})→U′}^{fun} f_{0} ∘ 𝔽 \overrightarrow{γ}(h′_{0}, h′_{1})}{initmap_{γ}(U′, T′, f_{0}, f_{1}) = h′_{0} : U_{γ} → U′}

Definition 4.2.1 The theory IR_{init}^{ext} is the extension of the logical framework by the formation/introduction rules for OP and for U, T, the rules of extensionality, the rules for 𝔽^{→} and the rules mentioned in this subsection.

4.3 Elimination Rules for OP

In Subsection 4.4 we will show that the elimination rules of U, T are equivalent to the rules for the same sets as an initial algebra. This will be shown by induction on γ : OP_{D} and we need therefore to add elimination and equality rules for OP.

Definition 4.3.1 The elimination and equality rules for OP are the following:

\frac{γ_{0} : OP_{D} γ : OP_{D} ⇒ E[γ] : type a : (ψ : D) → E[ι(ψ)] b : (A : stype, γ : A → OP_{D}, f : (x : A) → E[γ(x)]) → E[σ(A, γ)] c : (A : stype, γ : (A → D) → OP_{D}, f : (x : A → D) → E[γ(x)]) → E[δ(A, γ)]}{R_{D,E}^{OP}(γ_{0}, a, b, c) : E[γ]}

R_{D,E}^{OP}(ι(ψ), a, b, c) = a(ψ) ,
R_{D,E}^{OP}(σ(A, γ), a, b, c) = b(A, γ, (y)R_{D,E}^{OP}(γ(y), a, b, c)) ,
R_{D,E}^{OP}(δ(A, γ), a, b, c) = c(A, γ, (y)R_{D,E}^{OP}(γ(y), a, b, c)) .

We call these rules OP_{elim}. They presuppose the formation/introduction rules for OP.

4.4 Equivalence of the Elimination Principle and the Existence of Initial Algebras

We shall show that the two theories IR_{elim}^{ext} and IR_{init}^{ext} are equivalent under the assumption OP_{elim} by interpreting them in each other. See the diagram at the end of Sect. 5.3, p. 30 for a summary of the relationships.

Theorem 4.4.1 IR_{init}^{ext} can be interpreted in IR_{elim}^{ext} + OP_{elim}.

Remark 4.4.2 More precisely, Theorem 4.4.1 means that we can translate each symbol in the language of IR_{init}^{ext} to a term in the language of IR_{elim}^{ext} + OP_{elim}, such that each translated rule in IR_{init}^{ext} is provable in IR_{elim}^{ext} + OP_{elim}, that is, if the translated premises of the rule are provable so is the translated conclusion.

This translation can be extended by additional symbols and rules.

Proof: We work in IR_{elim}^{ext} extended with OP-elimination and construct the family of functors 𝔽_{γ} and initial algebras ⟨U_{γ}, T_{γ}, intro_{γ}, eq_{γ}⟩ for γ : OP_{D}. First the extensions of 𝔽 _{γ}^{U} and 𝔽 _{γ}^{T} to U : type and 𝔽 \overrightarrow{γ} can be defined by straightforward induction on γ such that the rules for 𝔽^{U}, 𝔽^{T} and 𝔽^{→} hold.

We are going to show that ⟨U_{γ}, T_{γ}, intro_{γ}, eq_{γ}⟩ is an initial 𝔽_{γ}-algebra for γ : OP_{D}. So let γ : OP_{D}, ⟨U′, T′, f_{0}, f_{1}⟩ be another 𝔽_{γ}-algebra, and construct a unique mediating arrow h = ⟨h_{0}, h_{1}⟩, such that diagram (∗) on page 17 commutes. To this end we shall use the elimination rule for U_{γ} with

E[u] := (u′ : U′) × (T′(u′) =_{D} T_{γ}(u))

for u : U_{γ}. To this end define locally by induction on γ′ : OP_{D}:

k_{γ′} : ((u : 𝔽 _{γ′}^{U}(U_{γ}, T_{γ})) × 𝔽 _{γ′}^{IH}(U_{γ}, T_{γ}, E, u)) → 𝔽 _{γ′}^{U}(U′, T′) ,
k_{ι(ψ)}(⟨∗, ∗⟩) = ∗ ,
k_{σ(A,γ′)}(⟨⟨a, b⟩, c⟩) = ⟨a, k_{γ′(a)}(⟨b, c⟩)⟩ ,
k_{δ(A,γ′)}(⟨⟨f′, b⟩, ⟨g′, c⟩⟩) = ⟨π_{0} ∘ g′, k_{γ′(T_{γ}∘f′)}(⟨b, c⟩)⟩ .

In the last equality we use that T′ ∘ π_{0} ∘ g′ = T_{γ} ∘ f′ by extensionality and the equality proof π_{1} ∘ g′. Moreover, we can show, by induction on γ′, that k_{γ′} has the property that both triangles in the following diagram commute (h′_{0} : U_{γ} → U′, h′_{1} : T′ ∘ h′_{0} =_{U_{γ}→U′}^{fun} T_{γ}):

𝔽 _{γ′}^{U}(U_{γ}, T_{γ})

[figure: ⟨id, 𝔽 _{γ′}^{map}(U_{γ}, T_{γ}, E, ⟨h′_{0}, h′_{1}⟩^{fun})⟩^{fun}]

[figure: (u : 𝔽 _{γ′}^{U}(U_{γ}, T_{γ})) × 𝔽 _{γ′}^{IH}(U_{γ}, T_{γ}, E, u); k_{γ′}; 𝔽 _{γ′}^{U}(U′, T′); 𝔽 \overrightarrow{γ′}(h′_{0}, h′_{1})]

[figure: 𝔽 _{γ′}^{T}(U_{γ}, T_{γ}) ∘ π_{0}]

D\begin{matrix}𝔽 _{γ′}^{T}(U′, T′) \\  \end{matrix}

Now let

g = (u, v)⟨f_{0}(k_{γ}(⟨u, v⟩)), ref⟩
: (u : 𝔽 _{γ}^{U}(U_{γ}, T_{γ}), 𝔽 _{γ}^{IH}(U_{γ}, T_{γ}, E, u)) → E[intro_{γ}(u)] .

ref has correct type since

T_{γ}(intro_{γ}(u)) = 𝔽 _{γ}^{T}(U_{γ}, T_{γ}, u)  =  𝔽 _{γ}^{T}(U′, T′, k_{γ}(⟨u, v⟩))
{diagram (∗) \atop =} T′(f_{0}(k_{γ}(⟨u, v⟩))) .

Now we can define the two components of the mediating arrow by

h_{0} := π_{0} ∘ R_{γ,E}(g) : U_{γ} → U′ ,
h_{1} := π_{1} ∘ R_{γ,E}(g) : T′ ∘ h_{0} =_{U_{γ}→D}^{fun} T_{γ} .

To show the commutativity of the outer square in the initial algebra diagram we use the equality rule for R_{γ}:

h_{0}(intro_{γ}(u)) = π_{0}(R_{γ,E}(g, intro_{γ}(u)))
= π_{0}(g(u, 𝔽 _{γ}^{map}(U_{γ}, T_{γ}, E, R_{γ,E}(g), u)))
= f_{0}(k_{γ}(⟨u, 𝔽 _{γ}^{map}(U_{γ}, T_{γ}, E, ⟨h_{0}, h_{1}⟩^{fun}, u)⟩))
= f_{0}(𝔽 \overrightarrow{γ}(h_{0}, h_{1}, u)) : U′ .

Finally, to prove uniqueness of h we assume that we have another mediating arrow ⟨h′_{0}, h′_{1}⟩, that is we have h′_{0} : U_{γ} → U′, h′_{1} : T′ ∘ h′_{0} =_{U_{γ}→D}^{fun} T_{γ}, such that h′_{0} ∘ intro_{γ} = f_{0} ∘ 𝔽 \overrightarrow{γ}(h′_{0}, h′_{1}).

Let for u : U_{γ} E′[u] := (h_{0}(u) =_{U′} h′_{0}(u)). By induction γ′ we can prove for all u : 𝔽 _{γ′}^{U}(U_{γ}, T_{γ}) and v : 𝔽 _{γ′}^{IH}(U_{γ}, T_{γ}, E′, u)

𝔽 \overrightarrow{γ′}(h_{0}, h_{1}, u) =_{𝔽 _{γ′}^{U} (U′,T′)} 𝔽 \overrightarrow{γ′}(h′_{0}, h′_{1}, u) .

So if u : 𝔽 _{γ}^{U}(U_{γ}, T_{γ}) and 𝔽 _{γ}^{IH}(U_{γ}, T_{γ}, E′, u) it follows that

h_{0}(intro_{γ}(u)) = f_{0}(𝔽 \overrightarrow{γ}(h_{0}, h_{1}, u)) = f_{0}(𝔽 \overrightarrow{γ}(h′_{0}, h′_{1}, u)) = h′_{0}(intro_{γ}(u)) : U′ .

Hence, by the induction principle it follows that h_{0}(u) =_{U′} h′_{0}(u) for all u : U_{γ}, and thus by extensionality h_{0} = h′_{0} : U_{γ} → U′. Hence, ⟨h_{0}, h_{1}⟩ = ⟨h′_{0}, h′_{1}⟩ as arrows in the slice category.

Theorem 4.4.3 IR_{elim} can be interpreted in IR_{init}^{ext} + OP_{elim}.

Proof: We shall work in IR_{init}^{ext} extended with OP-elimination and show how to define the constants 𝔽^{IH}, 𝔽^{map}, and R, which are specific to IR_{elim}^{ext}, so that their equality rules can be verified.

First, we can define in a straightforward way 𝔽 _{γ}^{IH} and 𝔽 _{γ}^{map} by OP-elimination and verify their equality rules.

We define now R_{γ} (the recursion operator for the inductive-recursive definition of U_{γ} and T_{γ}) and verify the corresponding equality rule. So let E[u] be a type for u : U_{γ} and assume

g : (u : 𝔽 _{γ}^{U}(U_{γ}, T_{γ}), 𝔽 _{γ}^{IH}(U_{γ}, T_{γ}, E, u)) → E[intro_{γ}(u)] .

We will define

R_{γ,E}(g) := π_{1} ∘ h_{0} : (u : U_{γ}) → E[π_{0}(h_{0}(u))] ,

and verify that π_{0}(h_{0}(u)) = u, where ⟨h_{0}, h_{1}⟩ is the unique mediating morphism in the following initial 𝔽_{γ}-algebra diagram:

𝔽 _{γ}^{U}(U_{γ}, T_{γ})  \overline{^{intro_{γ}}} U_{γ}

[figure: 𝔽 _{γ}^{T}(U_{γ}, T_{γ}); eq_{γ}; T_{γ}]

(x)ref  D  h_{1}

[figure: 𝔽 _{γ}^{T}(U_{γ}^{E}, T_{γ}^{E}); T_{γ}^{E}]

𝔽 _{γ}^{U}(U_{γ}^{E}, T_{γ}^{E})

\begin{matrix}𝔽 \overrightarrow{γ}(h_{0}, h_{1}) \\ \end{matrix}

≅ ; ⟨𝔽 \overrightarrow{γ}(π_{0}, (x)ref), j_{γ}⟩^{fun} ;

(u : 𝔽 _{γ}^{U}(U_{γ}, T_{γ})) × 𝔽 _{γ}^{IH}(U_{γ}, T_{γ}, E, u) 𝔽 _{γ}^{T}(U_{γ}, T_{γ}) ∘ π_{0} ⟨intro_{γ} ∘ π_{0}, g′⟩^{fun} U_{γ}^{E}

\begin{matrix}h_{0} \\ \end{matrix}

Here g′ : ((u : 𝔽 _{γ}^{U}(U_{γ}, T_{γ})) × 𝔽 _{γ}^{IH}(U_{γ}, T_{γ}, E, u)) → E[intro_{γ}(u)] is the uncurried version of g, U_{γ}^{E} := (x : U_{γ}) × E[x] and T_{γ}^{E} := T_{γ} ∘ π_{0} : U_{γ}^{E} → D. Furthermore j_{γ′} is defined by induction on γ′ : OP_{D} as follows (this is a local definition):

j_{γ′} : (u : 𝔽 _{γ′}^{U}(U_{γ}^{E}, T_{γ}^{E})) → 𝔽 _{γ′}^{IH}(U_{γ}, T_{γ}, E, 𝔽 \overrightarrow{γ′}(π_{0}, (x)ref, u)) ,
j_{ι(ψ)}(∗) = ∗ ,
j_{σ(A,γ′)}(⟨a, b⟩) = j_{γ′(a)}(b) ,
j_{δ(A,γ′)}(⟨f, b⟩) = ⟨π_{1} ∘ f, j_{γ′(T_{γ}∘(π_{0}∘f))}(b)⟩ .

(One can show by induction on γ′ that ⟨𝔽 \overrightarrow{γ′}(π_{0}, (x)ref), j_{γ′}⟩^{fun} is an isomorphism

𝔽 _{γ′}^{U}(U_{γ}^{E}, T_{γ}^{E}) ⟶^{≅} (u : 𝔽 _{γ′}^{U}(U_{γ}, T_{γ})) × 𝔽 _{γ′}^{IH}(U_{γ}, T_{γ}, E, u), but this is not needed in the current proof.) The lower left triangle in the initial algebra diagram commutes, since 𝔽 \overrightarrow{γ}(π_{0}, (x)ref) is an arrow in the slice category and the lower right triangle commutes by T_{γ}^{E} = T_{γ} ∘ π_{0}. Therefore it follows that the two triangles together form an 𝔽_{γ}-algebra, and hence we can construct the unique mediating morphism ⟨h_{0}, h_{1}⟩.

We show π_{0} ∘ h_{0} =_{U_{γ}→U_{γ}}^{fun} id and therefore R_{γ,E}(g) := π_{1} ∘ h_{0} : (u : U_{γ}) → E[u]. The following diagram commutes

𝔽 _{γ}^{U}(U_{γ}, T_{γ})  \overline{^{intro_{γ}}} U_{γ}

𝔽 _{γ}^{U}(U_{γ}^{E}, T_{γ}^{E})

\begin{matrix}𝔽 \overrightarrow{γ}(h_{0}, h_{1}) \\ \end{matrix}

⟨intro_{γ} ∘ π_{0}, g′⟩^{fun} ∘ ⟨𝔽 \overrightarrow{γ}(π_{0}, (x)ref), j_{γ}⟩^{fun} U_{γ}^{E}

\begin{aligned}h_{0} \\ & \end{aligned}

[figure: 𝔽 _{γ}^{U}(U_{γ}, T_{γ}); 𝔽 \overrightarrow{γ}(π_{0}, (x)ref); intro_{γ}; U_{γ}; π_{0}]

and all arrows are arrows in the slice category. So ⟨π_{0}∘h_{0}, (x)ref⟩^{fun} and ⟨id, (x)ref⟩^{fun} are two arrows ⟨h′_{0}, h′_{1}⟩ from ⟨U_{γ}, T_{γ}⟩ to itself in the slice category such that h′_{0} ∘ intro_{γ} = intro_{γ} ∘ 𝔽 \overrightarrow{γ}(h′_{0}, h′_{1}). Uniqueness of the arrows from an initial algebra implies now π_{0} ∘ h_{0} = id, the assertion.

Finally, we show that the equality rules hold with the above interpretation:

R_{γ,E}(g, intro_{γ}(u))
= π_{1}(h_{0}(intro_{γ}(u)))
= g′(⟨(𝔽 \overrightarrow{γ}(π_{0}, (x)ref) ∘ 𝔽 \overrightarrow{γ}(h_{0}, h_{1}))(u), (j_{γ} ∘ 𝔽 \overrightarrow{γ}(h_{0}, h_{1}))(u)⟩)
= g′(⟨𝔽 \overrightarrow{γ}(\underbrace{π_{0} ∘ h_{0}}_{=id}, (x)ref, u), 𝔽 _{γ}^{map}(U_{γ}, T_{γ}, E, π_{1} ∘ h_{0}, u)⟩)
= g′(⟨u, 𝔽 _{γ}^{map}(U_{γ}, T_{γ}, E, R_{γ,E}(g), u)⟩)
= g(u, 𝔽 _{γ}^{map}(U_{γ}, T_{γ}, E, R_{γ,E}(g), u)) ,

where the third equality uses the commutativity of the following diagram (which can be proved by induction on γ′ : OP_{D}):

u : 𝔽 _{γ′}^{U}(U_{γ}, T_{γ})

[figure] 𝔽 _{γ′}^{map}(U_{γ}, T_{γ}, E, π_{1} ∘ h_{0})

[figure: 𝔽 _{γ′}^{U}(U_{γ}^{E}, T_{γ}^{E}); 𝔽 \overrightarrow{γ′}(h_{0}, h_{1}); j_{γ′}; 𝔽 _{γ′}^{IH}(U_{γ}, T_{γ}, E, u)]

4.5 Conclusion

We have seen that in extensional type theory together with the elimination rules for OP, the principle of ⟨U_{γ}, T_{γ}, intro_{γ}, eq_{γ}⟩ being an initial algebra is equivalent to the elimination/equality rules for U_{γ}. In intensional type theory we cannot even express the principle of being an initial algebra, since the arrow part of the functors cannot be defined. However, because of the above mentioned equivalence, the principle of universe elimination can be described as a principle which can be formulated in intensional type theory and in the presence of extensionality expresses the initiality property.

5 Induction-recursion as a Reflection Principle

5.1 Background

When working in the slice category both U_{γ} and T_{γ} become part of the initial algebra and we break the pattern

inductively defined set  initial algebra
recursively defined function initial arrow

The slice algebra approach is an abstraction of the set theoretic semantics of inductiverecursive definitions in terms of inductive definitions. It suggests the view that T_{γ} (and not only U_{γ}) is inductively generated.

From a type-theoretic point of view, however, it is unnatural to view inductiverecursive definitions as special cases of inductive ones. We shall therefore recall an alternative formalization of induction-recursion which maintains the distinctions in the table above. This formalization was previously presented in Dybjer and Setzer [12]. It expresses induction-recursion as a reflection principle: for any type D and any D-operation d of “arity” ϕ, there is a set U′_{ϕ,d} which is closed under d and has decoding function T′_{ϕ,d} : U′_{ϕ,d} → D (we add an accent to U, T, intro, R in the current theory in order to distinguish them from the corresponding constants in IR_{elim}).

Consider again the case of the constructor Σ̂ for the first universe. We can express the fact that Σ̂ reflects (inside U′_{0}) the set-operation Σ by the following diagram:

(a : U′_{0}) × (T′_{0}(a) → U′_{0}) \overline{Σ̂} U′_{0}

[figure: (A : set) × (A → set); ⟨a, b⟩ ↦ ⟨T′_{0}(a), T′_{0} ∘ b⟩; Σ; set; T′_{0}]

We have simply observed that the diagonal arrow in the diagram in Section 3.1 factors through Σ.

The general reflection principle is captured by the following commuting diagram:

arg_{ϕ}(U′_{ϕ,d}, T′_{ϕ,d}) \begin{matrix}intro & {′ \atop ϕ,d} \\  \end{matrix}U′_{ϕ,d}

[figure: Arg_{D,ϕ}; map_{ϕ}(U′_{ϕ,d}, T′_{ϕ,d}); d; D; T′_{ϕ,d}]

Here ϕ is an element of the type SP_{D} of D-arities. It encodes both the domain Arg_{D,ϕ} of d, the domain arg_{ϕ}(U′_{ϕ,d}, T′_{ϕ,d}) of the constructor intro′_{ϕ,d} which reflects d, and also the function map_{ϕ}(U′_{ϕ,d}, T′_{ϕ,d}) which decodes the arguments of intro′_{ϕ,d}.

Note that this relationship with initial algebras is different from the initial algebra diagram in the slice category Type/D discussed in the previous section. There U_{γ}, T_{γ} arose as the carrier of an initial algebra and universe elimination arose as the initial arrow.

In this section we shall show the equivalence between the two formulations. To this end we briefly summarize the formalization in Dybjer and Setzer [12] and refer the reader to that paper for more details and discussion.

5.2 An Alternative Formalization

The first step is to introduce a new type SP_{D}

SP_{D} : type ,

containing codes for arities of D-operations. (The elements of SP_{D} can also be viewed as codes for strictly positive “functors”, hence the name.) SP_{D} has five associated operations (Again we write ϕ instead of D, ϕ in argument position. One exception is Arg_{D,ϕ}, where the equality rules refer to D.)

\frac{ϕ : SP_{D}}{Arg_{D,ϕ} : type}

\frac{ϕ : SP_{D}  U : set  T : U → D}{arg_{ϕ}(U, T) : stype}

\frac{ϕ : SP_{D}  U : set  T : U → D}{map_{ϕ}(U, T) : (arg_{ϕ}(U, T)) → Arg_{D,ϕ}}

\frac{ϕ : SP_{D}  U : set  T : (x : U) → D x : U ⇒ E[x] : type  b : arg_{ϕ}(U, T)}{IH_{ϕ,U,T,E}(b) : type}

\frac{ϕ : SP_{D}  U : set  T : (x : U) → D x : U ⇒ E[x] : type  h : (x : U) → E[x]}{mapIH_{ϕ,U,T,E}(h) : (x : arg_{ϕ}(U, T)) → IH_{ϕ,U,T,E}(x)}

We have the following introduction rules for SP:

nil : SP_{D}

\frac{A stype ϕ : A → SP_{D}}{nonind(A, ϕ) : SP_{D}}

\frac{A stype ϕ : (A → D) → SP_{D}}{ind(A, ϕ) : SP_{D}}

Arg_{D,nil} = 1 ,
Arg_{D,nonind(A,ϕ)} = (x : A) × Arg_{D,ϕ(x)} ,
Arg_{D,ind(A,ϕ)} = (f : A → D) × Arg_{D,ϕ(f)} .
arg_{nil}(U, T) = 1 ,
arg_{nonind(A,ϕ)}(U, T) = (x : A) × (arg_{ϕ(x)}(U, T)) ,
arg_{ind(A,ϕ)}(U, T) = (f : A → U) × (arg_{ϕ(T ∘f)}(U, T)) .
map_{nil}(U, T, ∗) = ∗ ,
map_{nonind(A,ϕ)}(U, T, ⟨a, b⟩) = ⟨a, map_{ϕ(a)}(U, T, b)⟩ ,
map_{ind(A,ϕ)}(U, T, ⟨f, b⟩) = ⟨T ∘ f, map_{ϕ(T ∘f)}(U, T, b)⟩ .
IH_{nil,U,T,E}(∗) = 1 ,
IH_{σ(A,ϕ),U,T,E}(⟨a, b⟩) = IH_{ϕ(a),U,T,E}(b) ,

IH_{δ(A,ϕ),U,T,E}(⟨f, b⟩) = ((y : A) → E[f(y)]) × (IH_{ϕ(T ∘f),U,T,E}(b)) .
mapIH_{nil,U,T,E}(h, ∗) = ∗ ,
mapIH_{σ(A,ϕ),U,T,E}(h, ⟨a, b⟩) = mapIH_{ϕ(a),U,T,E}(h, b) ,
mapIH_{δ(A,ϕ),U,T,E}(h, ⟨f, b⟩) = ⟨h ∘ f, mapIH_{ϕ(T ∘f),U,T,E}(h, b)⟩ .

We are now ready to give the formal rules for U′ and T′. These rules have the common additional premises ϕ : SP_{D} and d : Arg_{D,ϕ} → D:

Formation rules:

U′_{ϕ,d} : set
T′_{ϕ,d} : U′_{ϕ,d} → D

Introduction rule:

\frac{a : arg_{ϕ}(U′_{ϕ,d}, T′_{ϕ,d})}{intro′_{ϕ,d}(a) : U′_{ϕ,d}}

Equality rule for T′:

\frac{a : arg_{ϕ}(U′_{ϕ,d}, T′_{ϕ,d})}{T′_{ϕ,d}(intro′_{ϕ,d}(a)) = d(map_{ϕ}(U′_{ϕ,d}, T′_{ϕ,d}, a))}

Elimination rule:

\frac{e : (x : arg_{ϕ}(U′_{ϕ,d}, T′_{ϕ,d}), IH_{ϕ,U′_{ϕ,d},T′_{ϕ,d},E}(x)) → (E[intro′_{ϕ,d}(x)])}{R′_{ϕ,d,E}(e) : (a : U′_{ϕ,d}) → E[a]}

Equality rule:

R′_{ϕ,d,E}(e, intro′_{ϕ,d}(b)) = e(b, mapIH_{ϕ,U′_{ϕ,d},T′_{ϕ,d},E}(R′_{ϕ,d,E}(e), b)) .

Definition 5.2.1 (a) The theory IR_{refl} consists of the rules above in this subsection.

(b) IR_{refl}^{ext} is the extension of IR_{refl} by the rules of extensionality.

(c) The following are the elimination and equality rules for SP, called SP_{elim} (they presuppose the formation and introduction rules for SP):

\frac{ϕ_{0} : SP_{D} ϕ : SP_{D} ⇒ E[ϕ] : type a : E[nil] b : (A : stype, ϕ : A → SP_{D}, f : (x : A) → E[ϕ(x)]) → E[nonind(A, ϕ)] c : (A : stype, ϕ : (A → D) → SP_{D}, f : (x : A → D) → E[ϕ(x)]) → E[ind(A, ϕ)]}{R_{D,E}^{SP}(ϕ_{0}, a, b, c) : E[ϕ]}

R_{D,E}^{SP}(nil, a, b, c) = a ,
R_{D,E}^{SP}(nonind(A, ϕ), a, b, c) = b(A, ϕ, (y)R_{D,E}^{SP}(ϕ(y), a, b, c)) ,
R_{D,E}^{SP}(ind(A, ϕ), a, b, c) = c(A, ϕ, (y)R_{D,E}^{SP}(ϕ(y), a, b, c)) .

5.3 The Correspondence between IR_{elim} and IR_{refl}

We are going to analyze the correspondence between IR_{elim} and IR_{refl}. See the diagram at the end of this section, p. 30 for a summary of the relationships.

First we show that, in the type theory containing rules of both theories, OP_{elim}, SP_{elim} and extensionality laws, there is a 1-1 correspondence between objects γ : OP_{D} and pairs (ϕ : SP_{D}, d : Arg_{D,ϕ} → D) and that we obtain translations between the associated operations. Then we interpret the theory IR_{elim} in IR_{refl} and IR_{elim} + OP_{elim} in IR_{refl} + SP_{elim} (Theorem 5.3.3), and in a last step interpret, using one additional rule, IR_{refl}^{ext} + SP_{elim} in IR_{elim}^{ext} + OP_{elim} (Theorem 5.3.9). Using the results of [12] the consistency of all theories considered in this article follow (Corollary 5.3.4, Remark 5.3.6).

We start with translations between OP_{D} and (ϕ : SP_{D}) × (Arg_{ϕ} → D):

Definition 5.3.1 We define in a type theory containing formation/introduction/elimination/equality rules for OP and SP

sp_{D} : OP_{D} → SP_{D} ,
d_{D} : (γ : OP_{D}, Arg_{sp(γ)}) → D ,
op_{D} : (ϕ : SP_{D}, d : Arg_{ϕ} → D) → OP_{D} ,

by (we omit the index D in sp, d, op)

sp(ι(ψ)) = nil ,
sp(σ(A, γ)) = nonind(A, sp ∘ γ) ,
sp(δ(A, γ)) = ind(A, sp ∘ γ) ,
d(ι(ψ), ∗) = ψ ,
d(σ(A, γ), ⟨a, b⟩) = d(γ(a), b) ,
d(δ(A, γ), ⟨f, b⟩) = d(γ(f), b) .
op(nil, d) = ι(d(∗)) ,
op(nonind(A, γ), d) = σ(A, (a)op(γ(a), (b)d(⟨a, b⟩))) ,
op(ind(A, γ), d) = δ(A, (f)op(γ(f), (b)d(⟨f, b⟩))) .

Theorem 5.3.2 Assume a type theory including formation/introduction/elimination/equality rules for OP and SP, rules for 𝔽^{U}, 𝔽^{T}, 𝔽^{IH}, 𝔽^{mapIH}, Arg, arg, map, IH, mapIH and extensional equality. Then, with variables chosen of appropriate type, the following holds (we omit in op, sp, d the parameter D):

𝔽 _{γ}^{U}(U, T) = arg_{sp(γ)}(U, T) ,
𝔽 _{γ}^{T}(U, T, a) = d(γ, map_{sp(γ)}(U, T, a)) ,
𝔽 _{γ}^{IH}(U, T, E, a) = IH_{sp(γ),U,T,E}(a) ,
𝔽 _{γ}^{map}(U, T, E, h, a) = mapIH_{sp(γ),U,T,E}(h, a) ;
arg_{ϕ}(U, T) = 𝔽 _{op(ϕ,d)}^{U}(U, T) ,
d(map_{ϕ}(U, T, a)) = 𝔽 _{op(ϕ,d)}^{T}(U, T, a) ,
IH_{ϕ,U,T,E}(u) = 𝔽 _{op(ϕ,d)}^{IH}(U, T, E, u) ,
mapIH_{ϕ,U,T,E}(h, a) = 𝔽 _{op(ϕ,d)}^{map}(U, T, E, h, a) ,
Arg_{D,ϕ} = 𝔽 _{op(ϕ,d)}^{U}(D, id) ,
map_{ϕ} = 𝔽 \overrightarrow{op(ϕ,d)}(T′_{ϕ,d}, (x)ref) ;
op(sp(γ), d(γ)) = γ ,
sp(op(ϕ, d)) = ϕ ,
d(op(ϕ, d)) = d .

The following diagram summarizes the correspondence (γ = op(ϕ, d)):

arg_{ϕ}(U′_{ϕ,d}, T′_{ϕ,d}) = 𝔽 _{γ}^{U}(U′_{ϕ,d}, T′_{ϕ,d}) \overline{^{intro′_{ϕ,d}}} U′_{ϕ,d}

[figure: 𝔽 _{γ}^{T}(U′_{ϕ,d}, T′_{ϕ,d})]

Arg_{D,ϕ} = 𝔽 _{γ}^{U}(D, id)

map_{ϕ}(U′_{ϕ,d}, T′_{ϕ,d}) = 𝔽 \overrightarrow{γ}(T′_{ϕ,d}, (x)ref)

d D

\begin{matrix}T′_{ϕ,d} \\ \end{matrix}

Proof of Theorem 5.3.2: Straightforward induction on OP and SP.

Theorem 5.3.3 (a) IR_{elim} can be interpreted in IR_{refl}.

(b) IR_{elim} + OP_{elim} can be interpreted in IR_{refl} + SP_{elim}.

Note that in Theorem 5.3.3 extensionality is not needed: the constants of IR_{elim} can all be defined in IR_{refl} in such a way that all the equality rules of IR_{elim} are translated into definitional equalities in IR_{refl}.

Corollary 5.3.4 (a) IR_{refl}^{ext} +SP_{elim}, IR_{elim}^{ext} +OP_{elim} and IR_{init}^{ext} +OP_{elim} are consistent.

(b) The same holds with subtheories IR_{refl}, IR_{refl}^{ext}, IR_{refl} + SP_{elim}, IR_{elim}, IR_{elim}^{ext}, IR_{elim} + OP_{elim}, IR_{init}^{ext}.

Proof of the corollary: In [12] we gave a model for IR_{refl}. This model fulfills the extensionality rules (with ref^{∗} := 0, r =_{A} s := {0 | r^{∗} = s^{∗} ∧ s^{∗} ∈ A^{∗}}), and we can easily interpret R^{SP} and verify SP_{elim}. Therefore IR_{refl}^{ext} +SP_{elim} is consistent. By Theorems 4.4.1, 5.3.3 and the fact that the above interpretations hold if one extends the theories by additional rules and constants, the consistency of IR_{elim}^{ext} + OP_{elim} and IR_{init}^{ext} + OP_{elim} follows.

Proof of Theorem 5.3.3: The following list gives an interpretation of all terms in the language of IR_{elim}, which are not in the language of IR_{refl} (this interpretation has to be applied inductively to subterms as well)

OP_{D} ↦ OP_{D}^{∗} := (ϕ : SP_{D}) × (Arg_{ϕ} → D) ,

and with

sp′ := (γ)π_{0}(γ) : OP_{D}^{∗} → SP_{D} ,
d′ := (γ)π_{1}(γ) : (γ : OP_{D}^{∗}, Arg_{sp′(γ)}) → D ,
ι(ψ) ↦ ⟨nil, (x)ψ⟩ ,
σ(A, γ) ↦ ⟨nonind(A, sp′ ∘ γ), d̃⟩ with d̃(⟨x, y⟩) = d′(γ(x), y) ,
δ(A, γ) ↦ ⟨ind(A, sp′ ∘ γ), d̃⟩ with d̃(⟨x, y⟩) = d′(γ(x), y) ,
𝔽 _{γ}^{U}(U, T) ↦ arg_{sp′(γ)}(U, T) ,
𝔽 _{γ}^{T}(U, T, a) ↦ d′(γ, map_{sp′(γ)}(U, T, a) ,
𝔽 _{γ}^{IH}(U, T, E, a) ↦ IH_{sp′(γ),U,T,E}(a) ,
𝔽 _{γ}^{map}(U, T, E, h, a) ↦ mapIH_{sp′(γ),U,T,E}(h, a) ,
U_{γ} ↦ U′_{sp′(γ),d′(γ)} ,
T_{γ}(a) ↦ T′_{sp′(γ),d′(γ)}(a) ,
intro_{γ}(a) ↦ intro′_{sp′(γ),d′(γ)}(a) ,
R_{γ,E}(e) ↦ R′_{sp′(γ),d′(γ),E}(e) .

Further, in part (b) we have, with E′[ϕ] := (d : Arg_{ϕ} → D) → E[⟨ϕ, d⟩] the translation

R_{D,E}^{OP}(γ, a, b, c) ↦ \begin{matrix}R_{D,E′}^{SP}( & sp′(γ), \\ (d) & a( & d(∗)), \\ (A, ϕ, f, d) & b( & A, \\ (x)⟨ϕ(x), (y)d(⟨x, y⟩)⟩ \\ (x)f(x, (y)d(⟨x, y⟩))), \\ (A, ϕ, f, d) & c( & A, \\ (x)⟨ϕ(x), (y)d(⟨x, y⟩)⟩ \\ (x)f(x, (y)d(⟨x, y⟩)))) \\ (d′(γ)) \end{matrix}

One easily verifies that with this interpretation the rules of IR_{elim} and IR_{elim} + OP_{elim} hold in IR_{refl}, IR_{refl} + SP_{elim} respectively.

We are now going to study the interpretation of IR_{refl} in IR_{elim}. We will need additionally OP_{elim}, extensionality and the following rules:

Definition 5.3.5 (a) Let Case_{2}^{type} be the following rules, expressing case distinction for 2 into type:

\frac{a : 2  A : type  B : type}{case_{2}^{type}(a, A, B) : type}

case_{2}^{type}(∗_{0}, A, B) = A
case_{2}^{type}(∗_{1}, A, B) = B

(b) Using Case_{2}^{type} we define for A : type, B : type:

• A + B := (x : 2) × case_{2}^{type}(x, A, B) : type.

• For a : A, inl(a) := ⟨∗_{0}, a⟩ : A + B.

• For b : A, inr(b) := ⟨∗_{1}, b⟩ : A + B.

• Using additionally an equality on 2, let for a : A + B isl(a) := (π_{0}(a) =_{2} ∗_{0}) : stype.

Remark 5.3.6 Case_{2}^{type} can be interpreted in the model of [12] in a straightforward way, therefore IR_{refl}^{ext} + SP_{elim} + Case_{2}^{type}, IR_{elim}^{ext} + OP_{elim} + Case_{2}^{type}, IR_{init}^{ext} + OP_{elim} + Case_{2}^{type} are consistent as well.

Further we need the subtree relation on OP_{D}:

Lemma 5.3.7 In IR_{elim}^{ext} + OP_{elim} the following holds under assumption D : type:

(a) We can define for γ : OP_{D}

case_{D}^{OP}(γ) : D + (((A : stype) × (A → OP_{D}))
+ ((A : stype) × ((A → D) → OP_{D}))) ,

such that we can prove

• case_{D}^{OP}(ι(ψ)) = inl(ψ),

• case_{D}^{OP}(σ(A, γ)) = inr(inl(⟨A, γ⟩)),

• case_{D}^{OP}(δ(A, γ)) = inr(inr(⟨A, γ⟩)).

(b) For γ, γ′ : OP_{D} we can define γ′ ⪯_{D} γ : type (expressing “γ′ is a subtree of γ or equal to γ”), such that we can prove • γ′ ⪯_{D} ι(ψ) iff γ′ = ι(ψ),

• γ′ ⪯_{D} σ(A, γ) iff γ′ = σ(A, γ) or γ′ ⪯_{D} γ(a) for some a : A,

• γ′ ⪯_{D} δ(A, γ) iff γ′ = δ(A, γ) or γ′ ⪯_{D} γ(f) for some f : A → D,

• ⪯_{D} is transitive and reflexive.

Definition 5.3.8 In the situation of the last lemma we write ∀γ′ ⪯_{D} γ.E[γ′] for

(γ′ : OP_{D}) → γ′ ⪯_{D} γ → E[γ′] .

Proof of Lemma 5.3.7: (a) case_{D}^{OP}(γ) can be defined by induction on γ. In (b) we cannot simply use elimination rules on γ since for this we need a type to collect γ′ ⪯_{D} γ for all γ : OP_{D}. We define γ′ ⪯_{D} γ iff there exists n : N, f : N_{n+1} → OP_{D}, such that

• f(0_{n+1}) = γ,

• f(n_{n+1}) = γ′,

• if k + 1 < n + 1, then f(k_{n+1}) ≠ ι(ψ) and

– if f(k_{n+1}) = σ(A, γ′′), then f((k + 1)_{n+1}) = γ′′(a) for some a : A, and

– if f(k_{n+1}) = δ(A, γ′′), then f((k + 1)_{n+1}) = γ′′(g) for some g : A → D.

The verification of the properties of ⪯_{D} is now easy.

Theorem 5.3.9 IR_{refl}^{ext}+SP_{elim} can be interpreted in IR_{elim}^{ext}+OP_{elim}+Case_{2}^{type}.

Proof: The main problem is the interpretation of SP. Once this is done and the formation/introduction/elimination/equality rules for SP are verified, we can in a straightforward way define Arg, arg, map, IH, mapIH, op, sp, d and therefore the equations in Theorem 5.3.2 hold. Now interpret U′_{ϕ,d}, T′_{ϕ,d}(a), intro′_{ϕ,d}(a), R′_{ϕ,d,E}(f) as U_{op(ϕ,d)}, T_{op(ϕ,d)}(a), intro_{op(ϕ,d)}(a), R_{op(ϕ,d),E}(f). All rules are then trivially fulfilled and we are done.

We will now interpret SP and verify the rules for it and work in the following in IR_{elim}^{ext} + OP_{elim} + Case_{2}^{type}.

We cannot interpret SP_{D} as OP_{D}. For instance, if D is empty, OP_{D} is empty but SP_{D} is not empty. Instead we will interpret elements of SP_{D} as γ : OP_{D+1}, such that

• for all subtrees of γ of the form ι(ψ) we have ψ = inl(∗), which corresponds to the fact that in SP_{D} leaves do not refer to D,

• all subtrees of γ of the form δ(A, γ′) are such that

γ′(f) = σ((x : A) → isl(f(x)), γ′′(f)) ,

which means that (since all proofs of (x : A) → isl(f(x)) are equal and force f to be equal to inl ∘ f′ for some f′ : A → D) γ′′(f, g) = γ′′′(f′) where f′ : A → D such that f = inl ∘ f′.

However, there will be no direct relationship between the functors on slice categories coded by the corresponding elements in SP_{D} and OP_{D+1}, we use OP_{D+1} only as a type of trees.

So SP_{D} is interpreted as

SP_{D}^{∗} := (γ : OP_{D+1}) × Cor_{D}(γ) ,

and we define

õp := (ϕ)π_{0}(ϕ) : SP_{D}^{∗} → OP_{D+1} ,
cor := (ϕ)π_{1}(ϕ) : (ϕ : SP_{D}^{∗}) → Cor_{D}(õp(ϕ)) ,

where for γ : OP_{D+1}, Cor_{D}(γ) iff for all γ′ ⪯_{D+1} γ:

• if γ′ = ι(ψ), then ψ = inl(∗);

• if γ′ = δ(A, γ′′), then γ′′(f) = σ((x : A) → isl(f(x)), γ′′′) for some γ′′′.

ψ, A, γ′′, γ′′′ can be expressed as terms in γ′ by using case_{D}^{OP}, and therefore Cor_{D}(γ) is built from universal quantifications, implication and conjunction only with the right side of all implications being an equality. By uniqueness of equality proofs follows therefore

for all p, p′ : Cor_{D}(γ) p = p′ .

Further by transitivity of ⪯_{D+1} it follows

Cor_{D}(γ) → ∀γ′ ⪯_{D+1} γ.Cor_{D}(γ′) .

We now interpret

(i) nil as ⟨ι(inr(∗)), p⟩,

(ii) nonind(A, ϕ) as ⟨σ(A, õp ∘ ϕ), q⟩, and

(iii) ind(A, ϕ) as ⟨δ(A, (f)σ((x : A) → isl(f(x)), (g)õp(ϕ(f′)))), r⟩.

Here p, q, r are suitable proofs of Cor_{D}(γ′) for the corresponding γ′ : OP_{D+1} we obtain using in (ii), (iii) cor ∘ ϕ. Further in (iii) f′ : A → D is obtained from f and g such that inl ∘ f′ = f.

By the uniqueness of elements of Cor_{D}(γ) and the uniqueness of proofs of (x : A) → isl(f(x)) it follows:

• If γ : OP_{D} such that Cor_{D}(γ), then

– γ = õp(nil) or

– γ = õp(nonind(A, ϕ)) for some unique A, ϕ or

– γ = õp(ind(A, ϕ)) for some unique A, ϕ.

We can now interpret R^{SP} and verify its rules in the following way.

Assume γ_{0}, E, a, b, c as in the premise of the elimination rule for SP_{D}. We show for γ : OP_{D+1},

g(γ) : (p : Cor_{D}(γ), γ′ : OP_{D}, q : γ′ ⪯_{D+1} γ).E[⟨γ′, p′⟩] ,

where g(γ) is defined using OP_{elim} and p′ is a proof of Cor_{D}(γ′) obtained from p and q.

Assume the assertion for immediate subtrees of γ, γ′ ⪯_{D+1} γ. If γ′ is a proper subtree of γ, the assertion follows from the IH. Otherwise γ′ = γ. Then γ′ = õp(nil) or γ′ = õp(nonind(A, ϕ)) or γ′ = õp(ind(A, ϕ)) for some ϕ. In the last two cases we obtain, since for x : A respective x : A → (D + 1), õp(ϕ(x)) is a proper subtree of γ by IH E[ϕ(x)], and therefore in all three cases by the steps a, b, c E[⟨γ′, p⟩].

We now define the interpretation of R^{SP}

R_{D,E}^{SP,∗}(ϕ, a, b, c) := g(õp(ϕ), cor(ϕ), õp(ϕ), r(ϕ)) : E[ϕ] ,

where r(ϕ) : õp(ϕ) ⪯_{D+1} õp(ϕ). Note that from the uniqueness of proofs p : Cor_{D}(γ) it follows that for all p, p′ : Cor_{D}(γ)

R_{D,E}^{SP,∗}(⟨γ, p⟩, a, b, c) = R_{D,E}^{SP,∗}(⟨γ, p′⟩, a, b, c)

.

It remains to verify that the equality rules for SP hold:

• R_{D,E}^{SP,∗}(nil, a, b, c) = a is immediate.

• R_{D,E}^{SP,∗}(nonind(A, ϕ), a, b, c) = b(A, ϕ, h).

• R_{D,E}^{SP,∗}(ind(A, ϕ), a, b, c) = c(A, ϕ, h).

In the last two equations h(x) is a proof of E[ϕ(x)]. It follows that

R_{D,E}^{SP,∗}(ϕ(x), a, b, c) = h(x).

Summary. The following diagram summarizes the relationships between the theories considered above (5.3.9 requires the addition of Case_{2}^{type} to the logical framework):

IR_{refl}^{ext} + SP_{elim}

[figure: IR_{elim}^{ext} + OP_{elim}; 5.3.9, with Case_{2}^{type}; 5.3.3(b); 4.4.3; \underline{4.4.1}; IR_{init}^{ext} + OP_{elim}]

6 The Mahlo Universe

6.1 The Internal Mahlo Universe

In this final section we recall Setzer’s definition of a Mahlo universe [36, 34, 35] in Martin-Löf type theory. In fact, we consider two versions of it, the original “internal” version, and another, to our knowledge yet unpublished “external” one, both of which have been the subject of much discussion during the last few years.

There are several interesting connections between Mahlo notions and induction-recursion. First, the external Mahlo universe is a powerful example of what can be defined by induction-recursion in the current theory IR_{elim}. Secondly, the internal Mahlo universe is a canonical example of a definition which goes beyond induction-recursion as formalized by IR_{elim}. Whereas the external Mahlo universe, as all inductive-recursive definitions in IR_{elim}, has constructors which are strictly positive in the set defined, this is not the case for the internal Mahlo universe.

The second author has determined a lower bound of the proof-theoretic strength of the internal Mahlo universe [36] and shown that its strength is substantially greater than the strength of the type theory known before (with W-type and finitely iterated universes). He will show in Subsection 6.4 how to modify this result to obtain a lower bound of the proof-theoretic strength of the external Mahlo universe, which is only slightly below the strength of the internal Mahlo universe. As a consequence we therefore get a lower bound of the proof-theoretic strength of the theory of inductive-recursive definitions IR_{elim} and its variants IR_{init}^{ext} and IR_{refl}.

The goal of the definition of the Mahlo universe is to find a constructive analogue of a Mahlo cardinal and its recursive analogue, a recursively Mahlo ordinal. We briefly repeat the definitions. A cardinal κ is Mahlo (or more precisely weakly Mahlo) if it is regular and every normal function f : κ → κ has a regular fixed point.

The recursive analogue of a regular cardinal is an admissible, where an ordinal κ is admissible if it is > 0 and for every (set theoretic) Π_{2}-formula φ with parameters in L_{κ} which holds in L_{κ} there exists an α < κ s.t. L_{α} contains the parameters and φ holds in L_{α}. An ordinal is recursively Mahlo if it is > 0 and for every Π_{2}-formula φ (as before with parameters) which holds in L_{κ} there exists an admissible π < κ s.t. φ holds in L_{π}.

Related to the notion of a recursively Mahlo ordinal is the notion of recursively inaccessible: an ordinal is recursively inaccessible if it is admissible and the limit of admissibles. It can easily be seen that a recursively Mahlo ordinal is recursively inaccessible, and that the π mentioned above can always be chosen to be inaccessible. So an ordinal κ is recursively Mahlo, if it is recursively inaccessible and for every Π_{2}-formula φ with parameters which holds in L_{κ} there exists an inaccessible π < κ such that φ holds in L_{π}, and we will take this characterization as a basis for the type-theoretic formulation.

In term models, W-sets correspond to inductive definitions which can be modeled by iterations of a certain operator up to an admissible κ such that the interpretations of the underlying sets are in L_{κ}. A universe is inductively defined and closed under the W-formation and therefore modeled by iterating an operation up to a recursively inaccessible ordinal. Roughly speaking recursively inaccessible ordinals correspond to universes.

A universe V : set with decoding function S : V → set can be seen as the type theoretic analogue of a recursively inaccessible κ, and the type theoretic analogue of a Π_{2}-formula, which holds in L_{κ}, is a function f : Fam(V) → Fam(V). Here Fam(V) := (a : V) × (S(a) → V) are V -indexed families of sets in V. The analogy of the fact that for any Π_{2}-formula there exists a recursively inaccessible closed under it is now that for every function f as above there exists a universe U_{f} closed under f.

So a formulation of the Mahlo principle in type theory is as follows: There exists a universe V which is a set with decoding function S such that for every function f : Fam(V) → Fam(V) there exists a subuniverse U_{f} of V, closed under f and represented in V.

We can simplify this by currying f and splitting it into two functions f, g: Instead of

f : ((a : V) × (S(a) → V)) → ((a : V) × (S(a) → V))

we take

f : (a : V, b : S(a) → V) → V ,
g : (a : V, b : S(a) → V, S(f(a, b))) → V .

The precise formalization of the Mahlo principle in type theory is now as follows:

First of all V : set , S : V → set ,

and V, S is closed under the standard universe constructions.

Assume now f, g as before. Then the Mahlo principle claims that we have a subuniverse U_{fg}, T̂_{fg} of V, S closed under f and g and represented in V. So we have

U_{fg} : set ,  T̂_{fg} : U_{fg} → V ,

and define for a : U_{fg}

T_{fg}(a) := S(T̂_{fg}(a)) : set .

For the standard constructors of V, like

N̂ : V ,
S(N̂) = N ,
Π̂ : (a : V, b : S(a) → V) → V ,
S(Π̂(a, b)) = Π(S(a), S ∘ b) ,

we claim the existence of codes in U_{fg}, reflecting them, i.e.

N̂_{fg} : U_{fg} ,
T̂_{fg}(N̂_{fg}) = N̂ ,
Π̂_{fg} : (a : U_{fg}, b : T_{fg}(a) → U_{fg}) → U_{fg} ,
T̂_{fg}(Π̂_{fg}(a, b)) = Π̂(T̂_{fg}(a), T̂_{fg} ∘ b) .

Further Û_{fg} is closed under f and g, i.e. we have constructors

f̂_{fg} : (a : U_{fg}, b : T_{fg}(a) → U_{fg}) → U_{fg} ,
T̂_{fg}(f̂_{fg}(a, b)) = f(T̂_{fg}(a), T̂_{fg} ∘ b) ;
ĝ_{fg} : (a : U_{fg}, b : T_{fg}(a) → U_{fg}, c : S(f(T̂_{fg}(a), T̂_{fg} ∘ b)))
→ U_{fg} ,
T̂_{fg}(ĝ_{fg}(a, b, c)) = g(T̂_{fg}(a), T̂_{fg} ∘ b, c) ;

and U_{fg} is represented in V, i.e.

Û_{fg} : V , S(Û_{fg}) = U_{fg} .

U_{fg}, T̂_{fg} are inductive-recursively defined: They can be defined as

U_{fg} = U′(V, S, f, g, N̂, Π̂, …),  T̂_{fg} = T′(V, S, f, g, N̂, Π̂, …) ,

(“…” stands for other universe constructions) where for V : set, S : V → set, f : (x : V, y : S(x) → V) → V, g : (x : V, y : S(x) → V, S(f(x, y))) → V, a : V, b : (x : V, y : S(x) → V) → V etc.

U′(V, S, f, g, a, b, …) : set, T′(V, S, f, g, a, b, …) : U′(V, S, f, g, a, b, …) → V

can be defined by an inductive-recursive definition. However, V itself has apart from the standard constructors, which are strictly positive in V, also one constructor, which is not at all positive in it, namely

Û : (f : (a : V, b : S(a) → V) → V,
g : (a : V, b : S(a) → V, S(f(a, b))) → V) → V .

Therefore V definitely goes beyond induction-recursion as discussed in this article.

We call the above construction internal universe, since V is an element of set, in contrast to the construction in Section 6.3, where the Mahlo-universe is not an element of set, but set itself.

6.2 Simplification of U_{fg}

In the above definition we demanded U_{fg} to be closed under all standard universe construction. However these can be coded into suitable functions f, g typed as above.

Assume f, g as above. Define functions f′, g′ of the same type by

f′(a, b) = N_{1} + N + (S(a) × S(a)) + (S(a) × S(a))
+N_{3} + N_{1} + S(f(a, b)) .

and, if we call the i-th injection into this disjoint union i_{i}, then

g′(a, b, i_{0}(0_{1})) = N̂ ,  g′(a, b, i_{1}(k)) = N̂_{k} ,
g′(a, b, i_{2}(⟨c, d⟩)) = Î(a, c, d) , g′(a, b, i_{3}(⟨c, d⟩)) = b(c)ˆ+b(d) ,
g′(a, b, i_{4}(0_{3})) = Π̂(a, b) ,  g′(a, b, i_{4}(1_{3})) = Σ̂(a, b) ,
g′(a, b, i_{4}(2_{3})) = Ŵ(a, b) ,  g′(a, b, i_{5}(0_{1})) = f(a, b) ,
g′(a, b, i_{6}(c)) = g(a, b, c) .

A non-empty sub-collection of sets of V, i.e. U : set, T : U → V, which is closed under f′, g′, but not necessarily under the standard universe constructions, has representatives for all universe constructions and for f, g relativized to it, so it is essentially a subuniverse closed under f, g. So we can omit the closure of U_{fg} under universe constructions, except of one constant in order to obtain U_{fg} nonempty, and still have a universe which is sufficiently closed. The canonical choice for the constant would be N̂. Alternatively one could add additional parameters a : V, b : S(a) → V to f, g and demand that U_{abfg} contains additionally codes for a and b(x) (x : S(a)). Then closure under N̂ is not needed. Note however that V has in any case to be closed under the standard universe constructions.

6.3 The External Mahlo Universe

The unproblematic part of the above definition was the definition of U_{fg}. Now, instead of making this definition relative to V, we can make it relative to set as well:

Assume

f : (A : set, B : A → set) → set ,
g : (A : set, B : A → set, f(A, B)) → set .

Then we can define inductive-recursively a universe U_{fg}, T_{fg} closed under the standard universe constructions and under f, g. Again we can restrict the standard universe constructions to one, e.g. N, and have the following constructors of U_{fg}:

N̂ : U_{fg} ,
T_{fg}(N̂) = N ,
f̂ : (a : U_{fg}, b : T_{fg}(a) → U_{fg}) → U_{fg} ,
T_{fg}(f̂_{fg}(a, b)) = f(T_{fg}(a), T_{fg} ∘ b) ,
ĝ : (a : U_{fg}, b : T_{fg}(a) → U_{fg}, c : f(T_{fg}(a), T_{fg} ∘ b)) → U_{fg} ,
T_{fg}(ĝ_{fg}(a, b, c)) = g(T_{fg}(a), T_{fg} ∘ b, c) .

We obtain the following code for U_{fg} in OP_{set}:

γ_{U_{fg}} = σ(2, (x)case_{2}(x, ι(N) ,
σ(2, (x)case_{2}(x, δ(1, (A)δ(A(∗), (B)ι(f(A(1), B))) ,
δ(1, (A)δ(A(∗), (B)σ(f(A(1), B)), (C)g(A(1), B, C)))))))) .

This is a nice example, which demonstrates how easy it is to verify that something is an inductive-recursive definition: one just has to find a code for it in OP_{D}. Note that we got inductive-recursive definitions relative to parameters for free: assuming f, g as above we can derive elements of OP_{D} and the corresponding sets and decoding functions, like U_{fg} and T_{fg} above, will depend on these parameters.

We call the above construction, in which set plays the role of a Mahlo-universe (although set can be closed under other constructions as well), and which is subsumed by inductive-recursive definitions, the external Mahlo universe construction.

6.4 The Strength of the External Mahlo Universe

In [36] the second author showed that the strength of the internal Mahlo universe is at least as strong as the extension of Rathjen’s Kripke-Platek set theory for recursively Mahloness, KPM [28] by ω admissibles above a recursively Mahlo ordinal, KPM^{+}. [34] shows that this bound is sharp. The following theorem provides a lower bound for the strength of the external Mahlo universe. It is due to the second author.

Theorem 6.4.1 (Setzer). Let T be the type theory having standard type constructions including the W-type, all with elimination rules into all types, and rules for the universes U_{fg}, T_{fg} as above for every f, g of the above mentioned type (but no elimination rules for U_{fg} or other universes). The strength of T is at least that of KPM.

Roughly speaking, T as in the Theorem above can be called the type theory with the external Mahlo universe and full elimination rules

Corollary 6.4.2 IR_{elim}^{ext}, IR_{init}^{ext} have at least the strength of KPM.

Proof of Corollary 6.4.2. The external Mahlo universe is an instance of inductive-recursive definitions.

Proof of Theorem 6.4.1. We will show how to adapt the well-ordering proofs [36] for the internal Mahlo universe to its external variant. In a future article, the second author will give an alternative proof. There he will extend ordinal systems to recursively Mahlo ordinals, and obtain simpler and more perspicuous well-ordering proofs.

Most definitions, lemmata, theorems and proofs in [36] can be carried over directly to the external Mahlo universe, if we replace V everywhere by set. Especially P(N) becomes the type N → set, and we can for A : P(N) define M(A), W(A) : P(N), Ag(A) : type. W can be defined as a class, i.e. we can define a predicate W(a) s.t.

a : N ⇒ W(a) : type

by

W(a) := (A : P(A)) × Ag(A) × A(a) .

The only exception, where we can no longer carry over proofs from the internal Mahlo universe, is from the last part of Lemma 5.11 (b) onwards, because there we used W(W), which cannot be defined, since we are not allowed to define Wx : A.B for types A, B.

Instead we argue as follows. First we have transfinite induction over W, for if we have

∀x ∈ W.(∀y ≺ x.y ∈ W → φ(y)) → φ(x) ,

then, for every distinguished set A we have by A ⊑ W

∀x ∈ A.(∀y ≺ x.y ∈ A → φ(y)) → φ(x) ,

and by transfinite induction over A therefore ∀x ∈ A.φ(x). Since every element of W is in some distinguished set, it follows ∀x ∈ W.φ(x).

Next we define W′_{i} by:

W′_{0} := (W ∩ M) ∪ {M} ,
W′_{i+1} := {ω^{α_{1}} + ⋯ + ω^{α_{n}} | α_{i} ∈ W′_{i}} ,

which can be defined as classes. We have transfinite induction over W′_{0} and then by Gentzen’s trick (transfinite induction over ordinals built by Cantor normal form reduces to transfinite induction over the underlying ordinals) and Meta-induction on i we can show transfinite induction over W′_{i}.

Since W is closed under Cantor normal form, it follows W′_{i} ∩ M ≅ W ∩ M. Next we can show for (Meta-) all i ∈ N:

∀y ∈ W′_{i}.∀κ ∈ W′_{0} ∩ R.{y, κ} ⊆ C_{κ}(y) → ψ_{κ}(y) ∈ W . (+)

This is done by induction on y. Assume y and the IH. We show

C^{ψ_{κ}(y)}(W) ∩ C_{κ}(y) ∩ ω_{i}(M + 1) ⊆ W′_{i} ,

where ω_{0}(α) := α, ω_{n+1}(α) := ω^{ω_{n}(α)}.

This can be shown as in the proof of Lemma 5.2 (c), assertion (∗) with A replaced by W, W(A) replaced by W′_{i}, τ^{+} replaced by ω_{i}(M + 1) throughout in the proof.

Now it follows

C^{ψ_{κ}y}(W) ∩ ψ_{κ}y ⊆ W′_{i} ∩ M ⊆ W .

If y ≺ ψ̃_{κ}y, then

y ∈ W′_{i} ∩ ψ̃_{κ}y ≅ W ∩ ψ̃_{κ}y ⊆ C^{ψ_{κ}y}(W) ,

Otherwise y ∈ M(W′_{i}) ≅ M(W), y ∈ C^{y}(W) ⊆ C^{ψ_{κ}y}(W). Further κ ∈ W′_{0}, κ ∈ M(W), κ ∈ C^{κ}(W) ⊆ C^{ψ_{κ}y}(W). It follows ψ_{κ}y ∈ C^{ψ_{κ}y}(W). Now we have ψ_{κ}y ∈ M(W), τ^{W}(ψ_{κ}y) ≅ C^{ψ_{κ}y}(W) ∩ ψ_{κ}y ⊆ W′_{i} ∩ M ≅ W, ψ_{κ}y ∈ A^{W}(W) ∩ M ⊆ W, and (+) is shown.

Now ω_{n}(M + 1) ∈ W′_{n+1}, Ω_{1} ∈ W, Ω_{1}, ω_{n}(M + 1) ∈ C_{Ω_{1}}(ω_{n}(M + 1)), therefore by (+)

ψ_{Ω_{1}}(ω_{n}(M + 1)) ∈ W ∩ Ω_{1} ⊑ OT ,

and from transfinite induction over W follows transfinite induction up to ψ_{Ω_{1}}(ω_{n}(M + 1)) for n ∈ ω, which in the limit reaches ψ_{Ω_{1}}(ϵ_{M+1}). Rathjen determined the strength of KPM in [27, 28, 29]. The ordinal notation systems we used is based on [3], where it is shown that the strength of KPM is at most ψ_{Ω_{1}}(ϵ_{M+1}) (which can be seen to be sharp as in [29] or by taking the above proof and adapting it to KPM). Therefore the assertion of the theorem follows.

A Complete Rules of the Logical Framework

In this article we omit in general additional contexts in rules. So for n ≥ 1 a rule

\frac{Δ_{1} ⇒ θ_{1}  ⋯  Δ_{n} ⇒ θ_{n}}{Δ ⇒ θ}

stands for

\frac{Γ, Δ_{1} ⇒ θ_{1}  ⋯  Γ, Δ_{n} ⇒ θ_{n}}{Γ, Δ ⇒ θ}

and a rule without premises Δ ⇒ θ stands for \frac{Γ context}{Γ, Δ ⇒ θ} The only exception are the context and assumption rules.

Context- and Assumption-rules

∅ context  \frac{Γ context  Γ ⇒ A : type}{Γ, x : A context}

\frac{Γ context Γ ⇒ A : type}{Γ, x : A ⇒ x : A} \frac{Γ ⇒ x : A Γ ⇒ B : type}{Γ, y : B ⇒ x : A}

(if x ≠ y, y ∉ FV(A))

Equality Rules

\frac{a : A}{a = a : A}  \frac{A : type}{A = A : type}
\frac{a = b : A}{b = a : A}  \frac{A = B : type}{B = A : type}
\frac{a = b : A  b = c : A}{a = c : A}  \frac{A = B : type  B = C : type}{A = C : type}
\frac{a : A  A = B : type}{a : B}  \frac{a = b : A  A = B : type}{a = b : B}

Rules for →

\frac{A : stype  x : A ⇒ B : stype}{(x : A) → B : stype}  \frac{x : A ⇒ B : type}{(x : A) → B : type}

\frac{A = A′ : stype x : A ⇒ B = B′ : stype}{(x : A) → B = (x : A′) → B′ : stype}

\frac{A = A′ : type x : A ⇒ B = B′ : type}{(x : A) → B = (x : A′) → B′ : type}

\frac{x : A ⇒ t : B}{(x : A)t : (x : A) → B}

\frac{x : A ⇒ t = t′ : B}{(x : A)t = (x : A)t′ : (x : A) → B}

\frac{x : A ⇒ B : type  t : (x : A) → B  s : A}{t(s) : B[x := s]}
\frac{x : A ⇒ B : type  t = t′ : (x : A) → B  s = s′ : A}{t(s) = t′(s′) : B[x := s]}

\frac{x : A ⇒ r : B s : A}{((x : A)r)(s) = r[x := s] : B[x := s]}

\frac{x : A ⇒ B : type s : (x : A) → B}{s = (x : A)s(x) : (x : A) → B}

Rules for ×

\frac{A : stype  x : A ⇒ B : stype}{(x : A) × B : stype}  \frac{x : A ⇒ B : type}{(x : A) × B : type}

\frac{A = A′ : stype x : A ⇒ B = B′ : stype}{(x : A) × B = (x : A′) × B′ : stype}

\frac{A = A′ : type x : A ⇒ B = B′ : type}{(x : A) × B = (x : A′) × B′ : type}

\frac{r : A  s : B[x := r]  x : A ⇒ B : type}{⟨r, s⟩ : (x : A) × B}

\frac{r = r′ : A  s = s′ : B[x := r]  x : A ⇒ B : type}{⟨r, s⟩ = ⟨r′, s′⟩ : (x : A) × B}

\frac{x : A ⇒ B : type r : (x : A) × B}{π_{0}(r) : A}

\frac{x : A ⇒ B : type r = r′ : (x : A) × B}{π_{0}(r) = π_{0}(r′) : A}

\frac{x : A ⇒ B : type r : (x : A) × B}{π_{1}(r) : B[x := π_{0}(r)]}

\frac{x : A ⇒ B : type r = r′ : (x : A) × B}{π_{1}(r) = π_{1}(r′) : B[x := π_{0}(r)]}

\frac{r : A  s : B[x := r]  x : A ⇒ B : type}{π_{0}(⟨r, s⟩) = r : A}

\frac{r : A  s : B[x := r]  x : A ⇒ B : type}{π_{1}(⟨r, s⟩) = s : B[x := r]}

\frac{x : A ⇒ B : type r : (x : A) × B}{r = ⟨π_{0}(r), π_{1}(r)⟩ : (x : A) × B}

In the paper we have the following general assumption about equality versions of rules, omitting types in equality judgements and about bracket notations like E[t]:

General assumption A.0.3 (a) In the following all rules are understood to be supplemented by additional equality rules. For instance the rule

\frac{(x : A) ⇒ B : type}{(x : A) → B : type}

should be supplemented by

\frac{A = A′ : type (x : A) ⇒ B = B′ : type}{(x : A) → B = (x : A′) → B′ : type}

and the rule

\frac{(x : A) ⇒ b : B}{(x : A)b : (x : A) → B}

should be supplemented by

\frac{(x : A) ⇒ b = b′ : B}{(x : A)b = (x : A)b′ : (x : A) → B}

(b) We will usually omit the type in an equality judgement and assumptions about the types of the variables in it, it they can easily be filled in by the reader.

(c) We follow a common convention and write E[x] for an expression which may depend on a free variable x. After the first occurrence of it, E[t] denotes the result of substituting the term t for the variable x in E[x]. Further, after such an occurrence, E not followed by a square bracket stands for (x)E[x]. The latter will be used to denote parameters only.

B Derivation of Ex Falsum Quodlibet for N′_{0}

We verify that we can define ex falsum quodlibet for N′_{0} defined by γ := σ(1, (f)ι_{∗}):

Let N′_{0} := U_{γ}, T′ := T_{γ}. Assume x : N′_{0} ⇒ E[x] : type. We show that there exists f : (x : N′_{0}) → E[x].

Define E′ := (x : N′_{0}) → E[x], E′′[y] := E′. Definitionally we have

𝔽 _{γ}^{IH}(N′_{0}, T′, E′′, u) = 𝔽 _{γ}^{IH}(N′_{0}, T′, E′′, ⟨π_{0}(u), π_{1}(u)⟩)
= ((x : 1) → E′′[π_{0}(u)]) × 𝔽 _{ι_{∗}}^{IH}(N′_{0}, T′, E′′, π_{1}(u))
= (1 → E′) × 1 .

The argument of R_{γ,E′′} has type

(u : 𝔽 _{γ}^{U}(N′_{0}, T′), 𝔽 _{γ}^{IH}(N′_{0}, T′, E′′, u)) → E′′[intro_{γ}(u)]
= 𝔽 _{γ}^{U}(N′_{0}, T′) → ((1 → E′) × 1) → E′ .

g := (u, v)π_{0}(v)(∗) has this type. Therefore g′ := R_{γ,E′′}(g) : N′_{0} → (x : N′_{0}) → E′[x]. Define f := (x)g′(x, x).

References

[1] P. Aczel. Frege structures and the notions of proposition, truth, and set. In J. Barwise, H. J. Keisler, and K. Kunen, editors, The Kleene Symposium, pages 31–59. North-Holland, 1980.

[2] S. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Department of Computer Science, Cornell University, 1987.

[3] W. Buchholz. A note on the ordinal analysis of KP M. In J. Oikkonen and J. Väänänen, editors, Logic Colloquium ’90, ASL Summer Meeting Helsinki, volume 2 of Springer Lecture Notes in Logic, pages 1 – 9, 1993.

[4] J. Cartmell. Generalized algebraic theories and contextual categories. Annals of Pure and Applied Logic, 32:209–243, 1986.

[5] C. Coquand. The Agda homepage, February 2000.

http://www.cs.chalmers.se/~catarina/agda/.

[6] T. Coquand and C. Paulin. Inductively defined types, preliminary version. In LNCS 417, COLOG ’88, International Conference on Computer Logic. Springer-Verlag, 1990.

[7] P. Dybjer. Inductive sets and families in Martin-Löf’s type theory and their settheoretic semantics. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 280–306. Cambridge University Press, 1991.

[8] P. Dybjer. Universes and a general notion of simultaneous inductive-recursive definition in type theory. In B. Nordström, K. Petersson, and G. Plotkin, editors, Proceedings of the 1992 Workshop on Types for Proofs and Programs, 1992.

[9] P. Dybjer. Inductive families. Formal Aspects of Computing, 6:440–465, 1994.

[10] P. Dybjer. Internal type theory. In TYPES ’95, Types for Proofs and Programs, volume 1158 of Lecture Notes in Computer Science, pages 120–134. Springer, 1996.

[11] P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2):525–549, 2000.

[12] P. Dybjer and A. Setzer. A finite axiomatization of inductive-recursive definitions. In J.-Y. Girard, editor, Typed Lambda Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, pages 129–146. Springer, April 1999.

[13] P. Dybjer and A. Setzer. Indexed induction-recursion. In R. Kahle, P. Schroeder-Heister, and R. Stärk, editors, Proof Theory in Computer Science, pages 93 – 113. LNCS 2183, 2001.

[14] M. Hofmann. Syntax and semantics of dependent types. In A. Pitts and P. Dybjer, editors, Semantics and Logics of Computation, pages 79–130. Cambridge University Press, 1997.

[15] J. Lambek and P. J. Scott. Introduction to higher order categorical logic, volume 7 of Cambridge studies in advanced mathematics. Cambridge University Press, 1986.

[16] C. Löfwall and G. Sjödin. Strong normalizability in Martin-Löf’s type theory. Technical Report R91-09, Swedish Institute of Computer Science, 1991.

[17] P. Martin-Löf. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium ‘73, pages 73–118. North-Holland, 1975.

[18] P. Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI, 1979, pages 153–175. North-Holland, 1982.

[19] P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.

[20] P. Martin-Löf. An intuitionistic theoy of types. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory, pages 127–172. Oxford University Press, 1998. Reprinted version of an unpublished report from 1972.

[21] P. F. Mendler. Predicative type universes and primitive recursion. In Proceedings Sixth Annual Synposium on Logic in Computer Science. IEEE Computer Society Press, 1991.

[22] B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’s Type Theory: an Introduction. Oxford University Press, 1990.

[23] E. Palmgren. On Fixed Point Operators, Inductive Definitions and Universes in Martin-Löf’s Type Theory. PhD thesis, Uppsala University, 1991.

[24] E. Palmgren. Type-theoretic interpretation of iterated, strictly positive inductive definitions. Arch. Math. Logic, 32:75–99, 1992.

[25] E. Palmgren. On universes in type theory. In G. Sambin and J. Smith, editors, Twenty five years of constructive type theory, pages 191 – 204, Oxford, 1998. Oxford University Press.

[26] C. Paulin-Mohring. Inductive definitions in the system Coq - rules and properties. In Typed lambda calculi and applications, volume 664 of Lecture Notes in Computer Science, pages 328–245. Springer-Verlag, 1993.

[27] M. Rathjen. Ordinal notations based on a weakly Mahlo cardinal. Arch. Math. Logic, 29:249 – 263, 1990.

[28] M. Rathjen. Proof-theoretical analysis of KPM. Arch. Math. Logic, 30:377 – 403, 1991.

[29] M. Rathjen. Collapsing functions based on recursively large cardinals: A wellordering proof for KPM. Arch. Math. Logic, 33:35–55, 1994.

[30] M. Rathjen, E. R. Griffor, and E. Palmgren. Inaccessibility in constructive set theory and type theory. Annals of Pure and Applied Logic, 94:181 – 200, 1998.

[31] D. S. Scott. Constructive validity. In Symposium on Automatic Demonstration, pages 237–275. Springer Lecture Notes in Mathematics 125, 1970.

[32] R. A. G. Seely. Locally cartesian closed categories and type theory. Proceedings of the Cambridge Philosophical Society, 95:33–48, 1984.

[33] A. Setzer. Proof theoretical strength of Martin-Löf Type Theory with Wtype and one universe. PhD thesis, Fakultät für Mathematik der Ludwig-Maximilians-Universität München, 1993.

[34] A. Setzer. A model for a type theory with Mahlo universe. Draft, available from http://www-compsci.swan.ac.uk/∼csetzer/, 1996.

[35] A. Setzer. A type theory for Mahlo universes. Abstract for Logic Colloquium 95. Bulletin of Symbolic Logic, 3:128 – 129, 1997.

[36] A. Setzer. Extending Martin-Löf type theory by one Mahlo-universe. Arch. Math. Logic, 39:155 – 181, 2000.