Indexed Induction-Recursion

Peter Dybjer^{a,⋆}

aDepartment of Computer Science and Engineering, Chalmers University of Technology, 412 96 Göteborg, Sweden

   Email: peterd@cs.chalmers.se, http://www.cs.chalmers.se/∼peterd/,

Tel: +46 31 772 1035, Fax: +46 31 772 3663.

Anton Setzer^{b,1}

bDepartment of Computer Science, University of Wales Swansea, Singleton Park, Swansea SA2 8PP, UK,

   Email: a.g.setzer@swan.ac.uk, http://www.cs.swan.ac.uk/∼csetzer/,

Tel: +44 1792 513368, Fax: +44 1792 295651.

Abstract

An indexed inductive definition (IID) is a simultaneous inductive definition of an indexed family of sets. An inductive-recursive definition (IRD) is a simultaneous inductive definition of a set and a recursive definition of a function on that set. An indexed inductive-recursive definition (IIRD) is a combination of both.

We present a closed theory which allows us to introduce all IIRD in a natural way without much encoding. By specialising it we also get a closed theory of IID. Our theory of IIRD includes essentially all definitions of sets which occur in Martin-Löf type theory. We show in particular that Martin-Löf’s computability predicates for dependent types and Palmgren’s higher order universes are special kinds of IIRD and thereby clarify why they are constructively acceptable notions.

We give two axiomatisations. The first formalises a principle for introducing meaningful IIRD by using the data-construct in the original version of the proof assistant Agda for Martin-Löf type theory. The second one admits a more general form of introduction rule, including the introduction rule for the intensional identity relation, which is not covered by the first axiomatisation. If we add an extensional identity relation to our logical framework, we show that the theories of restricted and general IIRD are equivalent by interpreting them in each other.

Finally, we show the consistency of our theories by constructing a model in classical set theory extended by a Mahlo cardinal.

Key words: Dependent type theory, Martin-Löf Type Theory, inductive definitions, inductive-recursive definitions, inductive families, initial algebras, normalisation proofs, generic programming.

Preprint submitted to Elsevier Science 14 July 2005

1 Introduction

Martin-Löf type theory is a foundational framework for constructive mathematics. It is also a functional programming language with a powerful type theory. In this theory, induction is one of the two principles for constructing sets; the other is function space formation. For this reason, it has been important to spell out the principles of inductive definability underlying Martin-Löf type theory [11,12]. A similar notion of inductive definability is a core concept of the Calculus of Inductive Constructions [10,28], the impredicative type theory underlying the Coq-system.

Inductive-recursive definitions. Simple inductive definitions and function spaces alone do not suffice to define all sets in Martin-Löf type theory. Consider for example the universe à la Tarski [22]. It consists of a set U of codes for small sets, and a decoding function T, which maps a code to the set it denotes. This definition is simultaneously inductive and recursive: U is inductively generated at the same time as T is defined by recursion on the way the elements of U are generated. To see why they are simultaneously defined we look at the closure of small sets under Σ stating that the disjoint union of a small family of small sets is small. This is expressed by an introduction rule for U: if a : U and b(x) : U for x : T(a), then Σ̂(a, b) : U, that is,

Σ̂ : (a : U) → (T(a) → U) → U

is a constructor for U. Here (x : A) → B is the dependent function space, that is, the set of functions f, which map an element a : A to an element f(a) of B[x := a]. There is also a recursive equation for T:

T(Σ̂(a, b)) = Σx : T(a).T(b(x)).

Observe that the introduction rule for U refers to T, something which is not allowed in an inductive definition. Therefore, T has to be defined simultaneously with U. To capture this we need the more general notion of an inductiverecursive definition [13], where we simultaneously define a set U and a decoding T : U → D into an arbitrary type D.

Other examples of inductive-recursive definitions were known before (larger universes, computability predicates for dependent types), but the new idea [13] was that these are instances of a general notion, equally natural as that of an inductive definition. It is a constructively acceptable notion: its rules can

⋆ Supported by Vetenskapsrådet, grant Typed Lambda Calculus and Applications. 1 Supported by Nuffield Foundation, grant ref. NAL/00303/G and EPSRC grant GR/S30450/01.

be justified by meaning explanations in the sense of Martin-Löf in a similar way as the rules for inductive definitions.

In the original presentation [13] induction-recursion is described as an external schema spelling out criteria for correct formation, introduction, elimination, and equality rules. However, this schema is not fully rigorous and the authors therefore presented a closed axiomatisation of inductive-recursive definitions in Martin-Löf type theory [14,16].

Indexed inductive-recursive definitions. There are many examples (see Section 3) where we want to define a whole family of sets simultaneously, but the previous articles [14,16] only consider the case of an inductive-recursive definition of one set at a time. It is the objective of this paper to extend this to indexed inductive-recursive definitions (IIRD), that is, inductive-recursive definitions of indexed families of sets U(i) and functions T(i) : U(i) → D[i] for i : I, where I is a set and D[i] is an I-indexed family of types. (We must write D[i] rather than D(i), since the typing D : I → type is not expressible in our logical framework. See Section 2 for more information about the notation.)

Our theories for IIRD are the most general existing versions of Martin-Löf type theory. They encompass virtually all sets that have been used in Martin-Löf type theory before, with the exception of some notions of even larger universes (like the Mahlo universe) of proof-theoretic interest considered by the second author [31,32].

Indexed inductive definitions (IID). IID is the principle of defining an indexed family of sets by a simultaneous inductive definition. IID are ubiquitous when using Martin-Löf type theory for formalising mathematics or programming problems.

IID appear as special cases of IIRD where the recursively defined function is degenerate (has codomain 1). Therefore, a side effect of our paper is to provide the first closed axiomatisation of IID.

Several examples of IID can be found in Section 3.1 and of proper IIRD in Section 3.2.

General and restricted IIRD. We consider two classes of indexed inductive-recursive definitions: general IIRD (as in [13]) and restricted IIRD as introduced by T. Coquand for use in the Half and Agda [7] systems. Coquand’s restricted IIRD have not been spelled out in detail in the literature, although they are supported by the Half and Agda systems. To illustrate the difference between restricted and general IIRD, we consider the inductive definition of the even number predicate Even : N → set. As a general IID, it is inductively generated by the two rules

C_{0} : Even(0) ,
C_{1} : (n : N) → Even(n) → Even(S(S(n))) .

As a restricted IIRD, the constructors instead have the following types:

C′_{0} : (m : N) → (m =_{N} 0) → Even(m) ,
C′_{1} : (m : N) → (n : N) → Even(n) → (m =_{N} S(S(n))) → Even(m) ,

where =_{N} is equality of natural numbers. In restricted IIRD, we can determine the constructors (and their arguments) of a particular set U(i) in the family without analysing i. For example, Even(m) has constructors C′_{0}(m) and C′_{1}(m). More formally, the first argument of each constructor is the index of the element introduced by the constructor. In an implementation which allows full recursion (like Agda), we can use case-distinction for one element as elimination principle for restricted IIRD. For instance, an element of Even(m) either has the form C′_{0}(m, p) or the form C′_{1}(m, n, p, q). In Agda, the argument m of the constructor is omitted (instead there is some notation which makes the whole type Even(m) part of the name of the constructor – we omit this here). The notation for case distinction is therefore as follows:

case m of {C′_{0}(p) → ⋯; C′_{1}(n, p, q) → ⋯}

In general IIRD we do not have the above restriction: if C is a constructor of an indexed set U and we apply it to the arguments a⃗, then the index i such that C(a⃗) : U(i) may depend on the arguments a⃗ in an arbitrary way. Case-distinction is no longer possible for one individual element of U(i). For example, in the definition of Even we have to define functions simultaneously for all pairs ⟨n, p⟩ such that n : N and p : Even(n), and we need to use pattern matching in order to distinguish between the cases ⟨n, p⟩ = ⟨0, C_{0}⟩ and ⟨n, p⟩ = ⟨S(S(m)), C_{1}(m, q)⟩.

Martin-Löf’s definition of the equality relation as inductively generated by the reflexivity rule is a key example of a general IID with no corresponding restricted version (unless we assume that the framework already contains an equality =_{A} in which case it would be pointless to introduce a second equality relation).

The proof assistant Alf [19,2] supports the use of general IIRD by using Coquand’s pattern matching with dependent types [9]. Recently, a construct for general IIRD has also been added to Agda.

Generic dependent type theory. Our axiomatisations of IIRD are related to generic programming. In generic functional programming [18,17], generic functions are defined by induction on the code of a data type. Our axiomatisation provides a type of codes for all IIRD, and therefore we can write programs by induction on the codes for IIRD. In this sense, we here provide a “generic dependent type theory”, a version of Martin-Löf type theory with generic formation, introduction, elimination, and equality rules. Benke, Dybjer, and Jansson [5] further develop an approach to generic programs and proofs which is based on ideas from the present paper. Other references to generic programs and proofs in dependent type theory are Pfeifer and Rueß [29] and Altenkirch and McBride [3].

Alternative axiomatisations. We emphasise that our objective is to axiomatise IIRD (and IID) as they are naturally presented in terms of rules for generating new elements of a set. It is thus not only a question of presenting a theory with a certain proof-theoretic strength: we would have reached equal proof-theoretic strength using a version of Martin-Löf type theory with wellorderings and a Mahlo universe. However, working with IIRD in such a theory would require elaborate encodings. Instead, we achieve a close correspondence between our codes for IIRD and the syntax for corresponding definitions in the Agda-system (using the data-construct). The latter can be viewed as a sugared version of the former.

By formalising a concrete theory of IIRD we give a rigorous definition of the concept of IIRD which makes metamathematical analysis possible. For example, in Section 7 we show how to interpret the theories of general and restricted IIRD in each other. In future work we plan to show further reductions of theories axiomatised in this way, for example, we plan to show how to interpret the theory of IIRD in the theory of IRD and the theory of “small” general IIRD in the theory of IID.

When explaining the idea behind our axiomatisations, we use some categorical notions. In particular, we consider algebras of certain endofunctors on the slice category Fam(I)/D, where Fam(I) is the category of I-indexed types (see Subsection 4.1). From the point of view of category theory it would be natural to use two more ideas from categorical semantics: that I-indexed types can be represented as fibrations, and that we expect our algebras to be initial. However, neither of these ideas taken literally gives rise to rules which are close to the usual type-theoretic rules for IIRD. The goal of this paper is to introduce and analyse theories with good intensional properties. The reduction of our theory to initial algebras requires extensional equality. Moreover, even in an extensional setting working directly with initial algebras would add an overhead which may make it impractical for use in proof assistants.

Nevertheless, we use categorical ideas in a limited way and show for example that Fam(I)/D is equivalent to the category Type/((i : I) × D[i]). This equivalence suggests that it is possible to reduce IIRD to IRD (non-indexed inductive-recursive definitions). As already mentioned we plan to show this formally in a future publication, where we also plan to discuss the relationship between IIRD and initial algebras.

2 The Logical Framework

Before giving the rules for IIRD we need to introduce the basic Logical Framework of dependent types. This is essentially Martin-Löf’s Logical Framework [25] extended with rules for dependent product types (x : A) × B and the types 0, 1, and 2. The complete set of rules for the logical framework can be found in Appendix A.1. Note that we will work in intensional type theory, except for Sect. 7 and when explicitly stated.

The Logical Framework has the following forms of judgements: Γ context (where Γ is of the form x_{1} : A_{1}, …, x_{n} : A_{n}); and A : type, A = B : type, a : A, a = b : A, depending on contexts Γ (written as Γ ⇒ A : type, etc.). We have set : type and if A : set, then A : type. The collection of types is closed under the formation of dependent function types written as (x : A) → B. (Πx : A.B is a common alternative notation for this construction, but it is used here for dependent function sets, that is, the inductively defined sets with constructor λ : ((x : A) → B) → (Πx : A.B).) The elements of (x : A) → B are denoted by (x : A)a (abstraction of x in a – this is often denoted by λx : A.a in the literature). Application is written as a(b). We follow Martin-Löf and have ηrules (note that we are working in intensional type theory) as well as β-rules in the logical framework. Types are also closed under the formation of dependent products written as (x : A) × B. (A common alternative notation is Σx : A.B, but this is here used for the inductively defined set with introduction rule p : ((x : A) × B) → (Σx : A.B).) The elements of (x : A) × B are denoted by ⟨a, b⟩, the projection functions by π_{0} and π_{1} and again we have β and η-rule (surjective pairing). There is the type 1, with unique element ⋆ : 1 and η-rule expressing that, if a : 1, then a = ⋆ : 1. Furthermore, we have the empty type 0 with elimination rule case_{0}.

Moreover, in our version of the logical framework we include the type 2 with two elements ⋆_{0} : 2 and ⋆_{1} : 2, ordinary elimination rule case_{2} : (i : 2, A[⋆_{0}], A[⋆_{1}]) → A[i] (where i : 2 ⇒ A[i] : type) and elimination into type, expressed as case_{2}^{type}(i, A, B) : type for i : 2, A : type, B : type. We need elimination into type, since we want to inductively define indexed families of sets U : I → set and functions T : (i : I) → U(i) → D[i] where D[i] depends nontrivially on i, as in the definition of Palmgren’s higher-order universe (where for instance D[0] := set, D[1] := ((X : set) × (X → set)) → ((X : set) × (X → set)), etc; see Subsect. 3.2 for details).

We can now define the disjoint union of two types A + B := (i : 2) × case_{2}^{type}(i, A, B), and prove the usual formation, introduction, elimination and equality rules (see Def. A.2 for details).

We also add a level between set and type, which we call stype for small types: stype : type. (The reason for the need for stype is discussed in [13].) If a : set then a : stype. Moreover, stype is also closed under dependent function types, dependent products and includes 0, 1, 2. However, set itself will not be in stype. The logical framework does not have any rules for introducing elements of set. They will be introduced by IIRD later and set will therefore consist exactly of the sets introduced by IIRD.

In Section 7 and when explicitly stated, we will use the rules of extensional equality (where a =_{A} b is the equality type for a, b : A) which can be found in Appendix A.2. Note that we introduce a =_{A} b for A : type.

We also use some standard abbreviations, see Definition A.1 in Appendix A.1 for a complete list. We just mention the following: We omit the type in an abstraction and write (x)a instead of (x : A)a; we write repeated function spaces as (x_{1} : A_{1}, …, x_{n} : A_{n}) → A instead of (x_{1} : A_{1}) → ⋯ (x_{n} : A_{n}) → A, repeated application as a(b_{1}, …, b_{n}) instead of a(b_{1}) ⋯ (b_{n}). We sometimes put arguments in subscript position and thus also write a_{b_{1},...,b_{n}} for (repeated) application. Repeated abstraction as is written as (x_{1} : A_{1}, …, x_{n} : A_{n})a or (x_{1}, …, x_{n})a instead of (x_{1} : A_{1}) ⋯ (x_{n} : A_{n})a; and we write (−) for the abstraction (x) of a variable x, which is not used later.

In the following, we will sometimes refer to a type depending on a variable x. We want to use the notation D[t] for D[x := t] for some fixed variable x and D for (x)D[x]. Note that we cannot simply introduce D : I → type, since this goes beyond the logical framework. Instead, we introduce the notion of an abstracted expression, which is an expression together with one or several designated free variables. For an abstracted expression E, E[t_{1}, …, t_{n}] means the substitution of the variables by t_{1}, …, t_{n}. If we let D above be an abstracted expression of the form (x)E, then D[t] denotes D[x := t] and we can write D as parameter for (x)E. More formally:

Definition 2.1 (a) An n-times abstracted expression is an expression (x_{1}, …, x_{n})E where x_{1}, …, x_{n} are distinct variables and E an expression of the language of type theory. An abstracted expression is a 1-times abstracted expression.

(b) ((x_{1}, …, x_{n})E)[t_{1}, …, t_{n}] := E[x_{1} := t_{1}, …, x_{n} := t_{n}].

(c) Whenever we write s[a_{1}, …, a_{n}], s is to be understood as an n-times abstracted expression.

(d) If U : A → B, we identify U with the abstracted expression (a)U(a).

3 Some Examples

3.1 Examples of Indexed Inductive Definitions

Trees and forests. Many IID occur as the simultaneous inductive definition of finitely many sets, each of which has a different name. One example is the set of well-founded trees Tree with finite branching degrees, which is defined together with the set Forest of finite lists of such trees. The constructors are:

tree : Forest → Tree ,
nil : Forest ,
cons : Tree → Forest → Forest .

If we instead of Forest and Tree introduce Tree′ : 2 → set and replace Tree by Tree′(⋆_{0}) and Forest by Tree′(⋆_{1}) in the types of tree, nil, cons above, then we obtain an IID with index set 2.

The accessible part of a relation. Let I be a set and <: I → I → set be a binary relation on it. We define the accessible part (the largest well-founded initial segment) of < as a predicate Acc : I → set by a generalised indexed inductive definition with one introduction rule:

acc : (i : I) → ((x : I) → (x < i) → Acc(x)) → Acc(i) .

Note that acc introduces elements of Acc(i) while referring to possibly infinitely many elements of the sets Acc(x) (for each x : I and each proof of x < i).

The identity relation. This is the only example of an IID in Martin-Löf’s original formulation of type theory with a non-trivial index type. For historical reasons it is often referred to as the “intensional identity type” – a more appropriate name would be “identity set”. Assume A : set. The rules for the intensional identity on A express that it is the least reflexive relation on A. The formation rule is I : A → A → set. The introduction rule expresses that it is reflexive:

r : (a : A) → I(A, a, a) .

The elimination rule expresses that the only elements of an identity set are those which are constructed by the introduction rule. So to define a function a : A, b : A, p : I(A, a, b) ⇒ C[a, b, p] it is sufficient to define the step-function s such that for every a : A we have s[a] : C[a, a, r(a)]. Thus the elimination rule states that for every a, b : A and p : I(A, a, b) we have J(A, C, a, b, p, (x)s[x]) : C[a, b, p]. Usually, in Martin-Löf type theory one assumes that C[a, b, p] is a set. However, in this paper the elimination rule is strengthened so that C[a, b, p] can be a type, that is, we have a so called large elimination rule. We will in general consider large elimination rules in this paper.

Context free grammars. IID occur very frequently in applications in computer science. For example a context free grammar over a finite alphabet Σ and a finite set of nonterminals NT is an NT×Σ^{∗}-indexed inductive definition, where each production corresponds to an introduction rule.

As an example, consider the context free grammar with Σ = {a, b}, NT = {A, B} and productions A ⟶ a, A ⟶ BB, B ⟶ AA, B ⟶ b. This corresponds to an inductive definition of a family of sets L indexed over NT × Σ^{∗}, where L(A, α) is the set of derivation trees of the string α from the start symbol A. So α is in the language generated by the grammar with start symbol A iff L(A, α) is inhabited. L has one constructor for each production: C_{0} : L(A, a), C_{1} : L(B, α) → L(B, β) → L(A, α∗β), and C_{2} : L(A, α) → L(A, β) → L(B, α ∗ β), C_{3} : L(B, b), where ∗ denotes concatenation.

Alternatively, we can inductively define an NT-indexed set D of “abstract syntax trees” for the grammar, and then recursively define the string d(A, p) (“concrete syntax”) corresponding to the abstract syntax tree p : D(A). In the example above we get C_{0} : D(A), C_{1} : D(B) → D(B) → D(A), C_{2} : D(A) → D(A) → D(B), C_{3} : D(B). Furthermore, d(A, C_{0}) = a, d(A, C_{1}(p, q)) = d(B, p) ∗ d(B, q), d(B, C_{2}(p, q)) = d(A, p) ∗ d(A, q), d(B, C_{3}) = b.

The simply typed lambda calculus. The traditional way of introducing the simply typed lambda calculus is to first define inductively the set of lambda types Ltype, the set of lambda contexts Lcontext, and the set of “raw” lambda terms Lraw. In typed lambda calculus à la Curry Lraw is just the set of untyped lambda terms, whereas in the typed lambda calculus à la Church the lambda terms have type labels associated with each binding occurrence of a variable. Then we define the typing relation inductively by writing down the typing rules for the simply typed lambda calculus. The typing relation is a ternary relation on Lcontext × Lterm × Ltype.

We here show an alternative approach, which is to directly give an IID of the well-typed terms Lterm(Γ, σ) of type σ in context Γ (see also Altenkirch and Reus [4] and Qiao [30]).

We first define the type Ltype of lambda types, constructed from the basic type o and function types (where ar(σ, τ) denotes the type σ → τ) as a simple inductive definition, having constructors

o : Ltype
ar : Ltype → Ltype → Ltype

We define the type Lcontext of contexts as a list of types:

empty : Lcontext
cons : Lcontext → Ltype → Lcontext

A variable v of type σ in context Γ will be an element of a set Lvar(Γ, σ), which is given as an IID indexed over Γ : Lcontext and σ : Ltype. In de Bruijn notation, the variable v_{0} (denoted by zVar(⋯) below) refers to the last element bound in the context, and the variable v_{n+1} (denoted by sVar(⋯, y), if y denotes v_{n}) in context Γ, σ is the result of lifting the variable v_{n} in context Γ to context Γ, σ. So, we get the following IID:

zVar : (Γ : Lcontext, σ : Ltype) → Lvar(cons(Γ, σ), σ)
sVar : (Γ : Lcontext, σ : Ltype, τ : Ltype) → Lvar(Γ, τ)
→ Lvar(cons(Γ, σ), τ)

The set of λ-terms is given as follows: Variables are λ-terms; if s is a term of type σ → τ and t a term of type σ then ap(s, t) is a term of type τ; if s is a term of type τ in context Γ, σ, then λ(s) is a term of type σ → τ in context Γ. So, the sets Lterm(Γ, σ) of λ-terms of type σ in context Γ are given by the following IID:

var : (Γ : Lcontext, σ : Ltype) → Lvar(Γ, σ) → Lterm(Γ, σ)
ap : (Γ : Lcontext, σ : Ltype, τ : Ltype)
→ Lterm(Γ, ar(σ, τ)) → Lterm(Γ, σ) → Lterm(Γ, τ)
lam : (Γ : Lcontext, σ : Ltype, τ : Ltype) → Lterm(cons(Γ, σ), τ)
→ Lterm(Γ, ar(σ, τ))

The definitions of Lvar and Lterm above correspond to the following four typing rules for the simply typed lambda calculus, where we have omitted the implicit fifth rule (corresponding to the constructor var) which expresses that a variable of type σ is also a term of type σ.

Γ, σ ⇒ v_{0} : σ  \frac{Γ ⇒ v_{n} : τ}{Γ, σ ⇒ v_{n+1} : τ}

\frac{Γ ⇒ s : σ → τ  Γ ⇒ t : σ}{Γ ⇒ s t : τ}  \frac{Γ, σ ⇒ s : τ}{Γ ⇒ λ(s) : σ → τ}

It is easy to translate the above into a restricted IID (without the need for a built-in equality): First, we define equalities =_{Ltype} and =_{Lcontext} in a straightforward way by case analysis on Ltype and Lcontext respectively. The constructors Lvar and Lterm then have the following types:

zVar : (Γ : Lcontext, σ : Ltype, Δ : Lcontext, p : cons(Δ, σ) =_{Lcontext} Γ)

→ Lvar(Γ, σ)

sVar : (Γ : Lcontext, σ : Ltype, Δ : Lcontext, τ : Ltype)

→ (cons(Δ, τ) =_{Lcontext} Γ) → Lvar(Δ, σ) → Lvar(Γ, σ)

lam : (Γ : Lcontext, σ : Ltype, τ : Ltype, ρ : Ltype, p : ar(τ, ρ) =_{Lterm} σ)

→ Lterm(cons(Γ, τ), ρ) → Lterm(Γ, σ)

var has the same type as before, and ap has the same type as before, but with arguments σ and τ interchanged.

More examples. There are many more examples of a similar kind. For example, if Formula is the set of formulas of a formal system, then to be a theorem can often be given by a Formula-indexed inductive definition of

Theorem : Formula → set

where the axioms and inference rules correspond to introduction rules. An element d : Theorem(ϕ) is a derivation (proof tree) with conclusion ϕ. Further examples are provided by the computation rules in the definition of the operational semantics of a programming language.

Proofs by induction on the structure of an indexed inductive definition are often called proofs by rule induction. Thus, the general form of rule induction is captured by the elimination rule for unrestricted IIRD to be given later.

3.2 Examples of Indexed Inductive-Recursive Definitions

Martin-Löf’s computability predicates for dependent types. We shall now turn to proper IIRD. As a first example, we shall formalise the Tait-style computability predicates for dependent types introduced by Martin-Löf [23]. This example was crucial for the historical development of IIRD, since it may be viewed as an early occurrence of the informal notion of an IIRD. In [23] Martin-Löf presents a version of his intuitionistic type theory and proves a normalisation theorem using such Tait-style computability predicates. He works in an informal intuitionistic metalanguage but gives no explicit justification for the meaningfulness of these computability predicates. (Later Aczel [1] has shown how to model a similar construction in classical set theory.) Since the metalanguage is informal the inductive-recursive nature of this definition is implicit. One of the objectives of the current work is indeed to present an extension of Martin-Löf type theory where the inductive-recursive nature of this and other definitions is formalised. In this way, we hope to clarify the reason why it is an acceptable notion from the point of view of intuitionistic meaning explanations in the sense of Martin-Löf [20,22,21].

First, recall that for the case of the simply typed lambda calculus the Taitcomputability predicates ϕ_{A} are predicates on terms of type A which are defined by recursion on the structure of A. We read ϕ_{A}(a) as “a is a computable term of type A”. To match Martin-Löf’s definition [23] we consider here a version where the clause for function types is

• If ϕ_{B}(b[a]) for all closed terms a such that ϕ_{A}(a) then ϕ_{A→B}(λx.b[x]).

How can we generalise this to dependent types? First, we must assume that we have introduced the syntax of expressions for dependent types including Π-types, with lambda abstraction and application. Now we cannot define ϕ_{A} for all (type) expressions A but only for those which are “computable types”. The definition of ϕ_{A} has several clauses, such as the following one for Π [23, p. 161]:

4.1.1.2. Suppose that ϕ_{A} has been defined and that ϕ_{B[a]} has been defined for all closed terms a of type A such that ϕ_{A}(a). We then define ϕ_{Πx:A.B[x]} by the following three clauses.

4.1.1.2.1. If λx.b[x] is a closed term of type Πx : A.B[x] and ϕ_{B[a]}(b[a]) for all closed terms a of type A such that ϕ_{A}(a), then ϕ_{Πx:A.B[x]}(λx.b[x]).

4.1.1.2.2…. 4.1.1.2.3….

(We omit the cases 4.1.1.2.2 and 4.1.1.2.3, which express closure under reduction. They are not relevant for the present discussion. Note that the complete definition of the computability predicate also has one case for each of the other type formers of type theory.)

We also note that Martin-Löf does not use the term “A is a computable type” but only states “that ϕ_{A} has been defined”. We can understand Martin-Löf’s definition as an indexed inductive-recursive definition by introducing a predicate Φ on expressions, where Φ(A) stands for “ϕ_{A} is defined” or “A is a computable type”. Moreover, we add a second argument to ϕ so that ϕ_{A}(p, a) means that a is a computable term of the computable type A, where p is a proof that A is computable. Now we observe that we define Φ inductively while we simultaneously recursively define ϕ.

It would be possible to formalise Martin-Löf’s definition verbatim, but for simplicity, we shall follow a slightly different version due to C. Coquand [8]. Assume that we have inductively defined the set Exp of expressions and have an operation Apl : Exp → Exp → Exp for the application of one expression to another. Apl is a constructor of Exp and we will write A b for Apl(A, b). There are also additional reduction rules for expressions, like reduction of β-redexes. We then define

Ψ : Exp → set ,
ψ : (A : Exp) → Ψ(A) → Exp → set .

by an Exp-indexed IIRD. Ψ is inductively defined and plays the rôle of U, and ψ is recursively defined and plays the rôle of T : (A : Exp, U(A)) → D[A], where D[A] = Exp → set for A : Exp. ψ will depend negatively on Ψ, so this is not a simultaneous inductive definition.

Informally, C. Coquand’s variant of 4.1.1.2 and 4.1.1.2.1 above reads as follows (note that the reference to λx.b[x] is replaced by the reference to arbitrary terms b):

• If Ψ(A) and for all expressions a such that ψ(A, a) we have Ψ(B a), then Ψ(Π(A, B)).

• If Ψ(Π(A, B)) holds according to the previous definition, then ψ(Π(A, B), b) holds iff ψ(B a, b a) holds for all expressions a such that ψ(A, a).

This can be formalised as follows:

π: (A : Exp, p : Ψ(A), B : Exp)
→ (q : (a : Exp, ψ(A, p, a)) → Ψ(B a))
→ Ψ(Π(A, B)) .

Note that q refers negatively to ψ(A, p, a), which is short for ψ(A, p)(a), where ψ(A, p) is the result of the recursively defined function for the second argument p. The corresponding equality rule is

ψ(Π(A, B), π(A, p, B, q), b) = ∀a : Exp.∀x : ψ(A, p, a).ψ(B a, q(a, x), b a) .

Again, the reader should be aware that we have presented only one crucial case of the complete IIRD in [8]. For instance, there are clauses corresponding to closure under reductions.

Palmgren’s higher order universes [27]. This construction generalises Palmgren’s super universe [26], which is a universe which is closed under all the usual operators for forming small sets but is as well closed under the operator for universe formation, that is, an operator which accepts an arbitrary family of sets (a “universe”) and builds a universe containing that family.

Palmgren [27] shows how to generalise this idea to a universe which is closed under higher order universe operators.

Let us first introduce some abbreviations. Let O_{k} be the type of universe operators of order k and F_{k} of families of universe operators of order k : N_{n} given by the following recursive definitions:

O_{0} = set
O_{k+1} = F_{k} → F_{k}
F_{k} = (A : set) × (A → O_{k})

Note that n is given in advance and that Palmgren defines a family ML^{n} of Martin-Löf type theories with universes closed under universe operations of level less than n. It is not possible to internalise the dependence on n : N, since it would require that we could define a family of types by recursion on n : N. In Palmgren [27] the definition of O_{k} and F_{k} are also given by an external recursion on k, but since we included the constant case_{2}^{type} which admits elimination into type for elements of the type 2 in our logical framework, we can internalise this recursion on the finite type N_{n}.

Let A : N_{n+1} → set and B : (k : N_{n+1}) → A_{k} → O_{k} be a family of universe operators. So A_{k} is an index set for universe operators of level k and B_{k} is the family of universe operators of level k indexed by A_{k}.

We shall now give an IIRD of a family

U : N_{n+1} → set
T : (k : N_{n+1}) → U_{k} → O_{k}

which depends on the parameters A and B. We will make the dependence on parameters implicit in the sequel, so that U = U(A, B) and T = T(A, B). The idea is that U_{k} is a set of codes for universe operators of level k with decoding function T_{k}. Informally, U, T is inductive-recursively generated by the following rules:

• There is one constructor for U_{0} corresponding to each of the standard set formers Σ, Π, +, etc.

• There is a code for each index set A_{k} in U_{0}.

• There is a code in U_{k} for each universe operator B_{k}(a).

• There are two constructors which together encode the application of an operator of level i + 1 to a family of operators of level i resulting in another family of operators of level i. To see what this means more precisely, note that families of operators of level i are coded by pairs a : U_{0} and b : (T_{0}(a) → U_{i}). So to each code f : U_{i+1} for an operator of level i+1 and each code (a, b) for a family of level i, we construct another code (a′, b′) for a family of level i encoding the result of applying the operator encoded by f to the family encoded by (a, b). Note that we need two constructors for this operation: one returns a′ : U_{0} and the other returns b′(x′) : U_{i} for x′ : T_{0}(a′).

Let 0 : N_{n+1}, and let inj, succ : N_{n} → N_{n+1} be the injections which map a number in N_{n} to the corresponding number in N_{n+1} and its successor in N_{n+1}, respectively. We have constructors expressing that (U_{0}, T_{0}) is a universe closed under Π, Σ, + etc. and the corresponding equality rules. Furthermore, we have the following constructors for U (note that ap_{i}^{0}(f, a, b) stands for ap^{0}(i, f, a, b), similarly for ap_{i}^{1}(f, a, b, x))

Â : N_{n+1} → U_{0}
B̂ : (k : N_{n+1}) → A_{k} → U_{k}
ap^{0} : (i : N_{n}) → U_{succ(i)} → (a : U_{0}) → (T_{0}(a) → U_{inj(i)}) → U_{0}
ap^{1} : (i : N_{n}) → (f : U_{succ(i)}) → (a : U_{0}) → (T_{0}(a) → U_{inj(i)}) →
T_{0}(ap_{i}^{0}(f, a, b)) → U_{inj(i)}

The equations for T are

T_{0}(Â_{k}) = A_{k}
T_{k}(B̂_{k}(a)) = B_{k}(a)
T_{0}(ap_{i}^{0}(f, a, b)) = π_{0}(T_{succ(i)}(f)(⟨T_{0}(a), T_{inj(i)} ∘ b⟩))
T_{inj(i)}(ap_{i}^{1}(f, a, b, x)) = π_{1}(T_{succ(i)}(f)(⟨T_{0}(a), T_{inj(i)} ∘ b⟩))(x)

As it stands the above is seems not to be an inductive-recursive definition, since the type of ap^{1} depends on T_{0}(ap_{i}^{0}(f, a, b)), which is not the result of applying T to one of the previous arguments of ap^{1}. However, this type is by the equality rules for T_{0} equal to π_{0}(T_{succ(i)}(f)(⟨T_{0}(a), T_{inj(i)} ∘ b⟩)), which is of the correct form: we make use of T_{0}(a), T_{inj(i)}(b(x)) and T_{succ(i)}(f), which is always T applied to a previous inductive argument. Note that there is no problem in applying T_{succ(i)}(f) to ⟨T_{0}(a), T_{inj(i)} ∘ b⟩: Once we have applied T_{succ(i)} to a previous inductive argument of ap^{1}, we obtain an element of O_{succ(i)} = F_{i} → F_{i}, which can be applied to arbritrary elements of F_{i}. If we spell out the type of ap^{1} so that it is clear that it forms part of an IIRD, we obtain the following:

ap^{1} : (i : N_{n}) → (f : U_{succ(i)}) → (a : U_{0}) → (T_{0}(a) → U_{inj(i)}) →
π_{0}(T_{succ(i)}(f)(⟨T_{0}(a), T_{inj(i)} ∘ b⟩)) → U_{inj(i)}

For more information about higher-order universes the reader is referred to Palmgren [27]. The difference between our version and Palmgren’s is that his version is a simultaneous inductive-recursive definition of n universes, whereas ours is an indexed inductive-recursive definition where N_{n} is the index set. Note also that ours is a general IIRD.

Alternatively, we can define a restricted IIRD which is closer to Palmgren’s by instead defining an external sequence of constructors (indexed by k = 0, …, n and i = 0, …, n − 1):

Â_{k}: U_{0}
B̂_{k}: A_{k} → U_{k}
ap_{i}^{0} : U_{i+1} → (a : U_{0}) → (T_{0}(a) → U_{i}) → U_{0}
ap_{i}^{1} : (f : U_{i+1}) → (a : U_{0}) → (T_{0}(a) → U_{i}) → T_{0}(ap_{i}^{0}(f, a, b)) → U_{i}

Again, by using the equality of T_{0} the type of ap_{i}^{1} is equal to the following, which makes clear that this is a constructor of an IIRD:

ap_{i}^{1} : (f : U_{i+1}) → (a : U_{0}) → (T_{0}(a) → U_{i}) →
π_{0}(T_{i+1}(f)(⟨T_{0}(a), T_{i} ∘ b⟩)) → U_{i}

Note that there are 4n + 2 constructors rather than the 4 constructors in the first version. Note also the following subtlety: k in A_{k} is an external index, whereas k in U_{k} is the corresponding internal index in N_{n+1}. Similarly, i is also used both as internal and external index.

The equations for T are written in our notation in the same way as before, except that inj(i), succ(i) are now replaced by i and i+1, respectively. However, although they look the same, they are to be understood differently. We now have 4n + 2 equations indexed externally by k and i, whereas before we had 4 equations, and k and i were internal variables.

We include Palmgren’s construction as an example of a proof-theoretically strong construction which is subsumed by our theory of IIRD. The version, in which elimination is restricted to sets, is conjectured to reach the strength of Kripke-Platek set theory with one recursive Mahlo ordinal. Since U is given by an IIRD it does not appear negatively in any type of its constructors. Note however, that the type of the parameter B refers negatively to set, so if U is considered as a constructor for set with the parameters as arguments, then the type of this constructor refers negatively to set, and we thus have a construction similar in character to the Mahlo universe.

Bove and Capretta’s analysis of the termination of nested recursive definitions of functional programs. Bove and Capretta [6] use indexed inductive-recursive definitions in their analysis of the termination of functions defined by nested general recursion. Given such a function f the idea is to simultaneously define a predicate D(x) expressing that f(x) terminates, and a function f′(x, p), which returns the same value as f(x), but has a proof p : D(x) that f(x) terminates as second argument. So, f′ is a total function defined on the subset of arguments for which f terminates. The role of f′ is to be a version of f which is definable in intuitionistic type theory. For nested recursion the introduction rules for D will refer to f′ and thus we have an indexed inductive-recursive definition.

Assume for instance the rewrite rules f(0) ⟶ f(f(1)), f(1) ⟶ 2, f(2) ⟶ f(1) on the domain {0, 1, 2}. We now inductive-recursively define the termination predicate D for f. We get one constructor for each rewrite rule: C_{0} : (p : D(1), q : D(f′(1, p))) → D(0), C_{1} : D(1), C_{2} : D(1) → D(2). Furthermore, the equality rules for f′ are f′(0, C_{0}(p, q)) = f′(f′(1, p), q), f′(1, C_{1}) = 2, f′(2, C_{2}(p)) = f′(1, p). This is a proper IIRD, since in the type of C_{0} the second argument depends on f′(1, p), where p is the first argument.

3.3 Why Restricted Indexed Inductive-Recursive Definitions?

As already mentioned in the introduction (p. 3) the syntax of case expressions in proof assistants based on dependent type theory is simpler when using restricted IIRD rather than general IIRD. Restricted IIRD were introduced by Thierry Coquand in the implementation of the proof assistant Half, and were also used in the Agda system [7], the successor of Half. (Recently, general IIRD have been added as a separate concept to Agda.) If U and T are given by a restricted IIRD, then we can determine the arguments of a constructor for a particular set U(i) in the family without analysing i. More precisely, if C is a constructor and we write its type in uncurried form, then its type is of the form ((i : I) × A(i)) → U(i).

An example which satisfies this restriction is the accessible part of a relation. We will see in the next subsection how to write the example of trees and forests and Palmgren’s higher order universes in restricted form.

It is easier to construct mathematical models of restricted IIRD, since they can be modelled as initial algebras in an I-indexed slice category. Furthermore, domain-theoretic models of restricted IIRD can be given more easily. One of the reasons why some believe that a fully satisfactory understanding of the identity type has not yet been achieved is that complications arise when introducing certain kinds of models, e.g. domain theoretic models, of unrestricted IIRD.

3.4 The definition of Data Types in the Proof Assistant Agda

Agda [7] allows a slightly more general form of restricted IIRD, in which one defines simultaneously finitely many sets inductively by defining different constructors for each of these sets. An example are the trees and forests mentioned above (8). This is not directly an IIRD in restricted form: If we replace Tree and Forest by Tree′(⋆_{0}) and Tree′(⋆_{1}) as mentioned above, the type of the constructors is as follows:

tree : Tree′(⋆_{1}) → Tree′(⋆_{0}) ,
nil : Tree′(⋆_{1}) ,
cons : Tree′(⋆_{0}) → Tree′(⋆_{1}) → Tree′(⋆_{1}) .

These types are not of the form ((i : 2) × A(i)) → Tree′(i) as required in restricted IIRD. However, we can easily translate this kind of general IIRD into restricted form. In this example, we replace tree, nil, cons by one constructor

C : ((i : 2) × A(i)) → Tree′(i) ,

where A(i) is defined by case distinction on i : 2:

A(⋆_{0}) = Tree′(⋆_{1}) ,
A(⋆_{1}) = 1 + (Tree′(⋆_{0}) × Tree′(⋆_{1})) .

C(⟨⋆_{0}, a⟩), C(⟨⋆_{1}, inl(⋆)⟩), C(⟨⋆_{1}, inr(⟨a, b⟩)⟩) now play the rôle of tree(a), nil and cons(a, b), respectively. What we have done is to form for each index i : 2 the disjoint union A(i) of the product of the arguments of the constructors with result type Tree′(i). This method can as well be applied to Palmgren’s higher order universes, where the constructors at each index can be determined by case analysis on N_{n+1}.

We will show how to generalise the above to the following situation: Assume that we have i : I ⇒ J_{i} : stype, i : I, j : J_{i} ⇒ D[i, j] : type. Assume we define inductive-recursively indexed over i : I, j : J_{i}

U_{ij} : set , T_{ij} : U_{ij} → D[i, j] .

Assume that the constructors of U_{ij} are given as

C_{ik} : (j : J_{i}) → B_{ijk} → U_{ij} ,

where k : K_{i} for some K_{i} : stype. Here B_{ijk} : stype for i : I, j : J_{i}, k : K_{i}. So the constructors are in restricted form relative to j, but not relative to i, but for each i : I the collection of constructors for U_{ij} is given by an index set K_{i}. Assume that we have the equations

T_{ij}(C_{ik}(j, b)) = E_{ik}(j, b) : D[i, j] ,

and that the definition of U_{ij} together with T_{ij} forms an instance of a general IIRD. We can simulate this general IIRD by a restricted IIRD by replacing the constructors C_{ik} by one constructor

C′ : (i : I, j : J_{i}, k : K_{i}, B_{ijk}) → U_{ij}

with equality rule

T_{ij}(C′(i, j, k, b)) = E_{ik}(j, b) .

So (k : K_{i})×B_{ijk} is the disjoint union of the arguments of all constructors with target type U_{ij}, which generalises the sets A(i) in the example Tree′ above.

One can now interpret the constructors of the original general IIRD into this restricted form by defining C_{ik} := (j, b)C′(i, j, k, b). It is an easy exercise to interpret the recursion operator of the general IIRD as well and to see that with this interpretation the equalities required by the rules for the original IIRD hold in the interpreted version.

In this sense restricted IIRD are closely related to the original inductive definition facility of Agda. However, we should add that the correspondence is not precise, since Agda has a more general termination check for functions.

4 Categories for IIRD

4.1 The Category of Indexed Families of Types

As for the non-indexed case, we shall derive a formalisation of IIRD by modelling them as algebras of certain endofunctors in slice categories. Let R be a set of rules for the language of type theory (where each rule is given by a finite set of judgements as premises and one judgement as conclusion). R includes the logical framework used in this article (but not necessarily extensional equality). Let TT(R) be the type theory generated by the rules in R. The category Type(R) is the category, the objects of which are A such that TT(R) proves A : type, and which has as morphisms from A to B terms f such that TT(R) proves f : A → B. We identify objects A, A′ such that TT(R) proves A = A′ : type and functions f, f′ : A → B such that TT(R) proves f = f′ : A → B. It is easy to see that we obtain a category. Note that this only relies on properties of judgemental equality and holds even if R does not contain any equality set. In particular it doesn’t rely on working in extensional type theory.

In order to model I-indexed inductive-recursive definitions, where I is an arbitrary stype, we will use the category Fam(R, I) of I-indexed families of types. An object of Fam(R, I) is an I-indexed family of types, that is, an abstracted expression A for which we can prove i : I ⇒ A[i] : type in TT(R). An arrow from A to B is an I-indexed function, that is, an abstracted expression f for which we can prove i : I ⇒ f[i] : A[i] → B[i] (in TT(R)). Again, we identify A, A′ such that we can prove i : I ⇒ A[i] = A′[i] : type and f, f′ such that we can prove i : I ⇒ f[i] = f′[i] : B[i] → C[i]. Again, it is easy to verify that we obtain a category.

In the following, we will usually omit the argument R in Fam(R, I) and Type(R).

If C is a category and D an object in it, then C/D is the slice category with objects pairs (A, f), where A is an object of C and f an arrow A → D, and morphisms from (A, f) to (B, g) are C-morphisms h : A → B such that g ∘ h = f. Note that we write, when working on the meta-level, pairs with round brackets. This is different from the notation ⟨a, b⟩ for the pair of a and b in the logical framework.

There are two alternative categories in which we can represent pairs (U, T) such that U : I → set and T : (i : I, U(i)) → D[i] (assuming i : I ⇒ D[i] : type).

One is Fam(I)/D, where we identify D with (i)D[i], which is therefore an object of Fam(I). For U, T as given before (U, T) is directly an object of Fam(I)/D.

The other is to model families as fibrations and to use that Fam(I) is equivalent to Type/I (provided the rules of extensional equality are part of R). Thus instead of Fam(I)/D we can equivalently use Type/D′ with D′ := (i : I) × D[i]. An object of this category is a type U′ together with a function T′ : U′ → D′. Intuitively, from U′, T′ we obtain U(i) as the inverse image of i under π_{0} ∘ T′. Furthermore, if u : U(i) and π_{0}(T′(u)) = i, then we can define T (i, u) := π_{1}(T′(u)) : D[i]. Note that in Type/D′ we access the elements of U(i) in an indirect way.

We can thus construct an equivalence of categories (assuming extensional equality):

𝔼_{I,D}^{Fam→Type} : Fam(I)/D → Type/((i : I) × D[i]) and
𝔼_{I,D}^{Type→Fam} : Type/((i : I) × D[i]) → Fam(I)/D .

The object part of these functors is defined as follows: Assume an element (A, f) of Fam(I)/D. Then i : I ⇒ A[i] : type and f : (i : I, A[i]) → D[i]. We define 𝔼_{I,D}^{Fam→Type}(A, f) := (A′, f′) where A′ := (i : I) × A[i] : type and f′ : A′ → ((i : I) × D[i]), f′(⟨i, a⟩) := ⟨i, f(i, a)⟩. Assume an element (A, f) of Type/((i : I) × D[i]). Then A : type, f : A → ((i : I) × D[i]). We define 𝔼_{I,D}^{Type→Fam}(A, f) := (A′, f′) where A′ := (i)((a : A) × (π_{0}(f(a)) =_{I} i)), so A′ is an element of Fam(I), and f′ : (i : I, A′[i]) → D[i], f′(i, ⟨a, p⟩) := π_{1}(f(a)). We leave it to the reader to work out the morphism parts of these functors and to show that they form an equivalence.

Note that 𝔼_{I,D}^{Fam→Type} and 𝔼_{I,D}^{Type→Fam} are meta-level functions, as are the natural transformations showing that they form an equivalence. For instance the object part of 𝔼_{I,D}^{Fam→Type} cannot be defined as a function inside type theory – we cannot even define its type. All we can do is to associate with every (A, f) as above a corresponding pair (A′, f′) as defined before.

General Assumption 4.1 (a) In the following, we assume I : stype,

i : I ⇒ D[i] : type (D an abstracted expression).

(b) We will often omit arguments I, D in functions and constructors in the following, if they are implicitly contained in other arguments, e.g. when one of the arguments is γ : OP_{I,D,E} (where OP will be introduced below).

4.2 Coding Several Constructors into One

We can code several constructors of an IIRD into one: let J be a finite index set for all constructors and A_{j} be the type of the jth constructor (see Appendix A.3 for the definition of J). Then replace all constructors by one constructor of type (j : J) → A_{j} which is definable using case-distinction on J. In case of restricted IIRD we can obtain one constructor in restricted form with type (i : I, j : J) → A_{ij} → C_{i}, if the type of the jth constructor is (i : I) → A_{ij} → C_{i}.

In this way, it will suffice to consider only IIRD with one constructor intro in the sequel.

4.3 Restricted IIRD as Algebras in Fam(I)/D

We already stated that for restricted IIRD, the first argument of the constructor determines the index of the constructed element. By uncurrying the remaining arguments to an element of one set ℍ^{U}(U, T, i) we get the following general form of a constructor

intro : (i : I) → ℍ^{U}(U, T, i) → U(i),

for certain functions (to be given later)

ℍ^{U} : (U : I → set, T : (i : I, U(i)) → D[i], I) → stype

with no free occurrences of U, T and i.

The equality rule for T has the form

T(i, intro(i, a)) = ℍ^{T}(U, T, i, a) ,

for certain functions (also to be given later)

ℍ^{T} : (U : I → set, T : (i : I, U(i)) → D[i], i : I, ℍ^{U}(U, T, i)) → D[i]

with no free occurrences of U, T, i or a. We draw the equality rule as a commuting diagram

ℍ^{𝕌}(U, T, i) \overline{intro(i)_{}}U(i)

[figure: D[i]; T(i); ℍ^{T}(U, T, i)]

in the category Fam(I), that is, the objects D[i], U(i), etc, and the arrows are i : I-indexed families. We will later see that, if we assume extensionality, ℍ^{U}, ℍ^{T} can be extended to work on all families of types (not just on families of sets) so that they together form the components of an endofunctor ℍ on Fam(I)/D, where ℍ(U, T) := (ℍ^{U}(U, T), ℍ^{T}(U, T)). ^{2} Hence (U, T) together with intro will be an ℍ-algebra in Fam(I)/D.

As an example, consider our second formulation of Palmgren’s higher-order universe which is a restricted IIRD with 4n+2 constructors. We only consider the constructor

ap_{i}^{0} : U_{i+1} → (a : U_{0}) → (T_{0}(a) → U_{i}) → U_{0}

where 0 ≤ i ≤ n − 1. The equality rule is

T_{0}(ap_{i}^{0}(f, a, b)) = π_{0}(T_{i+1}(f)(⟨T_{0}(a), T_{i} ∘ b⟩))

We consider the uncurried version of ap_{i}^{0} and draw a diagram:

⟨f, a, b⟩ : U_{i+1} × (a : U_{0}) × (T_{0}(a) → U_{i}) \overline{^{ap_{i}^{0}} ^{}}U_{i}

[figure: π_{0}(T_{i+1}(f)(⟨T_{0}(a), T_{i} ∘ b)⟩)); :; O_{i}; T_{i}; ℍ_{ap_{i}^{0}}^{T}(U, T, i)]

Hence, we have

ℍ_{ap_{i}^{0}}^{U}(U, T, i) := U_{i+1} × (a : U_{0}) × (T_{0}(a) → U_{i})
ℍ_{ap_{i}^{0}}^{T}(U, T, i, ⟨f, a, b⟩) := π_{0}(T_{i+1}(f)(⟨T_{0}(a), T_{i} ∘ b)⟩))

2 To be pedantic: one has to replace ℍ(U, T), ℍ^{U}(U, T), ℍ^{T}(U, T) by uncurried variants ℍ′((U, T)), ℍ′^{U}((U, T))

To define ℍ^{U}(U, T, i) for all constructors, we first do case analysis on i and then take the disjoint union of ℍ_{C}^{U}(U, T, i) for all constructors C with codomain U_{i}.

The diagram for IIRD generalises the situation for non-indexed inductionrecursion [16], where the rules for U and T give rise to an algebra of an appropriate endofunctor 𝔽 on the slice category Type/D.

If D[i] := 1 and therefore ℍ(U, T, i) does not depend on T, we have the important special case of a restricted indexed inductive definition (IID). Here follows as an example the diagram for the accessible part of a relation (we replace (x : I) → (x < i) → Acc(x) by its uncurried form ((x : I) × (x < i)) → Acc(x) in order to obtain the form (x : B) → Acc(x) of an inductive argument of an IID):

(((x : I) × (x < i)) → Acc(x)) \overline{acc(i)_{}}Acc(i)

[figure: 1; !; !]

that is, ℍ^{U}(U, T, i) := ((x : I) × (x < i)) → U(x).

4.4 General IIRD and Functors from Type/((i : I) × D[i]) to Fam(I)/D

In the general case, the constructor intro of an IIRD has no special first argument which determines the index. Instead, the index i : I, such that intro(a) : U(i), is a function of the arguments. So the general form of the type of a constructor is

intro : (a : 𝔾^{U}(U, T)) → U(𝔾^{I}(U, T, a))

for some

𝔾^{U} : (U : I → set, T : (i : I, U(i)) → D[i]) → stype ,
𝔾^{I} : (U : I → set, T : (i : I, U(i)) → D[i]) → 𝔾^{U}(U, T, a)) → I .

Furthermore, we have

T(𝔾^{I}(U, T, a), intro(a)) = 𝔾^{T}(U, T, a)

for some

\begin{aligned}𝔾^{T} & : & (U : I → set, T : (i : I, U(i)) → D[i]) \\ & & → 𝔾^{U}(U, T, a) → D[𝔾^{I}(U, T, a)] , \end{aligned}

We can combine 𝔾^{I} and 𝔾^{T} to get one function

𝔾^{IT} := (U, T, a)⟨𝔾^{I}(U, T, a), 𝔾^{T}(U, T, a)⟩
: (U : I → set, T : (i : I, U(i)) → D[i])
→ 𝔾^{U}(U, T, a) → ((i : I) × D[i]) .

Now we see that 𝔾^{U} and 𝔾^{IT} together form the two components of a function

𝔾 : (U : I → set, T : (i : I, U(i)) → D[i]) → ((U′ : stype) × (U′ → ((i : I) × D[i]))) .

We will later see that this can be extended from sets to types, and that we can prove, if we assume extensionality, that it forms the object part of a functor

𝔾 : Fam(I)/D → Type/((i : I) × D[i]) .

The equality rule is

T(𝔾^{I}(U, T, a), intro(a)) = 𝔾^{T}(U, T, a) ,

as expressed by the following “diagram”:

(a : 𝔾^{U}(U, T)) \overline{intro_{}}U(𝔾^{I}(U, T, a))

[figure: D[𝔾^{I}(U, T, a)]; T(𝔾^{I}(U, T, a)); 𝔾^{T}(U, T, a)]

In the example of the identity relation, we define I := A × A, D[i] := 1, 𝔾^{U}(U, T) := A, 𝔾^{I}(U, T, a) := ⟨a, a⟩, and U(⟨a, a⟩) := I_{A}(a, a). We obtain the following “diagram”:

[figure: (a : A); r; I_{A}(a, a); 1; !; !]

As a second illustration, we show how to obtain the rules for computability predicates for dependent types. (As in Section 3, we only give a definition containing one case, but the complete definition [8] can be obtained by expanding the definition corresponding to the additional constructors).

𝔾^{U}(Ψ, ψ) := (A : Exp) × (p : Ψ(A))× (B : Exp) × ((a : Exp) → ψ(A, p, a) → Ψ(B a)) ,

𝔾^{I}(Ψ, ψ, ⟨A, p, B, q⟩) := Π(A, B) ,
𝔾^{T}(Ψ, ψ, ⟨A, p, B, q⟩) := (b)∀a : Exp.∀x : ψ(A, p, a).ψ(B a, q(a, x), b a) .

4.5 Initial Algebras on Type/((i : I) × D[i])

If we assume extensional equality, we can extend the operation 𝔾 for a general IIRD to a functor 𝔾 : Fam(I)/D → Type/((i : I) × D[i]). We can also define the endofunctor 𝔽 := 𝔾 ∘ 𝔼_{I,D}^{Type→Fam} on Type/((i : I) × D[i]). If we define ℍ := 𝔼_{I,D}^{Fam→Type} ∘ 𝔾, we also obtain an endofunctor ℍ which has the same domain and codomain as the endofunctors corresponding to restricted IIRD, but ℍ will usually not be strictly positive in the sense that it arises from a code for restricted IIRD. So we obtain the following diagram where the two triangles commute and 𝔼_{I,D}^{Fam→Type} and 𝔼_{I,D}^{Fam→Type} form an equivalence of categories:

Type/((i : I) × D[i]) \overline{𝔽 ^{}}Type/((i : I) × D[i])

[figure: Fam(I)/D; 𝔼_{I,D}^{Fam→Type}; 𝔼_{I,D}^{Type→Fam}; ℍ; 𝔾; Fam(I)/D; 𝔼_{I,D}^{Type→Fam}; 𝔼_{I,D}^{Fam→Type}]

Instead of considering families of sets introduced by a functor 𝔾, we can consider initial algebras of the corresponding functor 𝔽 according to the above diagram. This essentially amounts to a reduction of IIRD to non-indexed inductive-recursive definitions, assuming extensional equality. We plan to prove this in detail in a future paper.

5 Formalising the Theory of IIRD

5.1 A Uniform Theory for Restricted and General IIRD

We now show how to formalise a uniform theory for restricted and general IIRD. To this end, we will introduce a theory which can be instantiated to these two cases. This may seem surprising, since restricted IIRD are naturally viewed as special cases of general IIRD – why not just formalise general IIRD, and then explain the restriction? The reason is that restricted IIRD give rise to an interesting simpler theory which can be defined without reference to general IIRD. Nevertheless, the theory of restricted IIRD shares much structure with the theory of general IIRD. It is therefore more economical to put both under one hat.

Recall that a general IIRD will be given by a functor

𝔾 : Fam(I)/D → Type/((x : I) × D[i])

and a restricted IIRD by a functor

ℍ : Fam(I)/D → Fam(I)/D .

Remark. By a functor, we here mean that we can define the object part of the functor and, assuming extensional equality, that we can also define the morphism part and prove the functor laws. However, only the object part of the functor will be used in the formalisation of the theories of IIRD, and therefore our theories can be used in an intensional setting.

Every element (U, T) : Fam(I)/D is uniquely determined by its projections π_{i}(U, T). We also note that for every sequence of functors ℍ_{i} : Fam(I)/D → Type/D[i] there exists a unique functor ℍ : Fam(I)/D → Fam(I)/D such that π_{i} ∘ ℍ = ℍ_{i}. ℍ and 𝔾 will be strictly positive functors in much the same way as 𝔽 in [16]. We draw a diagram which summarises the relationship between these functors:

Fam(I)/D \overline{𝔾_{}}Type/((i : I) × D[i])

[figure: Type/D[i]; ℍ_{i}; π_{i}; Fam(I)/D; 𝔼_{I,D}^{Fam→Type}; ℍ]

However, since ℍ is determined by π_{i} ∘ ℍ and both π_{i} ∘ ℍ and 𝔾 are functors Fam(I)/D ⟶ Type/E, (where E := (i : I) × D[i] in the general case and E := D[i] in the restricted case), it is more economical to introduce the more general notion of a strictly positive functor

𝕂 : Fam(I)/D ⟶ Type/E

for an arbitrary type E. From this we can derive the functors 𝔾 (by setting E := (i : I) × D[i]) and ℍ (by defining π_{i} ∘ ℍ using E := D[i]).

We proceed as in an earlier article [16] and define the type of indices OP_{I,D,E} of strictly positive functors

\frac{E : type}{OP_{I,D,E} : type}

together with

𝕂_{γ}^{U} : (U : I → set, T : (i : I, U(i)) → D[i]) → stype ,
𝕂_{γ}^{T} : (U : I → set, T : (i : I, U(i)) → D[i], a : 𝕂_{γ}^{U}(U, T)) → E ,

for γ : OP_{I,D,E}. (We suppress the arguments I, D, E, when the parameter γ is given.) We remark that one could extend the rules below and define for i : I ⇒ U[i] : type, T : (i : I, U[i]) → D[i]

𝕂_{γ}^{U}(U, T) : type ,
𝕂_{γ}^{T}(U, T) : (a : 𝕂_{γ}^{U}(U, T)) → E .

However, this kind of extension will not play any rôle in our theories of IIRD. We mention it only to be able to consider 𝕂_{γ} as a functor which is defined for all elements (U, T) of Fam(I)/D. Assuming extensional equality, we define the morphism part of this functor (but as before this will not be part of our rules): if i : I ⇒ U′[i] : type, T′ : (i : I, U′[i]) → D[i], then

𝕂_{γ}^{mor}(U, T, U′, T′) : (f : (i : I, U[i]) → U′[i])
→ ((i : I, a : U[i]) → T′(i, f(i, a)) =_{D[i]} T (i, a))
→ 𝕂_{γ}^{U}(U, T) → 𝕂_{γ}^{U}(U′, T′)

We leave it to the reader to verify (by induction on γ) that 𝕂_{γ}^{mor}(U, T, U′, T′, f, p) will be a morphism (i.e. to verify the corresponding commutative diagram) and that the functor laws hold.

We construct elements of OP_{I,D,E} in a similar way as in the non-indexed case:

• Base case: This corresponds to having an IIRD with no arguments of the constructor (i.e. the argument is of type 1). We only have to determine the result of E, which encodes the result of T(intro(a)) for restricted IIRD and both this result and the index i such that intro(a) : U(i) for general IIRD (Note that we suppress the dependency of ι on I, D, E, similarly for the other constructors of OP_{I,D,E})

\begin{aligned}ι & : & E → OP_{I,D,E} , \\ 𝕂_{ι(e)}^{U}(U, T) & = & 1 , \\ 𝕂_{ι(e)}^{T}(U, T, ⋆) & = & e , \end{aligned}

and, assuming extensionality

𝕂_{ι(e)}^{mor}(U, T, U′, T′, f, p, ⋆) = ⋆ .

• Non-dependent union of functors: This corresponds to the situation where the constructor has a first non-inductive argument of type A (that is, an argument which does not refer to U) and where the remaining arguments are coded by γ(a) which depends on a : A.

σ : (A : stype, γ : A → OP_{I,D,E}) → OP_{I,D,E} ,
𝕂_{σ(A,γ)}^{U}(U, T) = (a : A) × 𝕂_{γ(a)}^{U}(U, T) ,
𝕂_{σ(A,γ)}^{T}(U, T, ⟨a, b⟩) = 𝕂_{γ(a)}^{T}(U, T, b) .

and, assuming extensionality

𝕂_{σ(A,γ)}^{mor}(U, T, U′, T′, f, p, ⟨a, b⟩) = ⟨a, 𝕂_{γ(a)}^{mor}(U, T, U′, T′, f, p, b)⟩ .

• Dependent union of functors: This corresponds to the situation where the constructor has an inductive argument, referring to U. This argument has the form g : (a : A) → U(i(a)), where i : A → I. Later arguments can depend on T applied to elements of U, that is, on (see Def. A.6 in Appendix A for the definition of T ∘ ⟨⟨i, g⟩⟩):

T ∘ ⟨⟨i, g⟩⟩ : (a : A) → D[i(a)] .

Therefore the later arguments are given by a function γ : ((a : A) → D[i(a)]) → OP_{I,D,E}. So the parameters of the constructor for the dependent union of elements of OP_{I,D,E} are the stype A, the index function i and the function γ. If A, i, γ are given, the inductive argument will be of type (a : A) → U(i(a)). This argument is followed by the arguments given by γ(T ∘ ⟨⟨i, g⟩⟩), and the result of E will be determined by the remaining arguments (which depend on T∘⟨⟨i, g⟩⟩). So we have the following constructor and equations:

δ : (A : stype, i : A → I, γ : ((a : A) → D[i(a)]) → OP_{I,D,E}) → OP_{I,D,E} ,

𝕂_{δ(A,i,γ)}^{U}(U, T) = (g : (a : A) → U(i(a))) × 𝕂_{γ(T ∘⟨⟨i,g⟩⟩)}^{U}(U, T) ,
𝕂_{δ(A,i,γ)}^{T}(U, T, ⟨g, b⟩) = 𝕂_{γ(T ∘⟨⟨i,g⟩⟩)}^{T}(U, T, b) ,

and, assuming extensionality

𝕂_{δ(A,i,γ)}^{mor}(U, T, U′, T′, f, p, ⟨g, b⟩) = ⟨f ∘ ⟨⟨i, g⟩⟩, 𝕂_{γ(T ∘⟨⟨i,g⟩⟩)}^{mor}(U, T, b)⟩ .

5.2 Formation and Introduction Rules for Restricted IIRD

Restricted IIRD (indicated by a superscript r) are given by strictly positive endofunctors ℍ on the category Fam(I)/D, which can be given by their (strictly positive) projections π_{i} ∘ ℍ : Fam(I)/D → Type/D[i]. So, the set of codes for these functors is given as a family of codes for π_{i} ∘ ℍ. The type of codes is given as

OP_{I,D}^{r} := (i : I) → OP_{I,D,D[i]} : type .

Assume now γ : OP_{I,D}^{r}, U : I → set, T : (i : I, U(i)) → D[i], i : I. The object part of ℍ is defined as

ℍ_{γ}^{U}(U, T, i) := 𝕂_{γ(i)}^{U}(U, T) : stype
ℍ_{γ}^{T}(U, T, i, a) := 𝕂_{γ(i)}^{T}(U, T, a) : D[i]

for U : I → set, T : (i : I, U(i)) → D[i], and a : ℍ_{γ}^{U}(U, T, i).

Using extensionality we obtain the morphism part

ℍ_{γ}^{mor}(U, T, U′, T′, f, p, i, a) := 𝕂_{γ(i)}^{mor}(U, T, U′, T′, f, p, a) : ℍ_{γ}^{U}(U′, T′, i)

We have the following formation rules for U_{γ}^{r} and T_{γ}^{r}:

U_{γ}^{r}(i) : set , T_{γ}^{r}(i) : U_{γ}^{r}(i) → D[i] .

U_{γ}^{r}(i) has constructor

intro_{γ}^{r}(i) : ℍ_{γ}^{U}(U_{γ}^{r}, T_{γ}^{r}, i) → U_{γ}^{r}(i) ,

and the equality rule for T_{γ}^{r}(i) is:

T_{γ}^{r}(i, intro_{γ}^{r}(i, a)) = ℍ_{γ}^{T}(U_{γ}^{r}, T_{γ}^{r}, i, a) .

5.3 Formation and Introduction Rules for General IIRD

For general IIRD (as indicated by superscript g) we consider strictly positive functors 𝔾_{γ} : Fam(I)/D → Type/((i : I) × D[i]) for each code γ in the type of codes for general IIRD, defined as

OP_{I,D}^{g} := OP_{I,D,(i:I)×D[i]} : type .

The object part of the functor 𝔾_{γ} consists of the following three components:

𝔾_{γ}^{U}(U, T) := 𝕂_{γ}^{U}(U, T) : stype
𝔾_{γ}^{I}(U, T, a) := π_{0}(𝕂_{γ}^{T}(U, T, a)) : I
𝔾_{γ}^{T}(U, T, a) := π_{1}(𝕂_{γ}^{T}(U, T, a)) : D[𝔾_{γ}^{I}(U, T, a)]

for U : I → set, T : (i : I, U(i)) → D[i], and a : 𝔾_{γ}^{U}(U, T).

Using extensionality we obtain the morphism part

𝔾_{γ}^{mor}(U, T, U′, T′, f, p, a) := 𝕂_{γ}^{mor}(U, T, U′, T′, f, p, a) : 𝔾_{γ}^{U}(U′, T′) .

We have essentially the same formation rules for U_{γ}^{g} and T_{γ}^{g} as in the restricted case:

U_{γ}^{g} : I → set , T_{γ}^{g} : (i : I, U_{γ}^{g}(i)) → D[i] .

There is one constructor for all U_{γ}^{g}(i). The introduction rule is:

intro_{γ}^{g} : (a : 𝔾_{γ}^{U}(U_{γ}^{g}, T_{γ}^{g})) → U_{γ}^{g}(𝔾_{γ}^{I}(U_{γ}^{g}, T_{γ}^{g}, a)) .

where 𝔾_{γ}^{I}(U_{γ}^{g}, T_{γ}^{g}, a) determines the index from the argument of the constructor.

The equality rule for T_{γ}^{g} is:

T_{γ}^{g}(𝔾_{γ}^{I}(U_{γ}^{g}, T_{γ}^{g}, a), intro_{γ}^{g}(a)) = 𝔾_{γ}^{T}(U_{γ}^{g}, T_{γ}^{g}, a) .

5.4 Elimination Rules for IIRD

We now give the induction principle both for the restricted and the general case. We deviate in an important way from our previous formalisation [16] of non-indexed inductive-recursive definitions. In that paper we constructed the following type of induction hypotheses for the elimination and equality rules:

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

Moreover, for the recursive call in the equality rule we defined

𝔽_{γ}^{map}(U, T, E, h, a) : 𝔽_{γ}^{IH}(U, T, E, a) ,

where h : (u : U) → E[u] and a : 𝔽_{γ}^{U}(U, T).

𝔽_{γ}^{IH}(U, T, E, a) collects the types (b : B) → E[u′(b)] of induction hypotheses for each inductive argument of the form u′ : B → U contained in a. 𝔽_{γ}^{map}(U, T, E, h, a) composes these inductive arguments with h and creates an element of the corresponding induction hypothesis h ∘ u′ : (b : B) → E[u′(b)]. The elimination rule and equality rule were then defined as follows:

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

R_{γ,E}(g, intro_{γ}(a)) = g(a, 𝔽_{γ}^{map}(U_{γ}, T_{γ}, E, R_{γ,E}(g), a)) .

As pointed out to us by Ralph Matthes [24], the problem with that approach, is that 𝔽_{γ}^{IH}(U, T, E, a) is a type and cannot be defined by OP-elimination. This led to problems when interpreting theories into each other. (We plan to publish a note in which we elaborate on this and show how to redeem that problem). Since we would get similar problems in this article, we give an alternative definition. We first define (by OP-elimination)

𝔽_{γ}^{IArg}(U, T, a) : stype ,
𝔽_{γ}^{IArg→U}(U, T, a) : 𝔽_{γ}^{IArg}(U, T, a) → U .

(𝔽_{γ}^{IArg}(U, T, a), 𝔽_{γ}^{IArg→U}(U, T, a)) is a family of elements of U, namely those elements in U referred to in a by an inductive argument. 𝔽_{γ}^{IArg}(U, T, a) is obtained as the disjoint union of all B such that an inductive argument u′ : B → U occurs in a. If b : 𝔽_{γ}^{IArg→U}(U, T, a) originates from b′ : B, where B is as before, then 𝔽_{γ}^{IArg→U}(U, T, a) maps b to u′(b′) : U. Now we can define a variant of 𝔽_{γ}^{IH} and 𝔽_{γ}^{map}:

𝔽_{γ}^{IH}′(U, T, E, a) := (v : 𝔽_{γ}^{IArg}(U, T, a)) → E[𝔽_{γ}^{IArg→U}(U, T, a, v)] ,
𝔽_{γ}^{map}′(U, T, E, g, a) := (v)g(𝔽_{γ}^{IArg→U}(U, T, a, v)) : 𝔽_{γ}^{IH}′(U, T, E, a) .

In appendix B the variants of the theories for inductive-recursive definitions will be introduced in detail.

In case of indexed inductive-recursive definitions, we also need a function which maps elements of 𝔽_{γ}^{IArg}(U, T, a) to the index i : I which the original inductive argument (of the form u′ : (b : B) → U(i(b))) was referring to. In general we proceed as follows:

First we define more generally 𝕂_{γ}^{IArg}, 𝕂_{γ}^{IArg→I} and 𝕂_{γ}^{IArg→U} for γ : OP_{I,D,E}. Assume

\begin{matrix}γ : OP_{I,D,E} , U : I → set , T : (i : I, U(i)) → D[i] , \\ a : 𝕂_{γ}^{U}(U, T) . \end{matrix}

Then we have the following rules:

𝕂_{γ}^{IArg}(U, T, a) : stype , 𝕂_{γ}^{IArg→I}(U, T, a) : 𝕂_{γ}^{IArg}(U, T, a) → I , 𝕂_{γ}^{IArg→U}(U, T, a) : (v : 𝕂_{γ}^{IArg}(U, T, a)) → U(𝕂_{γ}^{IArg→I}(U, T, a, v)) .

𝕂_{ι(e)}^{IArg}(U, T, F, ⋆) = 0 ,

𝕂_{ι(e)}^{IArg→I}(U, T, F, ⋆, x) = case_{0}( , x) ,

𝕂_{ι(e)}^{IArg→U}(U, T, F, ⋆, x) = case_{0}( , x) .

𝕂_{σ(A,γ)}^{IArg}(U, T, ⟨a, b⟩) = 𝕂_{γ(a)}^{IArg}(U, T, b) , 𝕂_{σ(A,γ)}^{IArg→I}(U, T, ⟨a, b⟩, c) = 𝕂_{γ(a)}^{IArg→I}(U, T, b, c) , 𝕂_{σ(A,γ)}^{IArg→U}(U, T, ⟨a, b⟩, c) = 𝕂_{γ(a)}^{IArg→U}(U, T, b, c) .

𝕂_{δ(A,i,γ)}^{IArg}(U, T, ⟨f, b⟩) = A + 𝕂_{γ(T ∘⟨⟨i,f⟩⟩)}^{IArg}(U, T, b) , 𝕂_{δ(A,i,γ)}^{IArg→I}(U, T, ⟨f, b⟩, inl(a)) = i(a) , 𝕂_{δ(A,i,γ)}^{IArg→U}(U, T, ⟨f, b⟩, inl(a)) = f(a) , 𝕂_{δ(A,i,γ)}^{IArg→I}(U, T, ⟨f, b⟩, inr(a)) = 𝕂_{γ(T ∘⟨⟨i,f⟩⟩)}^{IArg→I}(U, T, b, a) , 𝕂_{δ(A,i,γ)}^{IArg→U}(U, T, ⟨f, b⟩, inr(a)) = 𝕂_{γ(T ∘⟨⟨i,f⟩⟩)}^{IArg→U}(U, T, b, a) .

We now define for U : I → stype, T : (i : I, U(i)) → D[i], i : I, u : U ⇒ F [i, u] : type, a : 𝕂_{γ}^{U}(U, T), g : (i : I, u : U) → F [i, u],

𝕂_{γ}^{IH}(U, T, F, a):=(v : 𝕂_{γ}^{IArg}(U, T, a)) → F [𝕂_{γ}^{IArg→I}(U, T, a, v), 𝕂_{γ}^{IArg→U}(U, T, a, v)]

: type ,

𝕂_{γ}^{map}(U, T, F, g, a):=(v)g(𝕂_{γ}^{IArg→I}(U, T, a, v), 𝕂_{γ}^{IArg→U}(U, T, a, v))

: 𝕂_{γ}^{IH}(U, T, F, a) .

In the restricted case, the elimination and equality rules are

R_{γ,F}^{r} (h) : (i : I, u : U_{γ}^{r}(i)) → F [i, u] ,
R_{γ,F}^{r} (h, i, intro_{γ}^{r}(i, a)) = h(i, a, 𝕂_{γ(i)}^{map}(U_{γ}^{r}, T_{γ}^{r}, F, R_{γ,F}^{r} (h), a)) ,

under the assumptions

γ : OP_{I,D}^{r} ,
i : I, u : U_{γ}^{r}(i) ⇒ F [i, u] : type ,

h : (i : I, a : ℍ_{γ}^{U}(U_{γ}^{r}, T_{γ}^{r}, i), 𝕂_{γ(i)}^{IH}(U_{γ}^{r}, T_{γ}^{r}, F, a)) → F [i, intro_{γ}^{r}(i, a)] .

In the general case the elimination and equality rules are

R_{γ,F}^{g} (h) : (i : I, u : U_{γ}^{g}(i)) → F [i, u] ,

R_{γ,F}^{g} (h, 𝔾_{γ}^{I}(U_{γ}^{g}, T_{γ}^{g}, a), intro_{γ}^{g}(a)) = h(a, 𝕂_{γ}^{map}(U_{γ}^{g}, T_{γ}^{g}, F, R_{γ,F}^{g} (h), a)) , under the assumptions

γ : OP_{I,D}^{g} ,
i : I, u : U_{γ}^{g}(i) ⇒ F [i, u] : type ,
h : (a : 𝔾_{γ}^{U}(U_{γ}^{g}, T_{γ}^{g}), 𝕂_{γ}^{IH}(U_{γ}^{g}, T_{γ}^{g}, F, a)) → F [𝔾_{γ}^{I}(U_{γ}^{g}, T_{γ}^{g}, a), intro_{γ}^{g}(a)] .

5.5 Elimination Rules for OP

Definition 5.1 The elimination and equality rules for OP are (assuming E : type and γ : OP_{I,D,E} ⇒ F [γ] : type):

\frac{a : (e : E) → F [ι(e)] b : (A : stype, γ : A → OP_{I,D,E}, f : (x : A) → F [γ(x)]) → F [σ(A, γ)] c : (A : stype, i : A → I, γ : ((a : A) → D[i(a)]) → OP_{I,D,E}) → (f : (x : (a : A) → D[i(a)]) → F [γ(x)]) → F [δ(A, i, γ)]}{R_{I,D,E,F}^{OP} (a, b, c) : (γ : OP_{I,D,E}) → F [γ]}

R_{I,D,E,F}^{OP} (a, b, c, ι(e)) = a(e) ,
R_{I,D,E,F}^{OP} (a, b, c, σ(A, γ)) = b(A, γ, (x)R_{I,D,E,F}^{OP} (a, b, c, γ(x))) ,
R_{I,D,E,F}^{OP} (a, b, c, δ(A, i, γ)) = c(A, i, γ, (x)R_{I,D,E,F}^{OP} (a, b, c, γ(x))) .

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

5.6 The Resulting Theories

Definition 5.2 (a) OP_{intro} consists of the logical framework and the forma-

tion and introduction rules for OP.

(b) The basic theory of indexed inductive-recursive definitions (Bas-IIRD) consists of OP_{intro} and the defining rules for 𝕂^{U}, 𝕂^{T}, 𝕂^{IArg}, 𝕂^{IArg→I}, 𝕂^{IArg→U}, 𝕂^{IH} and 𝕂^{map}.

(c) The theory IIRD^{r} of restricted indexed inductive-recursive definitions consists of Bas-IIRD, the defining rules for OP^{r}, ℍ^{U}, ℍ^{T}, and the formation/introduction/elimination/equality rules for U^{r}, T^{r}, intro^{r}, and R^{r}.

(d) The theory IIRD^{g} of general indexed inductive-recursive definitions consists of Bas-IIRD, the defining rules for OP^{g}, 𝔾^{U}, 𝔾^{I}, 𝔾^{T}, and the formation/introduction/elimination/equality rules for U^{g}, T^{g}, intro^{g}, and R^{g}.

(e) By ext we mean the rules of extensionality.

Note that we did not include the morphism parts of the functors into our rules. Assuming extensionality, they can be defined by recursion on γ, as long as we restrict ourselves as in the rules above to U : I → set.

6 The Examples Revisited

We first introduce the following abbreviations:

γ_{0} +_{OP} γ_{1} := σ(2, (x)case_{2}( , x, γ_{0}, γ_{1})) ,

and, if n ≥ 2,

γ_{0} +_{OP} ⋯ +_{OP} γ_{n} := (⋯ ((γ_{0} +_{OP} γ_{1}) +_{OP} γ_{2}) +_{OP} ⋯ +_{OP} γ_{n}) .

So, if γ_{i} are codes for constructors C_{i}, γ_{0} + γ_{1} is a code for a constructor C, which encodes C_{0} and C_{1}. The first argument of C encodes an element i of {0, 1}. The later arguments of C are the arguments of the constructor C_{i}. Similarly γ_{0} +_{OP} ⋯ +_{OP} γ_{n} is a code for a constructor C which encodes the union of the constructors C_{i} corresponding to γ_{i}. Let for i : I, ι_{⋆}^{g}(i) := ι(⟨i, ⋆⟩) : OP_{I,(−)1}^{g}, and let ι_{⋆}^{r} := ι(⋆) : OP_{I,D,1}.

• The trees and forests have code γ : OP_{2,(−)1}^{r} (= 2 → OP_{2,(−)1,1}), where

\begin{aligned}γ(⋆_{0}) & = & δ(1, (−)⋆_{1}, (−)ι_{⋆}^{r}) , \\ γ(⋆_{1}) & = & ι_{⋆}^{r} +_{OP} δ(1, (−)⋆_{0}, (−)δ(1, (−)⋆_{1}, (−)ι_{⋆}^{r})) . \end{aligned}

Then Tree = U_{2,(−)1,γ}^{r}(⋆_{0}), Forest = U_{2,(−)1,γ}^{r}(⋆_{1}) (we don’t suppress the arguments I = 2, D = (−)1).

• The even number predicate as a general IID as mentioned in the introduction has code ι_{⋆}^{g}(0) +_{OP} σ(N, (n)δ(1, (−)n, (−)ι_{⋆}^{g}(S(S(n)))))\begin{matrix}: OP_{N,(−)1}^{g} \\ (= OP_{N,(−)1,N×1}) . \end{matrix}

• The accessible part of a relation has code

(i)δ((x : I) × (x < i), (z)π_{0}(z), (−)ι_{⋆}^{r})\begin{matrix}: OP_{I,(−)1}^{r} \\ (= (i : I) → OP_{I,(−)1,1}) . \end{matrix}

As a general IIRD, it has code

σ(I, (i)δ((x : I) × (x < i), (z)π_{0}(z), (−)ι_{⋆}^{g}(i)))\begin{matrix}: OP_{I,(−)1}^{g} \\ (= OP_{I,(−)1,I×1}) . \end{matrix}

• The identity set has code σ(A, (a)ι_{⋆}^{g}(⟨a, a⟩)) : OP_{A×A,(−)1}^{g} (= OP_{A×A,(−)1,(A×A)×1}) .

• The simply typed lambda calculus (p. 9) given as a general IIRD can be encoded in the following way. First, Lvar can be encoded as an element of OP_{Lcontext×Ltype,(−)1}^{g} by:

γ_{Lvar} := γ_{Lvar}^{zVar} +_{OP} γ_{Lvar}^{sVar}
γ_{Lvar}^{zVar} := σ(Lcontext, (Γ)σ(Ltype, (α)ι_{⋆}^{g}(⟨cons(Γ, α), α⟩)))
γ_{Lvar}^{sVar} := σ(\begin{matrix}Lcontext, (Γ)σ(Ltype, (α)σ(Ltype, (β) \\ δ(1, (−)⟨Γ, β⟩, (−)ι_{⋆}^{g}(⟨cons(Γ, α), β⟩))))) \end{matrix}

After introducing notations for Lvar and its constructors one can introduce a code for Lterm as an element of OP_{Lcontext×Ltype,(−)1}^{g} as follows:

γ_{Lterm} := γ_{Lterm}^{var} +_{OP} γ_{Lterm}^{ap} +_{OP} γ_{Lterm}^{lam}
γ_{Lterm}^{var} := σ(Lcontext, (Γ)σ(Ltype, (α)σ(Lvar(Γ, α), (−)
ι_{⋆}^{g}(⟨Γ, α⟩))))
γ_{Lterm}^{ap} := σ(\begin{matrix}Lcontext, (Γ)σ(Ltype, (α)σ(Ltype, (β) \\ δ(1, (−)⟨Γ, ar(α, β)⟩, (−)δ(1, (−)⟨Γ, α⟩, (−) \\ ι_{⋆}^{g}(⟨Γ, β⟩)))))) \end{matrix}

γ_{Lterm}^{lam} := σ(\begin{matrix}Lcontext, (Γ)σ(Ltype, (α)σ(Ltype, (β) \\ δ(1, (−)⟨cons(Γ, α), β⟩, (−) \\ ι_{⋆}^{g}(⟨Γ, ar(α, β)⟩))))) \end{matrix}

• For the Tait-style computability predicates for dependent types we have I = Exp, D[i] = Exp → set. The rules given in Subsection 3.2 are incomplete, additional constructors have to be added by using +_{OP} (the current definition actually defines the empty set). The code for the constructor given in Subsection 3.2 is

σ(Exp, (A)

δ(1, (−)A, (f)

σ(Exp, (B)

\begin{matrix}δ((a : Exp) × f(⋆, a), (y)(B π_{0}(y)), (g) \\ ι(⟨Π(A, B), (b)∀a : Exp.∀x : f(⋆, a).g(⟨a, x⟩, b a)⟩))))) \end{matrix}

: OP_{I,D}^{g} (= OP_{I,D,(i:I)×D[i]}) .

• The first version of Palmgren’s higher order universes given by a general IIRD has code

γ := γ_{Univ}^{g} + γ_{A} + γ_{B} + γ_{ap}^{0} + γ_{ap}^{1} : OP_{N_{n+1},(k)O^{k}}^{g} ,

where γ_{Univ}^{g} : OP_{N_{n+1},(k)O^{k}}^{g} is a code expressing that U_{γ_{Univ}^{g},0}, T_{γ_{Univ}^{g},0} is closed under the standard constructors for a universe, and

γ_{A} := σ(N_{n+1}, (k)ι(⟨0, A_{k}⟩)) ,
γ_{B} := σ(N_{n+1}, (k)σ(A_{k}, (a)ι(⟨k, B_{k}(a)⟩))) ,
γ_{ap}^{0} := σ(N_{n+1}, (i) δ(1, (−)succ(i), (T_{f}) ; δ(1, (−)0, (T_{a}) ; \begin{matrix}δ(T_{a}(⋆), (−)inj(i), (T_{b}) \\ ι(⟨0, π_{0}(T_{f}(⋆, ⟨T_{a}(⋆), T_{b}⟩))⟩))))) , \end{matrix}

γ_{ap}^{1} := σ(N_{n+1}, (i) δ(1, (−)succ(i), (T_{f}) δ(1, (−)0, (T_{a}) ; δ(T_{a}(⋆), (−)inj(i), (T_{b}) ; \begin{matrix}σ(π_{0}(T_{f}(⋆, ⟨T_{a}(⋆), T_{b}⟩)), (x) \\ ι(⟨inj(i), π_{1}(T_{f}(⋆, ⟨T_{a}(⋆), T_{b}⟩))(x)⟩)))))) . \end{matrix}

• The second version of Palmgren’s higher order universes given by a restricted IIRD has code

γ : OP_{N_{n+1},(k)O^{k}}^{r}

where

γ(0) := γ_{Univ}^{r} +_{OP} γ_{A_{0}} +_{OP} ⋯ +_{OP} γ_{A_{n}} +_{OP} γ_{B_{0}}+_{OP}
γ_{ap}_{0}^{0} +_{OP} γ_{ap}_{1}^{0} +_{OP} ⋯ +_{OP} γ_{ap}_{n−1}^{0} +_{OP} γ_{ap}_{0}^{1} ,
γ(i) := γ_{B_{i}} +_{OP} γ_{ap}_{i}^{1}  (i = 1, …, n − 1) ,
γ(n) := γ_{B_{n}} ,

γ_{Univ}^{r} : OP_{N_{n+1},(k)O^{k}}^{r}(0) expresses as γ_{Univ}^{g} above that U_{γ_{Univ}^{r},0}, T_{γ_{Univ}^{r},0} is closed under the standard constructors for a universe, and

\begin{aligned}γ_{A_{k}} & := & ι(A_{k}) , \\ γ_{B_{k}} & := & σ(A_{k}, (a)ι(B_{k}(a))) , \\ γ_{ap}_{i}^{0} & := & δ(1, (−)(i + 1), (T_{f}) ; δ(1, (−)0, (T_{a}) ; \begin{matrix}δ(T_{a}(⋆), (−)i, (T_{b}) \\ ι(π_{0}(T_{f}(⋆, ⟨T_{a}(⋆), T_{b}⟩)))))) , \end{matrix} \\ γ_{ap}_{i}^{1} & := & δ(1, (−)(i + 1), (T_{f}) ; δ(1, (−)0, (T_{a}) ; δ(T_{a}(⋆), (−)i, (T_{b}) ; \begin{matrix}σ(π_{0}(T_{f}(⋆, ⟨T_{a}(⋆), T_{b}⟩)), (x) \\ ι(π_{1}(T_{f}(⋆), ⟨T_{a}(⋆), T_{b}⟩)(x)))))) . \end{matrix} \end{aligned}

7 Interpretations between Restricted and General IIRD

7.1 Preliminaries

We assume the rules ext of extensionality. For concrete examples, some of these translations can be carried out using only definitional equality. In such examples we usually only have finitely many levels of nesting of OP, whereas in our theory we may introduce infinitely nested (but still well-founded) elements of OP. For instance, assuming A : N → set, let for n : N

ρ(n) := σ(A(0), (−)σ(A(1), ⋯ σ(A(n), (−)ι_{⋆}^{g}(∗)) ⋯)) : OP_{1,(−)1}^{g} ,

and define γ := σ(N, (n)ρ(n)) : OP_{1,(−)1}^{g}. ρ(n) has n + 1 nesting of OP. Therefore γ has infinite nesting. U_{γ}^{g} has constructor

intro_{γ}^{g}(⟨n, ⟨a_{0}, ⟨a_{1}, …, ⟨a_{n}, 1⟩ ⋯⟩⟩⟩)

where n : N, a_{i} : A(i). So, intro_{γ}^{g} has an unbounded number of arguments. When translating codes we need to prove certain equalities by recursion on γ which require extensional equality in the presence of unbounded nesting of γ. These equalities often become definitional equalities if the nesting is finite, which is the case for most concrete examples.

We will assume OP_{elim} in order to be able to carry out various definitions by induction on γ.

For simplicity, we identify set and stype in the sequel. Note that for every stype A there exists a set A′ together with functions f : A → A′ and g : A′ → A such that ∀a : A.g(f(a)) =_{A} a and ∀a : A′.f(g(a)) =_{A′} a. Take as A′ the set, which is inductively defined with constructor C : A → A′. It is easy to define A′, f, g in any of the theories under consideration and prove the above equalities (using intensional or extensional equality).

We will work informally. From the proof it follows that terms of the first language can be interpreted in the second language such that all rules are valid (that is, the conclusion can be derived from the premises). Note that what we achieve is not just a reduction of categorical principles, but the proof theoretic result that the formal theories can be interpreted into each other. This is especially important when translating the elimination rules – we have to make sure that we can translate the elimination rules of one theory into the other. Most of these proofs rely on recursion on OP.

Notations: In this section, we will make use of the Notation A.4 (informal use of equality).

We summarise the results of this section in the following theorem

Theorem 7.1 (a) IIRD^{r} + OP_{elim} + ext and IIRD^{g} + OP_{elim} + ext can

be interpreted into each other.

(b) The same holds with the restriction of these theories to D[i] : stype.

7.2 Interpretations between Restricted and General IIRD

Informally it is clear that restricted IIRD are special cases of general IIRD. Moreover, we argued in Section 3.3 that general IIRD can be represented by restricted IIRD, provided we have an equality on the index set.

Below we show that the two theories, the one with restricted IIRD and the one with general IIRD can be formally interpreted in each other, provided they are extended with OP-elimination and extensional equality.

Modelling Restricted IIRD by General IIRD. The translation of restricted IIRD into general IIRD is quite simple: in restricted IIRD, we have a constructor intro : (i : I) → A → U_{i} for some set A. In general IIRD, we have a constructor intro′ : (a : A′) → U′_{i′(a)} for some set A′ and some function i′ : A′ → I. So, in order to reduce restricted to general IIRD, we define A′ := (i : I) × A and i′(a) := π_{0}(a). This means turning the special first argument i : I of a restricted IIRD into a similar non-inductive argument of a general IIRD. When we have no argument of the constructor, we have to provide an element of (i : I) × D[i] instead of an element of e : D[i] as in the restricted case: this element will be ⟨i, e⟩.

Categorically, this transformation can be seen as follows: From a functor ℍ : Fam(I)/D → Fam(I)/D of a restricted IIRD we obtain a functor 𝔾 := 𝔼_{I,D}^{Fam→Type} ∘ ℍ : Fam(I)/D → Type/((i : I) × D[i]) of a general IIRD. 𝔾 satisfies the following equations (where ℍ(U, T, i) = (ℍ^{U}(U, T, i), ℍ^{T}(U, T, i)) and 𝔾(U, T) = (𝔾^{U}(U, T), (a)⟨𝔾^{I}(U, T, a), 𝔾^{T}(U, T, a)⟩)):

𝔾^{U}(U, T) = (i : I) × ℍ^{U}(U, T, i) ,
𝔾^{I}(U, T, ⟨i, a⟩) = i ,
𝔾^{T}(U, T, ⟨i, a⟩) = ℍ^{T}(U, T, i, a) .

We are going to show that this translates strictly positive functors for restricted IIRD into strictly positive functors for general IIRD. For every γ : OP_{I,D}^{r} we define γ^{∧} : OP_{I,D}^{g} such that 𝔾_{γ^{∧}} = 𝔼_{I,D}^{Fam→Type} ∘ ℍ_{γ}. (This equality is to be understood componentwise, see Subsection 4.1 for how 𝔼_{I,D}^{Fam→Type} is to be understood type-theoretically.) We first define γ^{∧,i} : OP_{I,D}^{g} for i : I, γ : OP_{I,D,D[i]}:

ι(e)^{∧,i} = ι(⟨i, e⟩) ,
σ(A, γ)^{∧,i} = σ(A, (a)(γ(a))^{∧,i}) ,
δ(A, j, γ)^{∧,i} = δ(A, j, (f)(γ(f))^{∧,i}) .

For γ : OP_{I,D}^{r} we define

γ^{∧} := σ(I, (i)(γ(i))^{∧,i}) : OP_{I,D}^{g} .

Note that the above amounts to the replacement of the special first argument of a restricted IIRD by a similar non-inductive argument and in the base case (ι) the replacement of the argument e by ⟨i, e⟩.

Using extensional equality one easily derives for i : I, ρ : OP_{I,D,D[i]}, γ : OP_{I,D}^{r}, U : I → set, T : (i : I, U(i)) → D[i], a : 𝕂_{γ}^{U}(U, T) the following (the first three equations are shown by induction on ρ):

𝔾_{ρ^{∧,i}}^{U}(U, T) = 𝕂_{ρ}^{U}(U, T) ,
𝔾_{ρ^{∧,i}}^{I}(U, T, a) = i ,
𝔾_{ρ^{∧,i}}^{T}(U, T, a) = 𝕂_{ρ}^{T}(U, T, a) ,
𝔾_{γ^{∧}}^{U}(U, T) = (i : I) × ℍ_{γ}^{U}(U, T, i) ,
𝔾_{γ^{∧}}^{I}(U, T, ⟨i, a⟩) = i ,
𝔾_{γ^{∧}}^{T}(U, T, ⟨i, a⟩) = ℍ_{γ}^{T}(U, T, i, a) .

The interpretation of restricted IIRD into general IIRD is defined by

Ũ_{γ}^{r} := U_{γ^{∧}}^{g} ,  T̃_{γ}^{r} := T_{γ^{∧}}^{g} ,

and for i : I, a : ℍ_{γ}^{U}(Ũ_{γ}^{r}, T̃_{γ}^{r}, i),

\begin{matrix} \\ intro & rγ \end{matrix}(i, a) := intro_{γ^{∧}}^{g}(⟨i, a⟩) : Ũ_{γ}^{r}(i) (= U_{γ^{∧}}^{g}(𝔾_{γ^{∧}}^{I}(Ũ_{γ}^{r}, T̃_{γ}^{r}, ⟨i, a⟩))) .

We have

T̃_{γ}^{r}(\begin{matrix} \\ intro & rγ \end{matrix}(i, a)) = T_{γ^{∧}}^{g}(intro_{γ^{∧}}^{g}(⟨i, a⟩))
= 𝔾_{γ^{∧}}^{T}(Ũ_{γ}^{r}, T̃_{γ}^{r}, ⟨i, a⟩)
= ℍ_{γ}^{T}(Ũ_{γ}^{r}, T̃_{γ}^{r}, i, a) .

The following “diagram” summarises the relationships:

Ũ_{γ}^{r}(i)

[figure: ⟨i, a⟩ : 𝔾_{γ^{∧}}^{U}(Ũ_{γ}^{r}, T̃_{γ}^{r})); intro_{γ^{∧}}^{g}; =; (i : I) × ℍ_{γ}^{U}(Ũ_{γ}^{r}, T̃_{γ}^{r}); \begin{matrix} \\ intro & rγ \end{matrix}]

[figure: D[i]; T̃_{γ}^{r}(i); ℍ_{γ}^{T}(Ũ_{γ}^{r}, T̃_{γ}^{r}, i); 𝔾_{γ^{∧}}^{T}(Ũ_{γ}^{r}, T̃_{γ}^{r})]

where we let (for typographical reasons) \begin{matrix} \\ intro & rγ \end{matrix} represent its uncurried version

⟨i, a⟩ ↦ \begin{matrix} \\ intro & rγ \end{matrix}(i, a).

We will now interpret the elimination rules. First, one easily derives by induction over ρ, assuming i : I, ρ : OP_{I,D,D[i]}, U : I → set, T : (i : I, U(i)) → D[i], a : 𝕂_{ρ}^{U}(U, T), and v : 𝕂_{ρ^{∧,i}}^{IArg}(U, T, a) the following equations:

𝕂_{ρ^{∧,i}}^{IArg}(U, T, a) = 𝕂_{ρ}^{IArg}(U, T, a) ,
𝕂_{ρ^{∧,i}}^{IArg→I}(U, T, a, v) = 𝕂_{ρ}^{IArg→I}(U, T, a, v) ,
𝕂_{ρ^{∧,i}}^{IArg→U}(U, T, a, v) = 𝕂_{ρ}^{IArg→U}(U, T, a, v) .

Therefore we obtain for γ : OP_{I,D}^{g}; i : I; a : 𝕂_{γ^{∧}(i)}^{U}(U, T); v : 𝕂_{γ^{∧}(i)}^{IArg}(U, T, a); i : I, u : U ⇒ E[i, u] : type; g : (i : I, u : U(i)) → E[i, u]:

𝕂_{γ^{∧}}^{IArg}(U, T, ⟨i, a⟩) = 𝕂_{γ(i)}^{IArg}(U, T, a) ,
𝕂_{γ^{∧}}^{IArg→I}(U, T, ⟨i, a⟩, v) = 𝕂_{γ(i)}^{IArg→I}(U, T, a, v) ,
𝕂_{γ^{∧}}^{IArg→U}(U, T, ⟨i, a⟩, v) = 𝕂_{γ(i)}^{IArg→U}(U, T, a, v) ,
𝕂_{γ^{∧}}^{IH}(U, T, E, ⟨i, a⟩) = 𝕂_{γ(i)}^{IH}(U, T, E, a) ,
𝕂_{γ^{∧}}^{map}(U, T, E, g, ⟨i, a⟩, v) = 𝕂_{γ(i)}^{map}(U, T, E, g, a, v) .

Now assume the assumptions of the elimination rules, that is,

i : I, u : Ũ_{γ}^{r}(i) ⇒ E[i, u] : type ,

h : (i : I, a : ℍ_{γ}^{U}(Ũ_{γ}^{r}, T̃_{γ}^{r}, i), 𝕂_{γ(i)}^{IH}(Ũ_{γ}^{r}, T̃_{γ}^{r}, E, a)) → E[i, \begin{matrix} \\ intro & rγ \end{matrix}(i, a)] .

Define

h′ := (a, b)h(π_{0}(a), π_{1}(a), b) : (a : 𝔾_{γ^{∧}}^{U}(U_{γ^{∧}}^{g}, T_{γ^{∧}}^{g}), 𝕂_{γ^{∧}}^{IH}(U_{γ^{∧}}^{g}, T_{γ^{∧}}^{g}, E, a)) → E[𝔾_{γ^{∧}}^{I}(U_{γ^{∧}}^{g}, T_{γ^{∧}}^{g}, a), intro_{γ^{∧}}^{g}(a)] .

Then we can interpret R_{γ,E}^{r}(h) as

k := R_{γ^{∧},E}^{g}(h′) : (i : I, u : Ũ_{γ}^{r}(i)) → E[i, u] ,

and can verify

k(i, \begin{matrix} \\ intro & rγ \end{matrix}(i, a)) = h(i, a, 𝕂_{γ(i)}^{map}(Ũ_{γ}^{r}, T̃_{γ}^{r}, E, k, a)) .

So, we have shown

Lemma 7.2 IIRD^{r} + OP_{elim} + ext can be interpreted in IIRD^{g} + OP_{elim} + ext. The same holds if we restrict D[i] to stype or to D[i] = 1 in both theories.

Modelling General IIRD by Restricted IIRD. From a functor 𝔾 : Fam(I)/D → Type/((i : I) × D[i]) of a general IIRD we obtain a functor ℍ := 𝔼_{I,D}^{Type→Fam} ∘ 𝔾 : Fam(I)/D → Fam(I)/D. To define 𝔼_{I,D}^{Type→Fam} we need however an extensional equality relation =_{I} on I. Then ℍ satisfies the following equations (where as before ℍ(U, T, i) = (ℍ^{U}(U, T, i), ℍ^{T}(U, T, i)) and 𝔾(U, T) = (𝔾^{U}(U, T), (a)⟨𝔾^{I}(U, T, a), 𝔾^{T}(U, T, a)⟩)):

ℍ^{U} : (U : I → set, T : (i : I, U(i)) → D[i]) → I → set ,
ℍ^{U}(U, T, i) = (a : 𝔾^{U}(U, T)) × (𝔾^{I}(U, T, a) =_{I} i) ,
ℍ^{T} : (U : I → set, T : (i : I, U(i)) → D[i])
→ (i : I) → ℍ^{U}(U, T, i) → D[i] ,
ℍ^{T}(U, T, i, ⟨a, p⟩) = 𝔾^{T}(U, T, a) .

Note that the constructors have an additional argument, namely a proof of 𝔾^{I}(U, T, a) =_{I} i. This will add a computational overhead when working with proof assistants.

We show that for every strictly positive functor for a general IIRD the above essentially yields a strictly positive functor for a restricted IIRD, that is, we define for every γ : OP_{I,D}^{g} a γ^{∨} : OP_{I,D}^{r} such that ℍ_{γ^{∨}} is isomorphic to 𝔼_{I,D}^{Type→Fam} ∘ 𝔾_{γ}. (We do not obtain equality. Assume for simplicity that γ does not impose a variable number of arguments and that therefore 𝔾_{γ}^{U}(U, T) can be written as A_{1}×A_{2}×⋯×A_{n}. Then we will get ℍ_{γ^{∨}}^{U}(U, T, i) = A_{1}×(A_{2}× ⋯×(A_{n}×𝔾^{I}(U, T, a) =_{I} i)) instead of (A_{1}×A_{2}×⋯×A_{n})×(𝔾^{I}(U, T, a) =_{I} i).)

First, we define for γ : OP_{I,D}^{g} γ^{∨,i} : OP_{I,D,D[i]} as follows:

ι(⟨i′, e⟩)^{∨,i} = σ(i′ =_{I} i, (−)ι(e)) ,
σ(A, γ)^{∨,i} = σ(A, (a)(γ(a))^{∨,i}) ,
δ(A, j, γ)^{∨,i} = δ(A, j, (f)(γ(f))^{∨,i}) .

Now let for γ : OP_{I,D}^{g}

γ^{∨} := (i)γ^{∨,i} : OP_{I,D}^{r} .

𝔼_{I,D}^{Fam→Type} and 𝔼_{I,D}^{Type→Fam} form an equivalence, and ℍ_{γ^{∨}} is isomorphic to 𝔼_{I,D}^{Type→Fam} ∘ 𝔾_{γ} Therefore, 𝔾_{γ} is isomorphic to 𝔼_{I,D}^{Fam→Type} ∘ ℍ_{γ^{∨}}. In order to interpret IIRD^{g} + OP_{elim} + ext in IIRD^{r} + OP_{elim} + ext, we need to introduce such an isomorphism in IIRD^{r}+OP_{elim}+ext. Therefore, we define in this theory

\begin{aligned}F_{γ}(U, T) & : & (a : 𝔾_{γ}^{U}(U, T)) → ℍ_{γ^{∨}}^{U}(U, T, 𝔾_{γ}^{I}(U, T, a)) , \\ G_{γ}(U, T) & : & (i : I) → ℍ_{γ^{∨}}^{U}(U, T, i) → 𝔾_{γ}^{U}(U, T) . \end{aligned}

We then show that (we use here the notation (f, g) introduced in Def. A.7 in Appendix A) (𝔾_{γ}^{I}, F_{γ}) : 𝔾_{γ} →^{·} 𝔼_{I,D}^{Fam→Type}∘ℍ_{γ^{∨}} and G_{γ} : 𝔼_{I,D}^{Fam→Type}∘ℍ_{γ^{∨}} →^{·} 𝔾_{γ} are natural isomorphisms as expressed by the following diagram^{3} :

𝔾_{γ}^{U}(U, T) (𝔾_{γ}^{I}(U, T), F_{γ}(U, T)) ^{}_{\underline{G_{γ}(U, T)}} (𝔼_{I,D}^{Fam→Type} ∘ ℍ_{γ^{∨}})^{U}(U, T)

= (i : I) × ℍ_{γ^{∨}}^{U}(U, T, i)

[figure: (i : I) × D[i]; (𝔾_{γ}^{I}(U, T), 𝔾_{γ}^{T}(U, T)); (𝔼_{I,D}^{Fam→Type}∘ℍ_{γ^{∨}})^{T}(U,T) =(b)⟨π_{0}(b),ℍ_{γ^{∨}}^{T}(U,T,π_{0}(b),π_{1}(b))⟩]

F_{γ} and G_{γ} are defined as follows:

F_{ι(e)}(U, T, ⋆) = ⟨ref, ⋆⟩ ,
F_{σ(A,γ)}(U, T, ⟨a, b⟩) = ⟨a, F_{γ(a)}(U, T, b)⟩ ,
F_{δ(A,i,γ)}(U, T, ⟨f, b⟩) = ⟨f, F_{γ(T ∘⟨⟨i,f⟩⟩)}(U, T, b)⟩ ,

G_{ι(e)}(U, T, i, ⟨p, ⋆⟩) = ⋆ ,
G_{σ(A,γ)}(U, T, i, ⟨a, b⟩) = ⟨a, G_{γ(a)}(U, T, i, b)⟩ ,
G_{δ(A,i,γ)}(U, T, i, ⟨f, b⟩) = ⟨f, G_{γ(T ∘⟨⟨i,f⟩⟩)}(U, T, i, b)⟩ .

The commutativity of the above diagram is expressed by the following equations, which can be shown by induction on γ (assuming U : I → set, T : (i : I, U(i)) → D[i], a : 𝔾_{γ}^{U}(U, T), i : I, b : ℍ_{γ^{∨}}^{U}(U, T, i)):

G_{γ}(U, T, 𝔾_{γ}^{I}(U, T, a), F_{γ}(U, T, a)) = a ,
𝔾_{γ}^{I}(U, T, G_{γ}(U, T, i, b)) = i ,

3 More precisely, in the previous equations and in the diagram below we refer to an uncurried version of G_{γ}(U, T) of type ((i : I) × ℍ_{γ^{∨}}^{U}(U, T, i)) → 𝔾_{γ}^{U}(U, T). Furthermore, if A is an object of the slice category Type/((i : I) × D[i]), then we denote its two components by A^{U} : Type and A^{T} : A^{U} → ((i : I) × D[i]).

𝔾_{γ}^{T}(U, T, G_{γ}(U, T, i, b)) = ℍ_{γ^{∨}}^{T}(U, T, i, b) ,
F_{γ}(U, T, G_{γ}(U, T, i, b)) = b .

One can verify that we have obtained natural transformations, but that fact will not be needed in our interpretation.

From the above equations follows

ℍ_{γ^{∨}}^{T}(U, T, 𝔾_{γ}^{I}(U, T, a), F_{γ}(U, T, a)) = 𝔾_{γ}^{T}(U, T, a) .

Now define

Ũ_{γ}^{g} := U_{γ^{∨}}^{r} ,  T̃_{γ}^{g} := T_{γ^{∨}}^{r} ,

and for a : 𝔾_{γ}^{U}(Ũ_{γ}^{g}, T̃_{γ}^{g}),

\begin{matrix} \\ intro & g γ \end{matrix}(a) := intro_{γ^{∨}}^{r}(𝔾_{γ}^{I}(Ũ_{γ}^{g}, T̃_{γ}^{g}, a), F_{γ}(Ũ_{γ}^{g}, T̃_{γ}^{g}, a)) : Ũ_{γ}^{g}(𝔾_{γ}^{I}(Ũ_{γ}^{g}, T̃_{γ}^{g}, a)) .

We easily obtain

T̃_{γ}^{g}(𝔾_{γ}^{I}(Ũ_{γ}^{g}, T̃_{γ}^{g}, a), \begin{matrix} \\ intro & g γ \end{matrix}(a)) = 𝔾_{γ}^{T}(Ũ_{γ}^{g}, T̃_{γ}^{g}, a) .

The above is summarised by the following diagram ^{4} :

_{U_{γ}^{g}}(𝔾_{γ}^{I}(_{U_{γ}^{g}},_{T_{γ}^{g}}))

𝔾_{γ}^{U}(_{U_{γ}^{g}},_{T_{γ}^{g}}))

(𝔾_{γ}^{I}(_{U_{γ}^{g}},_{T_{γ}^{g}}),F_{γ}(_{U_{γ}^{g}},_{T_{γ}^{g}}))

G_{γ}(_{U_{γ}^{g}},_{T_{γ}^{g}})

\begin{matrix} \\ intro & ^{g} γ \end{matrix}
(i:I)×ℍ_{γ∨}^{U}(_{U_{γ}^{g}},_{T_{γ}^{g}},i)

intro_{γ^{∨}}^{r}

[figure: D[𝔾_{γ}^{I}(_{U_{γ}^{g}},_{T_{γ}^{g}})]; _{T_{γ}^{g}}(𝔾_{γ}^{I}(_{U_{γ}^{g}},_{T_{γ}^{g}})); ℍ_{γ∨}^{T}(_{U_{γ}^{g}},_{T_{γ}^{g}}); 𝔾_{γ}^{T}(_{U_{γ}^{g}},_{T_{γ}^{g}})]

By induction on γ we can easily derive:

𝕂_{γ^{∨}(i)}^{IArg}(U, T, a) = 𝕂_{γ}^{IArg}(U, T, G_{γ}(U, T, i, a)) ,
𝕂_{γ^{∨}(i)}^{IArg→I}(U, T, a, v) = 𝕂_{γ}^{IArg→I}(U, T, G_{γ}(U, T, i, a), v) ,
𝕂_{γ^{∨}(i)}^{IArg→U}(U, T, a, v) = 𝕂_{γ}^{IArg→U}(U, T, G_{γ}(U, T, i, a), v) .

4 Again we are using uncurried versions of intro_{γ^{∨}}^{r}, ℍ_{γ^{∨}}^{T}(Ũ_{γ}^{g}, T̃_{γ}^{g}), G_{γ}(Ũ_{γ}^{g}, T̃_{γ}^{g}) and 𝔾_{γ}^{T}(Ũ_{γ}^{g}, T̃_{γ}^{g}).

Therefore, assuming i : I, u : U(i) ⇒ E[i, u] : type, g : (i : I, u : U(i)) → E[i, u], and a : 𝕂_{γ^{∨}(i)}^{U}(U, T), we get

𝕂_{γ^{∨}(i)}^{IH}(U, T, E, a) = 𝕂_{γ}^{IH}(U, T, E, G_{γ}(U, T, i, a)) ,
𝕂_{γ^{∨}(i)}^{map}(U, T, E, g, a) = 𝕂_{γ}^{map}(U, T, E, g, G_{γ}(U, T, i, a)) .

For interpreting the elimination rules assume that

i : I, a : Ũ_{γ}^{g}(i) ⇒ E[i, a] : type ,

h : (a : 𝔾_{γ}^{U}(Ũ_{γ}^{g}, T̃_{γ}^{g}), 𝕂_{γ}^{IH}(Ũ_{γ}^{g}, T̃_{γ}^{g}, E, a)) → E[𝔾_{γ}^{I}(Ũ_{γ}^{g}, T̃_{γ}^{g}, a), \begin{matrix} \\ intro & g γ \end{matrix}(a)] .

Define

h′ := (i, a, v)h(G_{γ}(Ũ_{γ}^{g}, T̃_{γ}^{g}, i, a), v) : (i : I, a : ℍ_{γ^{∨}}^{U}(U_{γ^{∨}}^{r}, T_{γ^{∨}}^{r}, i), 𝕂_{γ^{∨}(i)}^{IH}(U_{γ^{∨}}^{r}, T_{γ^{∨}}^{r}, E, a)) → E[i, intro_{γ^{∨}}^{r}(i, a)] .

Note that the type of h′(i, a, v) is

E[\begin{matrix}𝔾_{γ}^{I}(Ũ_{γ}^{g}, T̃_{γ}^{g}, G_{γ}(Ũ_{γ}^{g}, T̃_{γ}^{g}, i, a)), \\ intro_{γ^{∨}}^{r}(𝔾_{γ}^{I}(Ũ_{γ}^{g}, T̃_{γ}^{g}, G_{γ}(Ũ_{γ}^{g}, T̃_{γ}^{g}, i, a)), F_{γ}(Ũ_{γ}^{g}, T̃_{γ}^{g}, G_{γ}(Ũ_{γ}^{g}, T̃_{γ}^{g}, i, a)))] \end{matrix}

= E[i, intro_{γ^{∨}}^{r}(i, a)] .

Now we can interpret R_{γ,E}^{g}(h) as

k := R_{γ^{∨},E}^{r}(h′) : (i : I, u : Ũ_{γ}^{g}(i)) → E[i, u] ,

and obtain

k(𝔾_{γ}^{I}(Ũ_{γ}^{g}, T̃_{γ}^{g}, a), \begin{matrix} \\ intro & g γ \end{matrix}(a)) = h(a, 𝕂_{γ}^{map}(Ũ_{γ}^{g}, T̃_{γ}^{g}, E, k, a)) .

So, we have shown

Lemma 7.3 IIRD^{g} + OP_{elim} + ext can be interpreted in IIRD^{r} + OP_{elim} + ext. The same holds if we restrict D[i] to stype or to D[i] = 1 in both theories.

8 A Model for IIRD^{g}

We will prove the consistency of the theory IIRD^{g} by constructing a settheoretic model of it.

We modify the full set-theoretic model in Dybjer and Setzer [14]. The reader is referred to that paper for more information, since we lack space to repeat all definitions here.

The general setting is as given in [14] (like interpretation of the function type as the full function space, of set and stype as set^{∗} := stype^{∗} := V_{M} for some Mahlo cardinal M, of type as type^{∗} := V_{Λ}, and the interpretation of the logical framework). However, in this article Λ will be the first inaccessible cardinal above M and we omit all statements about λ_{n}. This is necessary since OP_{I,D,E} now refers to families of types D. One could probably avoid this by constructing a more refined model, but our model uses too much strength anyway. We conjecture that the ωth admissible above a recursive Mahlo ordinal suffices in order to build a model.

In the model one uses the standard term and type constructors and elimination constants from the underlying type theory with their arities. The set of raw terms is then defined as the set of expressions formed using constructors, elimination constants, application, abstraction and variables. The interpretation A_{ρ}^{∗} will be given for all raw terms A and all environments ρ referring to arbitrary raw terms, independent of whether A : type or A : B is derivable or not. Therefore A_{ρ}^{∗} might be undefined (which means it will be a special set used for undefinedness), written as A_{ρ}^{∗} ↑, or defined, in which case we write A_{ρ}^{∗} ↓. Consequently, equalities will be usually partial equalities, written as ≃, where A ≃ B means that A ↓⇔ B ↓ and that if A ↓, B ↓ then A and B are the same set. By A :≃ B we mean that we define A in such a way that A ≃ B. It will be part of the soundness theorem, that whenever we can derive in the type theory in question x_{1} : A_{1}, …, x_{n} : A_{n} ⇒ A : type or x_{1} : A_{1}, …, x_{n} : A_{n} ⇒ A : B and a_{i} : A_{i}[x_{1} := a_{1}, …, x_{i−1} := a_{i−1}], then with ρ := [x_{1} := a_{1}, …, x_{n} := a_{n}] we will have that A_{ρ}^{∗} ↓.

The interpretation of SP, arg and map has to be replaced by interpretations of the new constructions. So, we interpret

• (OP_{I,D,E})_{ρ}^{∗} :≃ OP_{I_{ρ}^{∗},λx∈I_{ρ}^{∗}.D[x]_{ρ}^{∗},E_{ρ}^{∗}}^{∗} ,

• σ(A, γ)_{ρ}^{∗} :≃ σ^{∗}(A_{ρ}^{∗}, γ_{ρ}^{∗}) ,

• similarly for the other new constructors,

where for I ∈ set^{∗}, D ∈ I → type^{∗}, E ∈ type^{∗} we define OP_{I,D,E}^{∗} as the least fixed point of the operator

Ψ(X) = E + Σ_{A∈set^{∗}}(A → X) + Σ_{A∈set^{∗}}Σ_{i∈(A→I)}.((Π_{a∈A}.D(i(a))) → X) .

By the inaccessibility of Λ, we have I, D, E ∈ V_{α} for some α < Λ, and therefore there exists a regular cardinal κ < Λ such that for all A ∈ set^{∗} and i ∈ (A → I) we have that the cardinality of E, A, Π_{a∈A}D(i(a)) is < κ. The fixed point is obtained by iterating Ψ up to κ. Since Λ is an inaccessible cardinal, this solution is an element of V_{Λ} = type^{∗}.

The interpretations of ι, σ, δ, and ι^{∗}, σ^{∗} and δ^{∗} are similar to analogous definitions of nil, nonind, ind in [14], and we define (OP_{I,D}^{g})_{ρ}^{∗} :≃ OP_{I_{ρ}^{∗},(i)D[i]_{ρ}^{∗}}^{g,∗} with OP_{I,D}^{g,∗} := OP_{I,D,E}^{∗}, where E := Σi : I.D[i].

We define (𝕂_{γ}^{U}(U, T))_{ρ}^{∗} :≃ 𝕂_{γ_{ρ}^{∗}}^{U∗}(U_{ρ}^{∗}, T_{ρ}^{∗}), similarly for the other operations on 𝕂, where we define for γ ∈ OP_{I,D}^{g,∗}, I ∈ type^{∗}, D ∈ I → type^{∗}, E ∈ type^{∗} by recursion on γ the set 𝕂_{I,D,E,γ}^{U∗}(U, T) ∈ stype^{∗} as follows (if γ, I, D, E are not of this form, we have 𝕂_{I,D,E,γ}^{U∗}(U, T) ↑; a similar proviso applies to all future definitions in this section):

𝕂_{I,D,E,ι^{∗}(e)}^{U∗}(U, T) = 1^{∗} ,
𝕂_{I,D,E,σ^{∗}(A,γ)}^{U∗}(U, T) = Σ_{a∈A}𝕂_{I,D,E,γ(a)}^{U∗}(U, T) ,
𝕂_{I,D,E,δ^{∗}(A,i,γ)}^{U∗}(U, T) = Σ_{f∈Π_{a∈A}U(i(a))} 𝕂_{I,D,E,γ(λx∈A.T (i(x))(f(x)))}^{U∗}(U, T) .

In a similar way, we can define 𝕂_{I,D,E,γ}^{T∗}, 𝕂_{I,D,E,γ}^{IArg∗}, 𝕂_{I,D,E,γ}^{IArg→I∗}, 𝕂_{I,D,E,γ}^{IArg→U∗}, and then define 𝔾_{I,D,γ}^{U∗}, 𝔾_{I,D,γ}^{I∗}, 𝔾_{I,D,γ}^{T∗}, 𝕂_{I,D,E,γ}^{IH∗}, 𝕂_{I,D,E,γ}^{map∗} in an obvious way. Now we interpret

(U_{I,D,γ}(i))_{ρ}^{∗}:≃ U_{I_{ρ}^{∗},(i)D[i]_{ρ}^{∗},γ_{ρ}^{∗}}^{M}(i_{ρ}^{∗}) ,
(T_{I,D,γ}(i, x))_{ρ}^{∗}:≃ T_{I_{ρ}^{∗},(i)D[i]_{ρ}^{∗},γ_{ρ}^{∗}}^{M}(i_{ρ}^{∗}, x_{ρ}^{∗}) ,

where we define for I ∈ set^{∗}, D ∈ I → type^{∗}, γ ∈ OP_{I,D}^{g,∗}, i ∈ I by recursion on γ simultaneously U_{I,D,γ}^{α}(i) ∈ stype^{∗} and T_{I,D,γ}^{α}(i) : U_{I,D,γ}^{α}(i) → type^{∗}, (written more briefly as U^{α}(i), T^{α}(i, x)) as follows:

U^{α}(i) = \{x | \begin{matrix}x ∈ 𝔾_{I,D,γ}^{U∗}(U^{<α}, T^{<α})∧ \\ 𝔾_{I,D,γ}^{I∗}(U^{<α}, T^{<α}, x) = i\} , \end{matrix}

T^{α}(i, x) = 𝔾_{I,D,γ}^{T∗}(U^{<α}, T^{<α}, x) .

with U^{<α} := λi ∈ I. ⋃_{β<α} U^{β}(i), T^{<α} := λi ∈ I. ⋃_{β<α} T^{β}(i).

We interpret intro^{g} using intro_{γ}^{g,∗}(a) := a and R^{g} as R^{g,∗}, where for α ∈ Ord and x ∈ U_{γ}^{<α}(i) we define R_{γ,F}^{g,∗} (g, i, x) by recursion on α in such a way that the definition is independent on α. Let R_{γ,F}^{g,<α}(g, i, x) be the restriction of R_{γ,F}^{g,∗} (g, i, x) to x ∈ U_{γ}^{<α}(i). Assume x ∈ U_{γ}^{α}(i). If x ∈ U_{γ}^{<α}(i), then

R_{γ,F}^{g,∗} (g, i, x) :≃ R_{γ,F}^{g,<α}(g, i, x) .

Otherwise we have x ∈ 𝔾_{I,D,γ}^{U∗}(U_{γ}^{<α}, T_{γ}^{<α}) and i = 𝔾_{I,D,γ}^{I∗}(U_{γ}^{<α}, T_{γ}^{<α}, x). Let

J := 𝕂_{I,D,γ}^{IArg∗}(U_{γ}^{<α}, T_{γ}^{<α}, x) ,
for a ∈ J j(a) := 𝕂_{I,D,E,γ}^{IArg→I∗}(U_{γ}^{<α}, T_{γ}^{<α}, x, a) ,
for a ∈ J u(a) := 𝕂_{I,D,E,γ}^{IArg→U∗}(U_{γ}^{<α}, T_{γ}^{<α}, x, a) ,
c := λa : J.R_{γ,F}^{g,<α}(g, j(a), u(a)) ,
R_{γ,F}^{g,∗} (g, i, x) :≃ g(x, c) .

We can now state a similar soundness theorem as in [14]:

Theorem 8.1 (Soundness theorem)

(a) If ⊢ Γ context, then Γ^{∗} ↓.

(b) If ⊢ Γ ⇒ A : E, where E ≡ type or E is a term, then Γ^{∗} ↓, ∀ρ ∈ Γ^{∗}.A_{ρ}^{∗} ↓ ∧A_{ρ}^{∗} ∈ E_{ρ}^{∗}, and if E ≢ type, ∀ρ ∈ Γ^{∗}.E_{ρ}^{∗} ↓ ∧E_{ρ}^{∗} ∈ type^{∗}.

(c) If ⊢ Γ ⇒ A = B : E, where E ≡ type or E is a term, then Γ^{∗} ↓, ∀ρ ∈ Γ^{∗}(A_{ρ}^{∗} ↓ ∧A_{ρ}^{∗} ∈ E_{ρ}^{∗} ∧ B_{ρ}^{∗} = A_{ρ}^{∗}), and if E ≢ type, ∀ρ ∈ Γ^{∗}.E_{ρ}^{∗} ↓ ∧E_{ρ}^{∗} ∈ type^{∗}.

(d) ⊬ a : 0.

The only difficulty is to show that U^{∗}(i) ∈ set^{∗}, that U^{∗}(i) is closed under intro^{g,∗}, and that R^{∗} is total and fulfils the equality rules. We introduce the following abbreviations for I ∈ set^{∗}, D ∈ I → type^{∗}:

(a) Fam(I, D) := {(U, T) | U ∈ I → set^{∗} ∧ T ∈ Π_{i∈I}(U(i) → D(i))}.

(b) If (U, T), (U′, T′) ∈ Fam(I, D), then (U, T) ≤_{I,D} (U′, T′) ⇔ ∀i ∈ I.(U(i) ⊆ U′(i) ∧ T (i′) ↾ U(i) = T (i)).

The analogue of Lemma 1 in [14] is now as follows:

Lemma 1 Assume I ∈ set^{∗}, D ∈ I → type^{∗}, γ ∈ OP_{I,D}^{g∗}, (U, T), (U′, T′) ∈ Fam(I, D), (U, T) ≤_{I,D} (U′, T′), a ∈ 𝔾_{I,D,γ}^{U∗}(U, T), E := Σi : I.D[i]. Then (a) 𝔾_{I,D,γ}^{U∗}(U, T) ⊆ 𝔾_{I,D,γ}^{U∗}(U′, T′).

(b) 𝔾_{I,D,γ}^{I∗}(U′, T′) ↾ 𝔾_{I,D,γ}^{U∗}(U, T) = 𝔾_{I,D,γ}^{I∗}(U, T).

(c) 𝔾_{I,D,γ}^{T∗}(U′, T′) ↾ 𝔾_{I,D,γ}^{U∗}(U, T) = 𝔾_{I,D,γ}^{T∗}(U, T).

(d) 𝕂_{I,D,E,γ}^{IArg∗}(U′, T′) ↾ 𝔾_{I,D,γ}^{U∗}(U, T) = 𝕂_{I,D,E,γ}^{IArg∗}(U, T).

(e) 𝕂_{I,D,E,γ}^{IArg→I∗}(U′, T′, a) = 𝕂_{I,D,E,γ}^{IArg→I∗}(U, T, a).

(f) 𝕂_{I,D,E,γ}^{IArg→U∗}(U′, T′, a) = 𝕂_{I,D,E,γ}^{IArg→U∗}(U, T, a).

As in [14], we define by induction on γ ∈ OP_{I,D}^{g∗} sets Aux_{I,D,γ}(U, T) by

Aux_{I,D,ι^{∗}(e)}(U, T) = 1 ,
Aux_{I,D,σ^{∗}(A,γ)}(U, T) = Π_{x∈A}Aux_{I,D,γ(x)}(U, T) ,
Aux_{I,D,δ^{∗}(A,j,γ)}(U, T) = A + Π_{f∈Π_{x∈A}U(j(x))}Aux_{I,D,γ(T ∘f)}(U, T) .

The analogue of Lemma 2 in [14] is as follows:

Lemma 2 Assume I ∈ set^{∗}, D ∈ I → type^{∗}, E := Σ_{i∈I}D(i), γ ∈ OP_{I,D}^{g∗}. Let κ be an inaccessible cardinal and let for α < κ, (U^{α}, T^{α}) ∈ Fam(I, D) such that for α < β < κ we have (U^{α}, T^{α}) ≤_{I,D} (U^{β}, T^{β}). Assume for some α_{0} < κ and for all α_{0} ≤ α < κ

Aux_{I,D,γ}(U^{α}, T^{α}) ∈ V_{κ} .

Then

𝔾_{I,D,γ}^{U∗}(U^{<κ}, T^{<κ}) = ⋃_{α<κ} 𝔾_{I,D,γ}^{U∗}(U^{α}, T^{α}) .

Note that Lemma 2 does not hold if we assume I ∈ type^{∗}, so indexed inductionrecursion over a proper type as index set is not covered by this model.

The proof is similar to the proof in [14] (one just lets ϕ = δ^{∗}(A, j, γ) and replaces f : A → U^{<β} by f ∈ Π_{a∈A}U^{<β}(j(a))).

The analogue of [14], Lemma 3 can be stated as follows:

Lemma 3 Assume I ∈ set^{∗}, D ∈ I → type^{∗}, E := Σ_{i∈I}D(i), γ ∈ OP_{I,D}^{g∗}. Abbreviate U^{α}(i) := U_{I,D,γ}^{α}(i), T^{α}(i, x) := T_{I,D,γ}^{α}(i, x), and note that U_{I,D,γ}^{U∗}(i) = U^{M}(i), T_{I,D,γ}^{U∗}(i, x) = T^{M}(i, x). Then the following holds:

(a) For α < M (U^{α}, T^{α}) ∈ Fam(I, D).

(b) If α < β, then (U^{α}, T^{α}) ≤_{I,D} (U^{β}, T^{β}).

(c) There exists κ < M such that U^{α} = U^{M} (and therefore T^{α} = T^{M}) for all α > κ.

(d) U^{M} ∈ V_{M}

(e) For all x ∈ 𝔾^{U∗}(I, D, γ, U^{M}, T^{M}), x ∈ U^{M}(𝔾^{I∗}(I, D, γ, U^{M}, T^{M}, x)).

The proof is similar to the proof of Lemma 3 in [14]. The chain of equivalences now reads:

x ∈ U^{κ}(i) ⇔ x ∈ 𝔾_{I,D,γ}^{U∗}(U^{<κ}, T^{<κ}) ∧ 𝔾_{I,D,γ}^{I∗}(U^{<κ}, T^{<κ}, x) = i
⇔ ∃α < κ.(x ∈ 𝔾_{I,D,γ}^{U∗}(U^{α}, T^{α}) ∧ 𝔾_{I,D,γ}^{I∗}(U^{α}, T^{α}, x) = i)
⇔ ∃α < κ.x ∈ U^{α+1}(i)
⇔ x ∈ U^{<κ}(i) .

The remaining proof of Lemma 3 follows as in [14].

By Lemma 3 (e) it follows that U^{M} is closed under intro^{g,∗}. The totality of R^{∗} follows from its definition above (which was by induction on α) and verifying (using Lemma 1) that all definitions given there result in defined values and the constructions are elements of the interpretations of their types, even when referring intermittently to U_{γ}^{<α}, T_{γ}^{<α} instead of U_{γ}^{M}, T_{γ}^{M}: We use the variables x, a, u(a), j(a) as above. We have x ∈ U_{γ}^{M}(i), J = 𝕂_{I,D,γ}^{IArg∗}(U_{γ}^{M}, T_{γ}^{M}, x), for a ∈ J, j(a) = 𝕂_{I,D,E,γ}^{IArg→I∗}(U_{γ}^{M}, T_{γ}^{M}, x, a) ∈ I, but also j(a) = 𝕂_{I,D,E,γ}^{IArg→I∗}(U_{γ}^{<α}, T_{γ}^{<α}, x, a), u(a) = 𝕂_{I,D,E,γ}^{IArg→U∗}(U_{γ}^{M}, T_{γ}^{M}, x, a), but as well u(a) = 𝕂_{I,D,E,γ}^{IArg→U∗}(U_{γ}^{<α}, T_{γ}^{<α}, x, a) ∈ U_{γ}^{<α}(j(a)), therefore (using that by definition R_{γ,F}^{g,∗} (g) ↾ U_{γ}^{<α} = R_{γ,F}^{g,<α}(g)) c = 𝕂_{I,D,E,γ}^{map∗}(U_{γ}^{M}, T_{γ}^{M}, F, R_{γ,F}^{g,∗} (g), x), which is an element of the interpretation of its associated type. Therefore g(a, c) ∈ F [i, intro_{γ}^{g,∗}(a)].

The correctness of the interpretation of the equality rules for T_{γ}^{M} and for R_{γ,F}^{g} follows easily.

9 Acknowledgements

We would like to thank the anonymous referee for valuable comments on previous versions of this paper. We thank as well Ralph Matthes for discovering [24] an error in a previous article [16] about IRD. As a consequence, we have modified the corresponding constructions for IIRD, too.

An earlier and much shorter version of this paper appeared in LNCS 2183 [15].

A Appendix: The Logical Framework A.1 Complete Rules of the Logical Framework In this article we usually do not write out the whole 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))

Rules Relating type, stype, set

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}

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}

Rules for 0, 1, 2

0 : stype  \frac{a : 0  x : 0 ⇒ A : type}{case_{0}((x)A, a) : A[x := 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}]}

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

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

Definition A.1 (a) We write (x)a instead of (x : A)a (abstraction).

(b) We write a(b_{1}, …, b_{n}) instead of a(b_{1}) ⋯ (b_{n}) for iterated application.

(c) We write repeated abstraction as (x_{1} : A_{1}, …, x_{n} : A_{n})a or (x_{1}, …, x_{n})a instead of (x_{1} : A_{1}) ⋯ (x_{n} : A_{n})a.

(d) We write (x_{1} : A_{1}, …, x_{n} : A_{n}) → C for (x_{1} : A_{1}) → ⋯ → (x_{n} : A_{n}) → C.

(e) We write A → B for (x : A) → B for some fresh x.

(f) We write (x : A, B) → C for (x : A, y : B) → C for some fresh y and similarly for longer terms.

(g) We write A × B for (x : A) × B for some fresh x;

(h) We write (x : A) × (y : B) × C for (x : A) × ((y : B) × C) and similarly for longer products.

(i) We write (x : A) × B × C for (x : A) × (y : B) × C for some fresh y. A × (y : B) × C, A × B × C and similar notions for longer products are defined in the same way.

(j) We write π_{0}^{3}(x) for π_{0}(x), π_{1}^{3}(x) for π_{0}(π_{1}(x)) and π_{2}^{3}(x) for π_{0}(π_{1}(π_{1}(x))). These are the 3 projections of a product (x : A) × (y : B) × C. Similarly we define the projections π_{i}^{n} for n > 3, i < n.

(k) (−) stands for an abstraction (x) for a variable x, which is not used later.

(l) We usually omit in case_{0}((x)A, ⋯) and case_{2}((x)A, ⋯) the first argument (x)A, and write case_{0}( , ⋯), case_{2}( , ⋯) instead.

The disjoint union of two types is not a primitive notion in our logical framework, but it can be defined as follows (note that it doesn’t refer to an equality type; in the following definition, we usually suppress arguments A, B):

Definition A.2 (a) We define an equality =′_{2} on 2 as follows x =′_{2} y := case_{2}((−)stype, x, case_{2}( , y, 1, 0), case_{2}( , y, 0, 1)) : stype. Note that (⋆_{0} =′_{2} ⋆_{0}) = (⋆_{1} =′_{2} ⋆_{1}) = 1, (⋆_{0} =′_{2} ⋆_{1}) = (⋆_{1} =′_{2} ⋆_{0}) = 0.

(b) Define ref′ : (x : 2) → (x =′_{2} x), ref′ x = case_{2}( , x, ⋆, ⋆). We write ref′_{x} for ref′ x.

(c) We define for A, B : type, h : (x : 2) → (x =′_{2} ⋆_{0}) → case_{2}^{type}(x, A, B) → A, h(x) = case_{2}( , x, (p, y)y, (p, y)case_{0}( , p)), and have h(⋆_{0}, p, x) = x.

Similarly we define k : (x : 2) → (x =′_{2} ⋆_{1}) → case_{2}^{type}(x, A, B) → B s.t. k(⋆_{1}, p, x) = x.

(d) We define A + B := (x : 2) × case_{2}^{type}(x, A, B), and for a : A, inl(a) := ⟨⋆_{0}, a⟩ : A + B, and for b : B, inr(b) := ⟨⋆_{1}, b⟩ : A + B.

(e) We define for A, B : type, x : (A + B) ⇒ C[x] : type

h′(C) : (x : 2, p : x =′_{2} ⋆_{0}, y : case_{2}^{type}(x, A, B), C[inl(h(x, p, y))]) → C[⟨x, y⟩] ,

h′(C, x) = case_{2}( , x, (p, y, c)c, (p, y, c)case_{0}( , p)). Similarly we define k′(C) : (x : 2, p : x =′_{2} ⋆_{1}, y : case_{2}^{type}(x, A, B), C[inr(k(x, p, y))]) → C[⟨x, y⟩] ,

and we note that h′(C, ⋆_{0}, p, y, c) = c, k′(C, ⋆_{1}, p, y, c) = c.

(f) We define for x : A + B ⇒ C[x] : type,

elim_{+}(C) : (\begin{matrix}step_{A} : (a : A) → C[inl(a)], \\ step_{B} : (b : B) → C[inr(b)], \\ c : A + B) → C[c] \end{matrix}

by elim_{+}(C, step_{A}, step_{B}, c) = f(π_{0}(c), c, ref_{π_{0}(c)}), where

f : (y : 2) → (x : A + B) → π_{0}(x) =_{2} y → C[x] ,

f(y) := case_{2}(\begin{matrix}, y, \\ (x, p)h′(C, π_{0}(x), p, π_{1}(x), step_{A}(h(π_{0}(x), p, π_{1}(x))), \\ (x, p)k′(C, π_{0}(x), p, π_{1}(x), step_{B}(k(π_{0}(x), p, π_{1}(x)))) . \end{matrix}

Note that elim_{+}(C, step_{A}, step_{B}, inl(a)) = f(⋆_{0}, inl(a), ref_{⋆_{0}}) = h′(C, ⋆_{0}, ref_{⋆_{0}}, a, step_{A}(h(⋆_{0}, ref_{⋆_{0}}, a)) = step_{A}(a) and similarly elim_{+}(C, step_{A}, step_{B}, inr(b)) = step_{B}(b).

(g) Because of the previous definition, we can define t[x] : C[x] depending on x : A+B for some type C[x] by defining t[inl(a)] := s_{inl}[a] and t[inr(b)] = s_{inr}[b] for some s_{inl}, s_{inr} s.t. a : A ⇒ s_{inl}[a] : C[inl(a)] and b : B ⇒ s_{inr}[b] : C[inr(b)]. This amounts to defining t[x] := elim_{+}(x, (a)s_{inl}[a], (b)s_{inr}[b]).

In this paper, we have the following general assumption about equality versions of rules and omitting types in equality judgements:

General Assumption A.3 (a) In this article, except for the previous part of the Appendix, all rules are understood to be supplemented by additional equality rules. For the rules of the logical framework above, the equality rules were already included above. They give examples how rules are to be supplemented: E.g. the rule

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

was 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}

was 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, as they can easily be filled in by the reader.

When proving the equivalence of theories, we will often argue informally, and use the following convention:

Notation A.4 By “we prove a = b” by induction on some parameter we mean (assuming a, b : C for some type C) that we introduce p : a =_{C} b by induction on this parameter. Note that in the presence of extensionality, the existence of such a p is equivalent to a = b : C.

We introduce the concept of isomorphisms between types:

Definition A.5 (a) Let A, B : type. Then

A ≅ B := \begin{matrix}(f : A → B)× \\ (g : B → A)× \\ ((x : A) → (g(f(x)) =_{A} x)) \\ ((x : B) → (f(g(x)) =_{B} x) \end{matrix}

(b) Assume f : A ≅ B. Then we define (see Lemma A.1 (j) for the definition of π_{i}^{n}):

f^{→}:= π_{0}^{4}(f) : A → B ,
f^{←}:= π_{1}^{4}(f) : B → A ,
f^{←^{→}}:= π_{2}^{4}(f) : (a : A) → f^{←}(f^{→}(a)) =_{A} a ,
f^{→^{←}}:= π_{3}^{4}(f) : (b : B) → f^{→}(f^{←}(b)) =_{B} b .

When referring to the later arguments on previous inductive arguments, we often make use of the expression T ∘ ⟨⟨i, f⟩⟩.

Definition A.6 Assume A, B : type, b : B ⇒ C[b] : type, b : B, c : C[b] ⇒ F [b, c] : type, g : A → B, h : (a : A) → C[g(a)], f : (b : B, c : C[b]) → F [b, c]. Then we define

f ∘ ⟨⟨g, h⟩⟩ := (a)f(g(a), h(a)) : (a : A) → F [g(a), h(a)] .

We introduce as well a notation for forming the product of two functions (we cannot use the usual notation in category theory ⟨f, g⟩, since it is used for pairs):

Definition A.7 Assume A, B : type, b : B ⇒ C[b] : type, f : A → B, g : (a : A) → C[f(a)]. Then we define

\begin{aligned}(f, g) & : (a : A) → ((b : B) × C[b]) , \\ (f, g)(a) & := ⟨f(a), g(a)⟩ . \end{aligned}

A.2 Rules of Extensionality

We have explained above how to define the equality set as an indexed inductive definition, but this equality will not be extensional. For some purposes we need to assume that we have an extensional equality type and add the following rules (ext) of extensionality. They are only added to our theory if mentioned explicitly.

\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}

A.3 Finite Sets with Elimination into Type

From the rules of 2 we can derive for any natural number n the set n of n-elements with elimination into type as follows:

• n is defined as 0, 1, 2 for n <= 2.

• For n ≥ 3, n = m + 1, n := (a : 2) × case_{2}^{type}(a, m, 1).

• For n ≥ 3, n = m + 1, a : n, A_{1}, …, A_{n} : type, we define

case_{n}^{type}(a, A_{1}, …, A_{n}) := case_{2}^{type}(π_{0}(a), case_{m}^{type}(π_{1}(a), A_{1}, …, A_{m}), A_{n}) .

• Ordinary case distinction case_{n} can be defined similarly.

B Appendix: Modified Rules for Inductive-Recursive Definitions

We define in the following the theory IR_{elim}^{ext}′, in which the use of 𝔽_{γ}^{IH}, 𝔽_{γ}^{map} for defining the elimination and equality rules for U_{γ} is replaced by 𝔽_{γ}^{IArg} and 𝔽_{γ}^{IArg→U}. See Subsection 5.4 on the motivation for this change.

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

𝔽_{ι(e)}^{IArg}(U, T, ∗) = 0 ,
𝔽_{ι(e)}^{IArg→U}(U, T, ∗, x) = case_{0}( , x) ,
𝔽_{σ(A,γ)}^{IArg}(U, T, ⟨a, b⟩) = 𝔽_{γ(a)}^{IArg}(U, T, b) ,
𝔽_{σ(A,γ)}^{IArg→U}(U, T, ⟨a, b⟩, c) = 𝔽_{γ(a)}^{IArg→U}(U, T, b, c) ,
𝔽_{δ(A,γ)}^{IArg}(U, T, ⟨f, b⟩) = A + 𝔽_{γ(T ∘f)}^{IArg}(U, T, b) ,
𝔽_{δ(A,γ)}^{IArg→U}(U, T, ⟨f, b⟩, inl(a)) = f(a) ,
𝔽_{δ(A,γ)}^{IArg→U}(U, T, ⟨f, b⟩, inr(a)) = 𝔽_{γ(T ∘f)}^{IArg→U}(U, T, b, a) ,
γ : OP_{D}
x : U_{γ} ⇒ E[x] : type

g : (a : 𝔽_{γ}^{U}(U_{γ}, T_{γ}), ih : (v : 𝔽_{γ}^{IArg}(U_{γ}, T_{γ}, a)) → E[𝔽_{γ}^{IArg→U}(U_{γ}, T_{γ}, a, v)]) → E[intro_{γ}(a)]

R_{γ,E}(g) : (u : U_{γ}) → E[u]
R_{γ,E}(g, intro_{γ}(a)) = g(a, (v)R_{γ,E}(g, 𝔽_{γ}^{IArg→U}(U, T, a, v)))

Definition B.1 (a) The theory IR_{elim}^{ext}′ is obtained from the theory IR_{elim}^{ext}, as defined in [16], by replacing the logical framework by the one used in this article (that is, with case_{2}^{type}), omitting the constants 𝔽^{IH}, 𝔽^{map} and the rules for introducing them, adding the rules for 𝔽^{IArg} and 𝔽^{IArg→U} as introduced above and replacing the elimination and equality rules for U_{γ} by the rules above.

(b) OP_{intro}^{s} and OP_{elim}^{s} are the introduction and elimination rules for OP_{D} for inductive-recursive definitions as introduced in [16]. Note that OP_{intro}^{s} is contained in the rules for IR_{elim}^{ext}′, but not OP_{elim}^{s}.

Lemma B.2 Let (𝔽^{IH}) be the rules for 𝔽^{IH}. Define 𝔽_{γ}^{map} by using OP_{elim}^{s}.

Define in IR_{elim}^{ext}′ + (𝔽^{IH}) + OP_{elim}^{s}

𝔽_{γ}^{IH}′(U, T, E, a) := (v : 𝔽_{γ}^{IArg}(U, T, a)) → E[𝔽_{γ}^{IArg→U}(U, T, a, v)] ,

𝔽_{γ}^{map}′(U, T, E, g, a) := (v : 𝔽_{γ}^{IArg}(U, T, a))g(𝔽_{γ}^{IArg→U}(U, T, a, v)) .

Then in IR_{elim}^{ext}′ +(𝔽^{IH})+OP_{elim}^{s} one can introduce the following isomorphism and show the following equation:

𝔽_{γ}^{IH,≅}(U, T, E, a) : 𝔽_{γ}^{IH}′(U, T, E, a) ≅ 𝔽_{γ}^{IH}(U, T, E, a)
𝔽_{γ}^{IH,≅}(U, T, E, a)^{→}(𝔽_{γ}^{map}′(U, T, E, g, a)) = 𝔽_{γ}^{map}(U, T, E, g, a)

In this sense it follows that the new rules are equivalent to the old rules. Note that however 𝔽_{γ}^{IH}(U, T, E, a) cannot be defined using the new rules.

References

[1] P. Aczel. Frege Structures and the Notions of Proposition, Truth, and Set, pages 31–59. North-Holland, 1980.

[2] T. Altenkirch, V. Gaspes, B. Nordström, and B. von Sydow. A user’s guide to ALF. http://www.cs.chalmers.se/ComputingScience/Research/ Logic/alf/guide.html, 1996.

[3] T. Altenkirch and C. McBride. Generic programming within dependently typed programming. In Generic Programming, 2003. Proceedings of the IFIP TC2 Working Conference on Generic Programming, Schloss Dagstuhl, July 2002.

[4] T. Altenkirch and B. Reus. Monadic presentations of lambda terms using generalized inductive types. In Computer Science Logic, 1999.

[5] M. Benke, P. Dybjer, and P. Jansson. Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing, 10:265–289, 2003.

[6] A. Bove and V. Capretta. Nested general recursion and partiality in type theory. In R. J. Boulton and P. B. Jackson, editors, Theorem Proving in Higher Order Logics: 43th International Conference, TPHOLs 2001, volume 2152 of Springer-Verlag, LNCS, pages 121–135, September 2001.

[7] C. Coquand. Agda. 2000. http://www.cs.chalmers.se/∼catarina/agda/.

[8] C. Coquand. A realizability interpretation of Martin-Löf’s type theory. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998.

[9] T. Coquand. Pattern matching with dependent types. In B. Nordström and Kent Petersson and Gordon Plotkin, editor, Proceedings of The 1992 Workshop on Types for Proofs and Programs, June 1992.

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

[11] 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.

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

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

[14] 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.

[15] P. Dybjer and A. Setzer. Indexed induction-recursion. In Proof Theory in Computer Science International Seminar, PTCS 2001 Dagstuhl Castle, Germany, number 2183 in LNCS, pages 93–113, October 2001.

[16] P. Dybjer and A. Setzer. Induction-recursion and initial algebras. Annals of Pure and Applied Logic, 124:1–47, 2003.

[17] R. Hinze and J. Jeuring. Generic Haskell: Practice and theory. In R. Backhouse and J. Gibbons, editors, Generic Programming, number 2793 in LNCS, pages 1 – 56. Springer-Verlag, 2003.

[18] P. Jansson and J. Jeuring. PolyP — a polytypic programming language extension. In Proc. POPL’97, pages 470–482. ACM Press, 1997.

[19] L. Magnusson and B. Nordström. The ALF proof editor and its proof engine. In Types for proofs and programs, volume 806 of Lecture Notes in Computer Science, pages 213–317. Springer, 1994.

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

[21] P. Martin-Löf. On the meaning of the logical constants and the justification of the logical laws, 1983. Notes from a series of lectures given in Siena.

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

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

[24] R. Matthes. Review of Dybjer, Peter and Setzer, Anton: Induction-recursion and initial algebras. Mathematical Reviews, MR2013392, 2005. To appear.

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

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

[27] E. Palmgren. On universes in type theory. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998.

[28] C. Paulin-Mohring. Inductive definitions in the system Coq - rules and properties. In Proceedings Typed λ-Calculus and Applications, pages 328–245. Springer-Verlag, LNCS, March 1993.

[29] H. Pfeifer and H. Rueß. Polytypic proof construction. In Y. Bertot, editor, Proc. TPHOLs’99, volume 1690 of LNCS, pages 55–72. Springer-Verlag, 1999.

[30] Qiao Haiyan. Formalising formulas-as-types-as-objects. In T. Coquand, P. Dybjer, B. Nordström, and J. Smith, editors, Types for Proofs and Programs, volume 1956 of Lecture Notes in Computer Science, pages 174–194. Springer, 2000.

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

[32] A. Setzer. Proof theory of Martin-Löf type theory – an overview. Mathematiques et Sciences Humaines, 42 année, n^{o}165:59 – 99, 2004.