Inductive-inductive Definitions

Fredrik Nordvall Forsberg^{}and Anton Setzer^{}

Swansea University

                    {csfnf, a.g.setzer}@swansea.ac.uk

Abstract. We present a principle for introducing new types in type theory which generalises strictly positive indexed inductive data types. In this new principle a set A is defined inductively simultaneously with an A-indexed set B, which is also defined inductively. Compared to indexed inductive definitions, the novelty is that the index set A is generated inductively simultaneously with B. In other words, we mutually define two inductive sets, of which one depends on the other. Instances of this principle have previously been used in order to formalise type theory inside type theory. However the consistency of the framework used (the theorem prover Agda) is not so clear, as it allows the definition of a universe containing a code for itself. We give an axiomatisation of the new principle in such a way that the resulting type theory is consistent, which we prove by constructing a set-theoretic model.

1 Introduction

Martin-Löf Type Theory [12] is a foundational framework for constructive mathematics, where induction plays a major part in the construction of sets. Martin-Löf’s formulation [12] includes inductive definitions of for example Cartesian products, disjoint unions, the identity set, finite sets, the natural numbers, wellorderings and lists. External schemas for general inductive sets and inductive families have been given by Backhouse et. al. [2] and Dybjer [6] respectively. Indexed inductive definitions have also been used for generic programming in dependent type theory [3, 13].

Another induction principle is induction-recursion, where a set U is constructed inductively simultaneously with a recursively defined function T U D for some possibly large type D. The constructor for U may depend negatively on T applied to elements of U. The main example is Martin-Löf’s universe à la Tarski [15]. Dybjer [8] gave a schema for such inductive-recursive definitions, and this has been internalised by Dybjer and Setzer [9–11].

In this article, we present another induction principle, which we, in reference to induction-recursion, call induction-induction. A set A is inductively defined simultaneously with an A-indexed set B, which is also inductively defined, and

Supported by EPSRC grant EP/G033374/1, Theory and applications of inductionrecursion.

the introduction rules for A may also refer to B. So we have formation rules A Set, B A Set and typical introduction rules might take the form

\begin{matrix}a A & b B a & … \\ intro_{A} a, b, … A \end{matrix} \begin{matrix}a_{0} A & b B a_{0} & a_{1} A & … \\ intro_{B} a_{0}, b, a_{1}, … B a_{1} \end{matrix}

This is not a simple mutual inductive definition of two sets, as B is indexed by A. It is not an ordinary inductive family, as A may refer to B. Finally, it is not an instance of induction-recursion, as B is constructed inductively, not recursively.

Let us consider a first example, which will serve as a running example to illustrate the formal rules. We simultaneously define a set of platforms together with buildings constructed on these platforms. The ground is a platform, and if we have a building, we can always construct a new platform from it by building an extension. We can always build a building on top of any platform, and if we have an extension, we can also construct a building hanging from it. (See Figure 1 for an illustration.) This gives rise to the following inductive-inductive definition of Platform Set, Building Platform Set (where p Platform means that p is a platform and b Building p means that b is a building constructed on the platform p)^{1} with constructors

ground Platform ,
extension p Platform Building p Platform ,
onTop p Platform Building p ,
hangingUnder p Platform b Building p  Building extension p, b .

Note that the index of the codomain of hangingUnder is extension p, b , i.e. hangingUnder p, b Building extension p, b . In other words, it is not possible to have a building hanging under the ground.

p  \begin{matrix}p \\ b \end{matrix}  \begin{matrix}p \\ b \end{matrix}

Fig. 1. onTop p , extension p, b and hangingUnder p, b .

1 The collection of small types in Martin-Löf type theory is called Set for historic reasons, whereas Type is reserved for the collection of large types. The judgement Building Platform Set means that for every p Platform, Building p Set. The type theoretic notation will be further explained in Section 2.

Inductive-inductive definitions have been used by Dybjer [7], Danielsson [5] and Chapman [4] to internalise the syntax and semantics of type theory. Slightly simplified, they define a set Ctxt of contexts, a family Ty Ctxt Set of types in a given context, and a family Term Γ Ctxt Ty Γ Set of terms of a given type. Let us for simplicity only consider contexts and types. The set Ctxt of contexts has two constructors

ε Ctxt ,
cons Γ Ctxt Ty Γ Ctxt ,

corresponding to the empty context and extending a context Γ with a new type. In our simplified setting, Ty Ctxt Set has the following constructors

’set’ Γ Ctxt Ty Γ ,
Π Γ Ctxt A Ty Γ Ty cons Γ, A  Ty Γ .

The first constructor states that ’set’ is a type in any context. The second constructor Π is the constructor for the Π-type: If we have a type A in a context Γ, and another type B in Γ extended by A (corresponding to abstracting a variable of type A), then Π A, B is also a type in Γ.

Note how the constructor cons for Ctxt has an argument of type Ty Γ , even though Ty is indexed by Ctxt. It is also worth noting that Π has an argument of type Ty cons Γ, A , i.e. we are using the constructor for Ctxt in the index of Ty. In general, we could of course imagine an argument of type Ty cons cons Γ, A , A^{}etc.

Both Danielsson [5] and Chapman [4] have used the proof assistant Agda [17] as a framework for their formalisation. Agda supports inductive-inductive (and inductive-recursive) definitions via the mutual keyword. However, the theory behind Agda is unclear, especially in relation to mutual definitions. For example, Agda allows the definition of a universe U à la Tarski, with a code u U for itself, i.e. T u U. This does not necessarily mean that Agda is inconsistent by Girard’s paradox, as, if we also demand closure under Π or Σ, the positivity checker rejects the code. However the consistency of Agda is by no means clear.

Nevertheless, Agda is an excellent tool for trying out ideas. We have formalised our theory in Agda, and this formalisation can be found on the authors’ home pages [14].

Acknowledgements We wish to thank Phillip James and the anonoymous referees of this and previous versions of this article for their helpful comments.

2 Type Theoretic Preliminaries

We work in a type theory with at least two universes Set and Type, with Set Type and if A Set then A Type. Both Set and Type are closed under dependent function types, written x A B (sometimes denoted Πx A B), where B is a set or type depending on x A. Abstraction is written as λx A.e, where e B depending on x A, and application as f x . Repeated abstraction and application are written as λx_{1} A_{1} … x_{k} A_{k}.e and f x_{1}, …, x_{k} . If the type of x can be inferred, we simply write λx.e as an abbreviation. Furthermore, both Set and Type are closed under dependent sums, written x A B (sometimes denoted Σx A B), where B is a set or type depending on x A, with pairs a, b , where a A and b B x a . We also have β- and η-rules for both dependent function types and sums.

We need an empty type 0 Set, with elimination !_{A} x 0 A for every A 0 Set. We need a unit type 1 Set, with unique element 1. We include an η-rule stating that if x 1, then x 1. Moreover, we include a two element set 2 Set, with elements tt 2, ff 2 and elimination constant if then else a 2 A tt A ff A a where A i Type for i 2.

With if then else and dependent products, we can now define the disjoint union of two sets A B x 2 if x then A else B with constructors inl λa A. tt, a and inr λb B. ff, b , and prove the usual formation, introduction, elimination and equality rules. We write A_{0} A_{1} … A_{n} for A_{0} A_{1} … A_{n} and in_{k} a for the kth injection inl inr^{k} a (with special case in_{n} a = inr^{n} a ).

Using (the derived) elimination rules for , we can, for A, B Set, C A B Type and f a A C inl a , g b B C inr b , define the case distinction f g c A B C c with equality rules

f g inl a f a ,
f g inr b g b .

We will use the same notation even when C does not depend on c A B, and we will write f g A B C D, where f A C, g B D, for inl f inr g .

Intensional type theory in Martin-Löf’s logical framework extended with dependent products and 0, 1 and 2 has all the features we need. Thus, our development could, if one so wishes, be seen as an extension of the logical framework.

3 From Inductive to Inductive-inductive Definitions

Let us first, before we move on to inductive-inductive definitions, informally consider how to formalise a simultaneous (generalised) inductive definition of two sets A and B, given by constructors

intro_{A} Φ_{A} A, B A intro_{B} Φ_{B} A, B B

where Φ_{A} and Φ_{B} are strictly positive in the following sense:

– The constant Φ A, B 1 is strictly positive. It corresponds to an introduction rule with no arguments (or more precisely, the trivial argument x 1).

– If K is a set and Ψ_{x} is strictly positive, depending on x K, then Φ A, B x K Ψ_{x} A, B , corresponding to the addition of a non-inductive premise, is strictly positive. So intro_{A} has one non-inductive argument x K, followed by the arguments given by Ψ_{x} A, B .

– If K is a set and Ψ is strictly positive, then Φ A, B K A Ψ A, B is strictly positive. This corresponds to the addition of a premise inductive in A, where K corresponds to the hypothesis of this premise in a generalised inductive definition. So intro_{A} has one inductive argument f K A, followed by the arguments given by Ψ A, B .

– Likewise, if K is a set and Ψ is strictly positive, then Φ A, B K B Ψ A, B is strictly positive. This is similar to the previous case.

In an inductive-inductive definition, B is indexed by A, so the constructor for B is replaced by

intro_{B} a Φ_{B} A, B B i_{A,B} a

for some index i_{A,B} a A which might depend on a Φ_{B} A, B . Furthermore, we must modify the inductive case for B to specify an index as well. This index can (and usually does) depend on earlier inductive arguments, so that the new inductive cases become

– If K is a set, and Ψ_{f} is strictly positive, depending^{2} on f K A only in indices for B, then Φ A, B f K A Ψ_{f} A, B is strictly positive.

– If K is a set, i_{A,B} K A is a function and Ψ_{f} is strictly positive, depending on f x K B i_{A,B} x only in indices for B, then Φ A, B f x K B i_{A,B} x Ψ_{f} A, B is strictly positive.

In what way can the index depend on f? Before we know the constructor for A, we do not know any functions with codomain A, so the index can only depend directly on f (e.g. B f x ). When we define the constructor for B, the situation is similar, but now we know one function into A, namely intro_{A} Φ_{A} A, B A, so that the index could be e.g. intro_{A} f x , b . (Our approach could also be straightforwardly extended to allow several constructors for A, where later constructors make use of earlier ones.)

4 An Axiomatisation

We proceed as in Dybjer and Setzer [9] and introduce a datatype of codes for constructors. In other words, we define a type SP (for strictly positive) whose elements represent the inductively defined sets, together with a way to construct the real sets from the representing codes. However, as we have two sets A and B with different roles, we need two types SP_{A} and SP_{B} of codes.

What do we need to know in order to reconstruct the inductively defined sets? A moment’s thought shows that all we need is the domain of the constructors, and in the case of B, we also need the index of the codomain of the constructor. From this, we can write down the introduction rules, and the elimination rules should be determined by these (see e.g. [6]). Thus, the codes in SP_{A} and SP_{B} will

2 The somewhat vague and informal phrase “depending on f only in indices for B” will be given an exact meaning in the formalisation in the next section.

be codes for the domain of the constructors, and we will have functions Arg_{A}, Arg_{B} that map the code to the domain it represents. For B, there will also be a function Index_{B} that gives the index (in A) of the codomain of the constructor.

We will have special codes A-ind, B-ind for arguments that are inductive in A and B respectively. In the case of B-ind, we also need to specify an index, which might depend on earlier arguments. For instance, the index p of the type of the second argument for the extension constructor

extension p Platform Building p Platform

depends on the first argument. How can we specify this index in the code? We cannot make use of the sets A and B themselves, since they are to be defined, but we can refer to their existence. We will introduce parameters A_{ref}, B_{ref} that get updated during the construction of the code. A_{ref} determines the elements of A that we can refer to, and B_{ref} determines the elements b of B, together with the index a such that b B a . At the beginning, we cannot refer to any arguments, and so A_{ref} B_{ref} 0. For example, after having written down the first argument p Platform, A_{ref} would be extended to include also an element representing p, which we use when writing down the type of the second argument, Building p .

4.1 SP_{A} and Arg_{A}

The above discussion leads us to the following formation rule for SP_{A}:

A_{ref} Set B_{ref} Set
SP_{A} A_{ref}, B_{ref} Type

A_{ref} and B_{ref} can be any sets. The codes for inductive-inductive definitions will however be elements from SP_{A}^{}SP_{A} 0, 0 , i.e. codes that do not refer to any elements to start with.

The introduction rules for SP_{A} reflect the rules for strict positivity in Section 3. The rules are as follows (we suppress the global premise A_{ref}, B_{ref} Set):

nil_{A} SP_{A} A_{ref}, B_{ref}

K Set γ K SP_{A} A_{ref}, B_{ref}
nonind K, γ SP_{A} A_{ref}, B_{ref}
K Set γ SP_{A} A_{ref} K, B_{ref}

A-ind K, γ SP_{A} A_{ref}, B_{ref}

K Set h_{index} K A_{ref} γ SP_{A} A_{ref}, B_{ref} K
B-ind K, h_{index}, γ SP_{A} A_{ref}, B_{ref}

The code nil_{A} represents a trivial constructor (the base case). The code nonind K, γ is meant to represent a noninductive argument x K, with the rest of the arguments given by γ x . The code A-ind K, γ is meant to represent a (generalised) inductive argument of type K A, with the rest of the arguments given by γ. Finally, the code B-ind K, h_{index}, γ represents an inductive argument of type x K B i x , where the index i x is determined by h_{index}, and the rest of the arguments are given by γ. For instance, a constructor

c x 2 ℕ A A

has the code γ_{c} nonind 2, λx.A-ind ℕ, nil_{A} . Note how 2 and ℕ appear in the code. We will see an example of the slightly more complicated constructor B-ind later.

We will now define Arg_{A}, which maps a code to the domain of the constructor it represents. Arg_{A} will need to take arbitrary A Set and B A Set as parameters to use as A and B in the inductive arguments, since we need Arg_{A} to define the A and B we want. We will then have axioms stating that for every code γ SP_{A}^{}, there are sets A_{γ}, B_{γ} closed under Arg_{A}, i.e. there is a constructor intro_{A} Arg_{A} γ, A_{γ}, B_{γ} A_{γ}. Arg_{A} has formation rule

A_{ref}, B_{ref} Set
γ SP_{A} A_{ref}, B_{ref}

{A Set \atop B A Set}

rep_{A} A_{ref} A
rep_{index} B_{ref} A
rep_{B} x B_{ref} B rep_{index} x
Arg_{A} A_{ref}, B_{ref}, γ, A, B, rep_{A}, rep_{index}, rep_{B} Set

The function rep_{A} translates elements in A_{ref} into the real elements they represent in A. Elements in B_{ref} represent elements b from B, but also elements from A, as we also need to store the index a such that b B a . This index is given by rep_{index}, and rep_{B} gives the real element in B rep_{index} y an element y B_{ref} represents.

We are actually only interested in Arg_{A} for codes γ SP_{A}^{}for inductiveinductive definitions (i.e. with A_{ref} B_{ref} 0), but we need to consider arbitrary A_{ref}, B_{ref} for the intermediate codes. For γ SP_{A}^{}, we can define a simplified version Arg_{A}^{}SP_{A}^{}A Set B A Set Set by Arg_{A}^{}γ, A, B Arg_{A} 0, 0, γ, A, B,!_{A},!_{A},!_{B !_{A}} . (Recall that !_{X} x 0 X is the function given by ex falso quodlibet.)

The definition of Arg_{A} also follows the rules for strict positivity in Section 3. We will, for readability, write “ ” for arguments which are simply passed on in the recursive call.

The code nil_{A} represents the constructor with no argument (i.e. a trivial argument of type 1):

Arg_{A} A_{ref}, B_{ref}, nil_{A}, A, B, rep_{A}, rep_{index}, rep_{B} 1

The code nonind K, γ represents one non-inductive argument k K, with the rest of the arguments given by the code γ (depending on k K):

Arg_{A} A_{ref}, B_{ref}, nonind K, γ , A, B, rep_{A}, rep_{index}, rep_{B}

k K Arg_{A} , , γ k , , , , ,

The code A-ind K, γ represents one generalised inductive argument j K A, with the rest of the arguments given by the code γ. In the following arguments, A_{ref} has now been updated to A_{ref} K, where elements in the old A_{ref} are mapped to A by the old rep_{A}, and elements in K are mapped to A by j. In effect, this means that we can refer to j k for k K in the following arguments.

Arg_{A} A_{ref}, B_{ref}, A-ind K, γ , A, B, rep_{A}, rep_{index}, rep_{B}

j K A Arg_{A} A_{ref} K, , γ, , , rep_{A} j, ,

Finally, the code B-ind K, h_{index}, γ represents one generalised inductive argument j x K B rep_{A} h_{index} x , where rep_{A} h_{index} picks out the index of the type of j x . This time, we can refer to more elements in B afterwards, namely those given by j (and indices given by rep_{A} h_{index}):

Arg_{A} A_{ref}, B_{ref}, B-ind K, h_{index}, γ , A, B, rep_{A}, rep_{index}, rep_{B}

j k K B rep_{A} h_{index} k

Arg_{A} , B_{ref} K, γ, , , , rep_{index} rep_{A} h_{index} , rep_{B} j

Let us take a look at the constructor

extension p Platform Building p Platform

again. It would have the code γ_{ext} A-ind 1, B-ind 1, λ .p̂, nil_{A} SP_{A}^{}where p̂ inr is the element in A_{ref} 0 1 representing the element introduced by A-ind. We have

Arg_{A}^{}γ_{ext}, Platform, Building p 1 Platform 1 Building p 1

which is isomorphic to the domain of extension thanks to the η-rules for 1 (i.e. X 1 X and X X 1).

4.2 Towards SP_{B}

If we did not want to use constructors for A as indices for B, like for example Building extension p, b , we could construct SP_{B} in more or less the same way as SP_{A} (this corresponds to choosing k 0 below). However, in general we do want to use constructors as indices, hence we have some more work to do. What do we need to know for such a constructor index? We need to know that we want to use a constructor, but that can be encoded in the code. We also need a way to specify the arguments to the constructor, i.e. we need to represent an element of Arg_{A}^{}γ, A, B ! If we want to use nested constructors (e.g. extension extension p, b , b^{}), we also need to be able to represent elements in Arg_{A}^{}γ, Arg_{A}^{}γ, A, B_{0} , B_{1} etc.

The idea is to represent elements in Arg_{A}^{}γ, A, B by corresponding elements in “Arg_{A}^{}γ, A_{ref}, B_{ref} ”. However, we must first reconstruct the structure of A_{ref}, B_{ref} as a family, i.e. we will construct \overline{A_{ref}} Set, \overline{B_{ref}} \overline{A_{ref}} Set, together with functions \overline{rep_{A}} \overline{A_{ref}} A and \overline{rep_{B}} x \overline{A_{ref}} \overline{B_{ref}} x B \overline{rep_{A}} x . Then, we will show that \overline{rep_{A}} and \overline{rep_{B}} can be lifted to a map lift^{}\overline{rep_{A}}, \overline{rep_{B}} Arg_{A}^{}γ, \overline{A_{ref}}, \overline{B_{ref}} Arg_{A}^{}γ, A, B , so that elements in Arg_{A}^{}γ, \overline{A_{ref}}, \overline{B_{ref}} indeed can represent elements in Arg_{A}^{}γ, A, B . The process can then be iterated to represent elements in Arg_{A}^{}γ, Arg_{A}^{}γ, A, B_{0} , B_{1} etc.

\overline{A_{ref}} should consist of representatives \overline{a} for elements a in A, and \overline{B_{ref}} \overline{a} should consist of representatives for elements in B a . The representative \overline{a} could either be from A_{ref} (with a rep_{A} \overline{a} ), in which case we do not know any elements in B a , or from B_{ref} (with a rep_{index} \overline{a} ), in which case we know a single element in B a , namely rep_{B} \overline{a} . Therefore, for A_{ref}, B_{ref} Set, we define

\overline{A_{ref}} A_{ref} B_{ref} , \overline{B_{ref}} λx.0 λx.1 ,

i.e. \overline{B_{ref}} inl a 0 and \overline{B_{ref}} inr b 1.

Mapping representatives in \overline{A_{ref}} to the elements they represent in A is now easy: we map inl \overline{a} \overline{A_{ref}} to rep_{A} \overline{a} and inr \overline{a} to rep_{index} \overline{a} . For \overline{B_{ref}}, we want to map representatives in \overline{B_{ref}} \overline{a} to the elements they represent in B a . However, we only have to consider \overline{B_{ref}} inr x 1, as there are no elements

in \overline{B_{ref}} inl x  0. We map  \overline{B_{ref}} inr \overline{a} to rep_{B} \overline{a} . To sum up, we can
define maps \overline{rep_{A}}  \overline{A_{ref}} A, \overline{rep_{B}} x \overline{A_{ref}}  \overline{B_{ref}} x B \overline{rep_{A}} x by

\overline{rep_{A}} rep_{A} rep_{index} and \overline{rep_{B}} λx.!_{B !_{A}} λx .rep_{B} x .

We now want to lift these maps to a map rep_{A,1} Arg_{A}^{}γ, \overline{A_{ref}}, \overline{B_{ref}} Arg_{A}^{}γ, A, B . This is made possible by the following more general result for arbitrary families A, B, A^{}, B^{}with respective representing functions rep_{A}, rep_{A}^{}etc. Assume we have maps g A A^{}, g^{}x A B x B^{}g x that respect the translations rep_{A} and rep_{A}^{}, i.e. we have a proof p that g rep_{A} x rep_{A}^{}x for all x A_{ref}. Then we can lift g to a map

lift g, g^{}, p Arg_{A} A_{ref}, B_{ref}, γ, A, B, rep_{A}, rep_{index}, rep_{B} Arg_{A} A_{ref}, B_{ref}, γ, A^{}, B^{}, rep_{A}^{}, rep_{index}^{}, rep_{B}^{}.

To avoid using the identity type when constructing lift, we will use a specialised version of Leibniz equality p x A_{ref} B^{}g rep_{A} x B^{}rep_{A}^{}x for the proof that g rep_{A} x rep_{A}^{}x . Under the assumption that γ SP_{A} A_{ref}, B_{ref} , and with A, B, rep_{A}, rep_{index}, rep_{B} as above, and A^{}, B^{}, rep_{A}^{}, rep_{index}^{}, rep_{B}^{} analogously, we now have formation rule

lift A_{ref}, B_{ref}, γ, A, B, rep_{A}, rep_{index}, rep_{B}, A^{}, B^{}, rep_{A}^{}, rep_{index}^{}, rep_{B}^{} g A A^{}g^{}x A B x B^{}g x

p x A_{ref} B^{}g rep_{A} x B^{}rep_{A}^{}x
Arg_{A} A_{ref}, B_{ref}, γ, A, B, rep_{A}, rep_{index}, rep_{B}
Arg_{A} A_{ref}, B_{ref}, γ, A^{}, B^{}, rep_{A}^{}, rep_{index}^{}, rep_{B}^{}

with defining equations (we write “ ” for passed on arguments in the recursive call)

lift A_{ref}, B_{ref}, nil_{A}, rep_{A}, rep_{index}, rep_{B}, rep_{A}^{}, rep_{index}^{}, rep_{B}^{}, g, g^{}, p,

lift A_{ref}, B_{ref}, nonind K, γ , rep_{A}, rep_{index}, rep_{B}, rep_{A}^{}, rep_{index}^{}, rep_{B}^{}, g, g^{}, p, k, y

k, lift , , γ k , , , , , , , , , , y

lift A_{ref}, B_{ref}, A-ind K, γ , rep_{A}, rep_{index}, rep_{B}, rep_{A}^{}, rep_{index}^{}, rep_{B}^{}, g, g^{}, p, j, y

g j, lift A_{ref} K, , γ, rep_{A} j, , , rep_{A}^{}g j , , , , , p λk, b.b , y lift A_{ref}, B_{ref}, B-ind K, h_{index}, γ , rep_{A}, rep_{index}, rep_{B}, rep_{A}^{}, rep_{index}^{}, rep_{B}^{}, g, g^{}, p, j, y

λk.p h_{index} k , g^{}rep_{A} h_{index} k , j k ,

lift , B_{ref} K, γ, , rep_{index} rep_{A} h_{index} , rep_{B} j, , rep_{index}^{}rep_{A}^{}h_{index} , rep_{B}^{}λk.p h_{index} k , g^{}rep_{A} h_{index} k , j k , , , , y .

Note how the proof p x A_{ref} B^{}g rep_{A} x B^{}rep_{A}^{}x gets updated to p λk b.b when A_{ref} is extended to A_{ref} K. For γ SP_{A}^{}, g A A^{}, g^{}x A B x B^{}g x , we define

lift^{}γ, A, B, A^{}, B^{}, g, g^{}Arg_{A}^{}γ, A, B Arg_{A}^{}γ, A^{}, B^{}

by

lift^{}γ, A, B, A^{}, B^{}, g, g^{}, a lift 0, 0, γ, A, B,!_{A},!_{A},!_{B !_{A}}, A^{}, B^{},!_{A^{}},!_{A^{}},!_{B^{}}, g, g^{}, triv, a .

where triv x 0 B^{}g rep_{A} x B^{}rep_{A}^{}x is the trivial proof supplied by ex falso quodlibet.

In our specific case, let for γ SP_{A}^{}, A_{ref}, B_{ref} Set and rep_{A} A_{ref} A, rep_{index} B_{ref} A, rep_{B} b B_{ref} B rep_{index} b

\overline{arg_{A}} γ, A_{ref}, B_{ref} Arg_{A}^{}γ, \overline{A_{ref}}, \overline{B_{ref}} ,
\overline{lift} rep_{A}, rep_{index}, rep_{B} lift^{}\overline{rep_{A}}, \overline{rep_{B}}  \overline{arg_{A}} γ, A_{ref}, B_{ref} Arg_{A}^{}γ, A, B .

We can now represent elements in Arg_{A}^{}γ, A, B by elements in \overline{arg_{A}} γ, A_{ref}, B_{ref} via rep_{A,1} \overline{lift} rep_{A}, rep_{index}, rep_{B} . For example, consider γ_{ext} once again. Suppose that we want to specify an element of Arg_{A}^{}γ_{ext}, Platform, Building , i.e. an argument to the extension constructor, and we have A_{ref} B_{ref} 0 1. \overline{A_{ref}} then consists of two elements, namely p̂ inl inr and { \atop pb} inr inr . We have that \overline{B_{ref}} p̂ 0 and \overline{B_{ref}} { \atop pb} 1. In other words, there is only one element { \atop pb} { \atop pb}, , of Arg_{A}^{}γ_{ext}, \overline{A_{ref}}, \overline{B_{ref}} , and rep_{A,1} { \atop pb} rep_{index} { \atop pb} , rep_{B} { \atop pb} , p, b, where rep_{index} { \atop pb} p Platform, rep_{B} { \atop pb} b Building p .

Let us now generalise this to multiple nestings of constructors. Given a sequence { \atop B_{ref n}} B_{ref, 0}, B_{ref, 1}, …, B_{ref, n 1} of sets, we iterate \overline{arg_{A}} by defining

arg_{A}^{0} γ, A_{ref}, { \atop B_{ref 0}} A_{ref} ,
arg_{A}^{n 1} γ, A_{ref}, { \atop B_{ref n 1}}  \overline{arg_{A}} γ, _{i 0}^{n} arg_{A}^{i} γ, A_{ref}, { \atop B_{ref i}} , B_{ref, n} .

arg_{A}^{k} should represent k nested constructors. The corresponding iteration of Arg_{A}^{} justifying this, is

Arg_{A}^{0} γ, A, { \atop B_{0}} A ,
Arg_{A}^{n 1} γ, A, { \atop B_{n 1}} Arg_{A}^{}γ, _{i 0}^{n} Arg_{A}^{i} γ, A, { \atop B_{i}} , _{i 0}^{n} B_{i} ,

where { \atop B_{n}} is a sequence B_{0}, B_{1}, …, B_{n 1} of families B_{i} Arg_{A}^{i} γ_{A}, A, { \atop B_{i 1}} Set.

Now assume that we have a sequence { \atop B_{ref n}} of sets and a sequence { \atop B_{n}} of families of sets as above. If we now in addition to rep_{A} A_{ref} A, also have functions rep_{index,i} B_{ref, i} Arg_{A}^{i} γ, A, B , and rep_{B,i} x B_{ref, i} B_{i} rep_{index,i} x (we will assume all this when working with SP_{B}), we can now construct functions rep_{A,n} arg_{A}^{n} γ, A_{ref}, { \atop B_{ref}} Arg_{A}^{n} γ, A, B with the help of lift^{}by defining

rep_{A,0}  rep_{A} ,
rep_{A,n 1}  \overline{lift} ∥_{i 0}^{n} rep_{A,i}, in_{n} rep_{index,n}, rep_{B,n} .

Note that rep_{A,1} as defined earlier is an instance of this definition.

4.3 SP_{B}, Arg_{B} and Index_{B}

The datatype SP_{B} of codes for constructors for B is just as SP_{A}, but with two differences: first, we can refer to constructors of A (so we will need a code γ_{A} SP_{A}^{}to know their form, and sets B_{ref, 0}, B_{ref, 1}, … B_{ref, i}, … to represent elements in B indexed by i nested constructors). Second, we also need to specify an index for the codomain of the constructor (so we will store this index in the nil_{B} code).

All constructions from now on will be parameterised on the maximum number k of nested constructors for A that we are using, so we are really introducing SP_{B,k}, Arg_{B,k} etc. However, we will work with an arbitrary k but suppress it as a premise. With this in mind, we have formation rule

γ_{A} SP_{A}^{}A_{ref} Set B_{ref, 0}, B_{ref, 1}, …, B_{ref, k} Set
SP_{B} γ_{A}, A_{ref}, B_{ref, 0}, B_{ref, 1}, …, B_{ref, k} Type

Let SP_{B}^{}γ_{A} SP_{B} γ_{A}, 0, 0, …, 0 for γ_{A} SP_{A}^{}be the code of inductiveinductive definitions.

The introduction rules for SP_{B} are very similar to the rules for SP_{A}, but now we specify an index in nil_{B}, and we have k 1 rules B_{0}-ind, …, B_{k}-ind corresponding to how many nested constructors for A we want to use:

a_{index} _{i 0}^{k} arg_{A}^{i} γ_{A}, A_{ref}, { \atop B_{ref}}
nil_{B} a_{index} SP_{B} γ_{A}, A_{ref}, B_{ref, 0}, …, B_{ref, k}

K Set γ K SP_{B} γ_{A}, A_{ref}, B_{ref, 0}, …, B_{ref, k}
nonind K, γ SP_{B} γ_{A}, A_{ref}, B_{ref, 0}, …, B_{ref, k}
K Set γ SP_{B} γ_{A}, A_{ref} K, B_{ref, 0}, …, B_{ref, k}
A-ind K, γ SP_{B} γ_{A}, A_{ref}, B_{ref, 0}, …, B_{ref, k}

K Set

h_{index} K arg_{A}^{ℓ} γ_{A}, A_{ref}, { \atop B_{ref}}
γ SP_{B} γ_{A}, A_{ref}, B_{ref, 0}, …, B_{ref, ℓ} K, …, B_{ref, k}
B_{ℓ}-ind K, h_{index}, γ SP_{B} γ_{A}, A_{ref}, B_{ref, 0}, …, B_{ref, k}

The rules nil_{B}, nonind and A-ind have the same meaning as before, but B-ind has been split up into several rules. The code B_{ℓ}-ind K, h_{index}, γ represents an inductive argument of type x K B i_{ℓ} x with the index i_{ℓ} x , using ℓ nested constructors for A, given by h_{index}. Hence h_{index} has codomain arg_{A}^{ℓ} γ_{A}, A_{ref}, { \atop B_{ref}} . For this to work, we will need k 1 families B_{i} Arg_{A}^{i} γ_{A}, A, { \atop B_{i 1}} Set to interpret these nested constructor indices, together with functions rep_{index,i} B_{ref, i} Arg_{A}^{i} γ, A, { \atop B_{i 1}} and rep_{B,i} x B_{ref, i} B_{i} rep_{index,i} x to map elements to the real elements they represent. Recall that from this and rep_{A} A_{ref} A, we can construct functions rep_{A,ℓ} arg_{A}^{ℓ} γ, A_{ref}, { \atop B_{ref}} Arg_{A}^{ℓ} γ, A, B .

Every case of Arg_{B} is the same as the corresponding case for Arg_{A}, except for B_{ℓ}-ind, where B has been replaced by B_{ℓ} and rep_{A} by rep_{A,ℓ} (we write “ ” for passed on arguments and “ ” for passed on sequents of arguments in the recursive call):

Arg_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, nil_{B} a_{index} , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B} 1

Arg_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, nonind K, γ , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}

k K Arg_{B} , , , γ k , , , , ,

Arg_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, A-ind K, γ , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}

j K A Arg_{B} , A_{ref} K, , γ, , , rep_{A} j, ,

Arg_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, B_{ℓ}-ind K, h_{index}, γ , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}

j k K B_{ℓ} rep_{A,ℓ} h_{index} k

Arg_{B} , , , B_{ref, ℓ} K, , γ, , , , , rep_{index,ℓ} rep_{A,ℓ} h_{index} , , , rep_{B,ℓ} j,

The last missing piece is now Index_{B}, which to each b Arg_{B}^{}γ_{A}, γ_{B}, A, B assigns the index a such that the element constructed from b is in B a . With γ_{A}, A_{ref}, B_{ref, i} etc as above, Index_{B} has formation rule

Index_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, γ_{B}, A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}

Arg_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, γ_{B}, A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B} _{i 0}^{k} Arg_{A}^{i} γ_{A}, A, B .

Index_{B} will take a_{index} _{i 0}^{k} arg_{A}^{i} γ_{A}, A_{ref}, { \atop B_{ref}} which is stored in nil_{B} and map it to the index element it represents in _{i 0}^{k} Arg_{A}^{i} γ_{A}, A, B . For other codes, it will follow exactly the same pattern as Arg_{B}.

Index_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, nil_{B} a_{index} , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B},  ∥_{i 0}^{k} rep_{A,i} a_{index}

Index_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, nonind K, γ , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, k, y Index_{B} , , , γ k , , , , , , y

Index_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, A-ind K, γ , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, j, y Index_{B} , A_{ref} K, , γ, , , rep_{A} j, , , y

Index_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, B_{n}-ind K, h, γ , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, j, y Index_{B} , , , B_{ref, n} K, , γ, , , , , rep_{index,n} rep_{A,n} h , , , rep_{B,n} j, , y .

For codes γ_{B} SP_{B}^{}γ_{A} for inductive-inductive definitions, let

Arg_{B}^{}γ_{A}, γ_{B}, A, B Arg_{B} γ_{A}, 0, 0, γ_{B}, A, B,!_{A}, { \atop !_{Arg_{A}}}, { \atop !_{B !}} ,
Index_{B}^{}γ_{A}, γ_{B}, A, B Index_{B} γ_{A}, 0, 0, γ_{B}, A, B,!_{A}, { \atop !_{Arg_{A}}}, { \atop !_{B !}} .

As an illustration, let us consider the constructor

hangingUnder p Platform b Building p Building extension p, b .

Here it is interesting to see that the index of the codomain of the constructor uses the constructor extension, so it will be represented by an element from \overline{arg_{A}} γ_{ext}, A_{ref}, B_{ref} . We end up with the code γ_{hu} A-ind 1, B_{0}-ind 1, λ .p̂, nil_{B} in_{1} { \atop pb} , where p̂ inr and { \atop pb} inr inr , , . (The reader is invited to check that { \atop pb} \overline{arg_{A}} γ_{ext}, A_{ref}, B_{ref} at that point in the construction of γ_{hu}.) We get

Arg_{B}^{}γ_{ext}, γ_{hu}, P, B p 1 P b 1 B p 1

and Index_{B}^{}γ_{ext}, γ_{hu}, P, B, p, b, in_{1} p, b, .

4.4 Formation and Introduction Rules

We are now ready to give the formal formation and introduction rules for A and B. They all have the common premises γ_{A} SP_{A}^{}and γ_{B} SP_{B}^{}γ_{A} , which will be omitted.

Formation rules:

A_{γ_{A},γ_{B}} Set , B_{γ_{A},γ_{B}} A_{γ_{A},γ_{B}} Set .

Introduction rule for A_{γ_{A},γ_{B}}:

a Arg_{A}^{}γ_{A}, A_{γ_{A},γ_{B}}, B_{γ_{A},γ_{B}}
intro_{A} a A_{γ_{A},γ_{B}}

For the introduction rule for B_{γ_{A},γ_{B}}, we need some preliminary definitions. We

have B_{γ_{A},γ_{B}} A_{γ_{A},γ_{B}} Set, but need B_{i} Arg_{A}^{i} γ_{A}, A_{γ_{A},γ_{B}}, { \atop B_{i 1}} Set for

0 i k to give to Arg_{B}^{}. We can assemble such B_{i}’s from B_{γ_{A},γ_{B}}, intro_{A} and lift^{}. To do so, define in a step by step manner

intro_{n} Arg_{A}^{n} γ_{A}, A_{γ_{A},γ_{B}}, B_{0}, …, B_{n 1} A_{γ_{A},γ_{B}}
B_{n} Arg_{A}^{n} γ_{A}, A_{γ_{A},γ_{B}}, B_{0}, …, B_{n 1} Set

(i.e. introduce first intro_{0}, B_{0}, then intro_{1}, B_{1} and so on) by

intro_{0} id
intro_{n 1} intro_{A} lift^{}_{i 0}^{n} intro_{i}, _{i 0}^{n} λa.id
B_{i} x B_{γ_{A},γ_{B}} intro_{i} x

Hence the introduction rule for B_{γ_{A},γ_{B}} can be given as:

b Arg_{B}^{}γ_{A}, γ_{B}, A_{γ_{A},γ_{B}}, B_{γ_{A},γ_{B}}, B_{1}, …, B_{k}
intro_{B} b B_{γ_{A},γ_{B}} \overline{index} b

where \overline{index} takes the index in _{i 1}^{k} Arg_{A}^{i} γ_{A}, A_{γ_{A},γ_{B}}, B returned by Index_{B}^{} and applies the right intro_{i} to it, i.e.

\overline{index} _{i 0}^{k} intro_{i} Index_{B}^{}γ_{A}, γ_{B}, A_{γ_{A},γ_{B}}, B_{0}, …, B_{k} .

4.5 Elimination rules

The intuitive idea behind the elimination rules is the following: we have E A Set and E^{}a A B a Set, and would like to construct functions f a A E a and g a A b B a E^{}a, b . f and g might very well be mutually recursive, since A and B are mutually defined. The elimination rules now state that if we can define functions f^{}a Arg_{A}^{}γ_{A}, A, B E intro_{A} a and g^{}b Arg_{B}^{}γ_{A}, γ_{B}, A, B E^{}\overline{index} b , intro_{B} b , given that we already know the value of (mutual) recursive calls, we have functions f a A E a and g a A b B a E^{}a, b .

To this end, let us define sets IH_{A} and IH_{B} of inductive hypotheses, together with maps mapIH_{A} Arg_{A}^{}γ_{A}, A, B IH_{A}, mapIH_{B} Arg_{B}^{}γ_{A}, γ_{B}, A, B IH_{B} which take care of the recursive call.

More specifically, if A_{ref}, B_{ref}, γ_{A}, A, B, rep_{A}, rep_{index}, rep_{B} are as in the premises for Arg_{A}, and E A Set, E^{}a A B a Set, then

IH_{A} A_{ref}, B_{ref}, γ_{A}, A, B, rep_{A}, rep_{index}, rep_{B}, E, E^{} Arg_{A} A_{ref}, B_{ref}, γ_{A}, A, B, rep_{A}, rep_{index}, rep_{B} Set and

mapIH_{A} A_{ref}, B_{ref}, γ_{A}, A, B, rep_{A}, rep_{index}, rep_{B}, E, E^{}

R a A E a R^{}a A b B a E^{}a, b

a Arg_{A} A_{ref}, B_{ref}, γ_{A}, A, B, rep_{A}, rep_{index}, rep_{B}

IH_{A} A_{ref}, B_{ref}, γ_{A}, A, B, rep_{A}, rep_{index}, rep_{B}, E, E^{}, a .

IH_{A} is defined as follows:

IH_{A} A_{ref}, B_{ref}, nil_{A}, A, B, rep_{A}, rep_{index}, rep_{B}, E, E^{}, 1

IH_{A} A_{ref}, B_{ref}, nonind K, γ , A, B, rep_{A}, rep_{index}, rep_{B}, E, E^{}, k, y

IH_{A} , , γ k , , , , , , , , y

IH_{A} A_{ref}, B_{ref}, A-ind K, γ , A, B, rep_{A}, rep_{index}, rep_{B}, E, E^{}, j, y

k K E j k IH_{A} A_{ref} K, , γ, , , rep_{A} j, , , , , y

IH_{A} A_{ref}, B_{ref}, B-ind K, h_{index}, γ , A, B, rep_{A}, rep_{index}, rep_{B}, E, E^{}, j, y

k K E^{}rep_{A} h_{index} k , j k
IH_{A} , B_{ref} K, γ, , , , rep_{index} rep_{A} h_{index} , rep_{B} j, , , y .

mapIH_{A} maps a Arg_{A} γ_{A}, A, B to IH_{A} γ_{A}, A, B, a , given that we have functions R, R^{}for the recursive calls. It has the following defining equations:

mapIH_{A} A_{ref}, B_{ref}, nil_{A}, A, B, rep_{A}, rep_{index}, rep_{B}, E, E^{}, R, R^{},
mapIH_{A} A_{ref}, B_{ref}, nonind K, γ , A, B, rep_{A}, rep_{index}, rep_{B}, E, E^{}, R, R^{}, k, y

mapIH_{A} , , γ k , , , , , , , , , , y

mapIH_{A} A_{ref}, B_{ref}, A-ind K, γ , A, B, rep_{A}, rep_{index}, rep_{B}, E, E^{}, R, R^{}, j, y

R j, mapIH_{A} A_{ref} K, , γ, , , rep_{A} j, , , , , , , y

mapIH_{A} A_{ref}, B_{ref}, B-ind K, h, γ , A, B, rep_{A}, rep_{index}, rep_{B}, E, E^{}, R, R^{}, j, y

λk.R^{}rep_{A} h k , j k ,

mapIH_{A} , B_{ref} K, γ, , , , rep_{index} rep_{A} h , rep_{B} j, , , , , y .

We now repeat the process for IH_{B} and mapIH_{B}. This time, however, we have not one B A Set but k 1 families B_{i} Arg_{A}^{i} γ_{A}, A, { \atop B_{i 1}} Set, so we need k 1 families E_{i}^{}a Arg_{A}^{i} γ_{A}, A, B B_{i} a Set and k 1 functions R_{i}^{}a Arg_{A}^{i} γ_{A}, A, B b B_{i} a E_{i}^{}a, b . Otherwise, the pattern is the same.

The formation rules are as follows: if γ_{A}, A_{ref}, B_{ref, i}, γ_{B}, A, B_{i}, rep_{A},

f_{A,i}^{},f_{B,i}^{}are as before, and E A Set, E_{i}^{}a Arg_{A}^{i} γ_{A}, A, { \atop B_{i 1}} B_{i} a

Set, then

IH_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, γ_{A}, A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, E, { \atop E^{}}

Arg_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, γ_{B}, A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B} Set

and mapIH_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, γ_{B}, A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, E, { \atop E^{}}

R a A E a R_{0}^{}a A b B_{0} a E_{0}^{}a, b

R_{1}^{}a Arg_{A}^{1} γ_{A}, A, B_{0} b B_{1} a E_{1}^{}a, b

R_{k}^{}a Arg_{A}^{k} γ_{A}, A, B_{k 1} b B_{k} a E_{k}^{}a, b
b Arg_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, γ_{B}, A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}
IH_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, γ_{B}, A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, E, { \atop E^{}}, b .

We get the equations for IH_{B} and mapIH_{B} by changing IH_{A} and mapIH_{A} in more or less the same way we changed Arg_{A} to get Arg_{B}; in the B_{n}-ind case, we replace rep_{A} with rep_{A,n}, rep_{index} with rep_{index,n}, rep_{B} with rep_{B,n}, B with B_{n} and now also E^{}with E_{n}^{}and R^{}with R_{n}^{}.

IH_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, nil_{B} d , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, E, { \atop E^{}},  = 1
IH_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, nonind K, γ , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, E, { \atop E^{}}, k, y =
IH_{B} , , , γ k , , , , , , , , y
IH_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, A-ind K, γ , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, E, { \atop E^{}}, j, y  =

k K E j k IH_{B} , A_{ref} K, , γ, , , rep_{A} j, , , , , y

IH_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, B_{n}-ind K, h, γ , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, E, { \atop E^{}}, j, y =

k K E_{n}^{}rep_{A,n} h k , j k IH_{B} , , , B_{ref, n} K, , γ, , , , , rep_{index,n} rep_{A,n} h , , , f_{B,n}^{}j, , , , y .

mapIH_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, nil_{B} d , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, E, { \atop E^{}}, R, { \atop R^{}},  =
mapIH_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, nonind K, γ , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, E, { \atop E^{}}, R, { \atop R^{}}, k, y =
mapIH_{B} , , , γ k , , , , , , , , , , y
mapIH_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, A-ind K, γ , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, E, { \atop E^{}}, R, { \atop R^{}}, j, y  =

R j, mapIH_{B} , A_{ref} K, , γ, , , rep_{A} j, , , , , , , y

mapIH_{B} γ_{A}, A_{ref}, { \atop B_{ref}}, B_{n}-ind K, h, γ , A, B, rep_{A}, { \atop rep}_{index}, { \atop rep}_{B}, E, { \atop E^{}}, R, { \atop R^{}}, j, y =

λk.R_{n}^{}rep_{A,n} h k , j k ,

mapIH_{A} , , , B_{ref, n} K, , γ, , , , , rep_{index,A,n} rep_{A,n} h , , , rep_{B,B,n} j, , , , , , y .

We make the usual abbreviations

IH’_{A} γ_{A}, A, B, E, E^{}, a

IH_{A} 0, 0, γ_{A}, A, B,!_{A},!_{A},!_{B !}, E, E^{}, a

mapIH_{A}^{}γ_{A}, A, B, E, E^{}, R, R^{}, a mapIH_{A} 0, 0, γ_{A}, A, B,!_{A},!_{A},!_{B !}, E, E^{}, R, R^{}, a

IH’_{B} γ_{A}, γ_{B}, A, B, E, { \atop E^{}}, b

IH_{B} γ_{A}, 0, 0, γ_{B}, A, B,!_{A},!_{Arg_{A}}, { \atop !_{B !}}, E, { \atop E^{}}, b

mapIH_{B}^{}γ_{A}, γ_{B}, A, B, E, { \atop E^{}}, R, { \atop R^{}}, b

mapIH_{B} γ_{A}, 0, 0, γ_{B}, A, B,!_{A},!_{Arg_{A}}, { \atop !_{B !}}, E, { \atop E^{}}, R, { \atop R^{}}, b .

It is now time to introduce the elimination and equality rules for A_{γ_{A},γ_{B}} and B_{γ_{A},γ_{B}}. We have used the abbreviations B_{n} from Section 4.4, as well as a new abbreviation E_{n}^{}λa, b.E^{}intro_{n} a , b .

For E A_{γ_{A},γ_{B}} Set and E^{}a A_{γ_{A},γ_{B}} B_{γ_{A},γ_{B}} a Set, we have elimination rules (we have abbreviated A A_{γ_{A},γ_{B}}, B B_{γ_{A},γ_{B}})

g a Arg_{A}^{}γ_{A}, A, B IH’_{A} γ_{A}, A, B, E, E^{}, a E intro_{A} a

h b Arg_{B}^{}γ_{A}, γ_{B}, A, B_{0}, …, B_{k} IH’_{B} γ_{A}, γ_{B}, A, B, E, E_{0}^{}, …, E_{k}^{}, b E^{}\overline{index} b , intro_{B} b R_{A} g, h a A_{γ_{A},γ_{B}} E a

g a Arg_{A}^{}γ_{A}, A, B IH’_{A} γ_{A}, A, B, E, E^{}, a E intro_{A} a

h b Arg_{B}^{}γ_{A}, γ_{B}, A, B_{0}, …, B_{k} IH’_{B} γ_{A}, γ_{B}, A, B, E, E_{0}^{}, …, E_{k}^{}, b E^{}\overline{index} b , intro_{B} b R_{B} g, h a A_{γ_{A},γ_{B}} b B_{γ_{A},γ_{B}} a E^{}a, b

with equality rules (premises omitted)

R_{A} g, h, intro_{A} a g a, mapIH_{A}^{}γ_{A}, A, B, E, E^{}, R_{A} g, h , R_{B} g, h , a

R_{B} g, h, \overline{index} b , intro_{B} b h b, mapIH_{B}^{}γ_{A}, γ_{B}, A, B, E, { \atop E^{}}, R_{A} g, h , R_{B} g, h , b

4.6 Contexts and Types Again

As a final example, let us construct Ctxt and Ty from Section 1. With the abbreviation γ_{0} _{SP} γ_{1} nonind 2, λx.if x then γ_{0} else γ_{1} , we can encode several constructors into one. The codes for the contexts and types are

γ_{Ctxt} nil_{A} _{SP} A-ind 1, B-ind 1, λ .inr , nil_{A} SP_{A}^{}
γ_{’set’} A-ind 1, nil_{B} inl inr
γ_{Π}  A-ind 1, B_{0}-ind 1, λ .inr , B_{1}-ind 1, λ . ff, λ .inr inr ,
λ . , , nil_{B} inl inr
γ_{Ty} γ_{’set’} _{SP} γ_{Π} SP_{B}^{}γ_{Ctxt} .

We have Ctxt A_{γ_{Ctxt},γ_{Ty}} and Ty B_{γ_{Ctxt},γ_{Ty}} and we can define the usual constructors by

ε Ctxt  ’set’ Γ Ctxt Ty Γ
ε intro_{A} tt, ,  ’set’ Γ intro_{B} tt, λ .Γ , ,

cons Γ Ctxt Ty Γ Ctxt cons Γ, b intro_{A} ff, λ .Γ , λ .b , ,

Π Γ Ctxt A Ty Γ Ty cons Γ, A Ty Γ Π Γ, A, B intro_{B} ff, λ .Γ , λ .A , λ .B , .

5 A Set-theoretic Model

Even though SP_{A} and SP_{B} are straightforward (large) inductive definitions, this axiomatisation does not reduce inductive-inductive definitions to indexed inductive definitions, since the formation and introduction rules are not instances of ordinary indexed inductive definitions. (However, we do believe that inductioninduction can be reduced to indexed induction with a bit of more work, and plan to publish an article about this in the future.) To make sure that our theory is consistent, it is thus neccessary to construct a model.

We will develop a model in ZFC set theory, extended by two inaccessible cardinals in order to interpret Set and Type. Our model will be a simpler version of the models developed in [9, 11]. See Aczel [1] for a more detailed treatment of interpreting type theory in set theory.

5.1 Preliminaries

We will be working informally in ZFC extended with the existence of two strongly inaccessible cardinals 𝔦_{0} 𝔦_{1}, and will be using standard set theoretic constructions, e.g.

a, b a, b ,
λx a.b x  x, b x x a
Π_{x a}b x f a _{x a}b x  x a.f x b x ,
Σ_{x a}b x  c, d c a d b c ,
0 , 1 0 , 2 0, 1 , …,
a_{0} … a_{n} Σ_{i 0,...,n} a_{i}

and the cumulative hierarchy V_{α} _{β α} V_{β} . Whenever we introduce sets A^{α}

indexed by ordinals α, let

A^{α} _{β α} A^{β}.

For every expression A of our type theory, we will give an interpretation ⟦A⟧_{ρ}, regardless if A Type or A B or not. Interpretations might however be undefined, written ⟦A⟧_{ρ} . If ⟦A⟧_{ρ} is defined, we write ⟦A⟧_{ρ} . We write A B for partial equality, i.e. A B if and only if A B and if A , then A B. We write A B if we define A such that A B.

Open terms will be interpreted relative to an environment ρ, i.e. a function mapping variables to terms. Write ρ_{x a} for the environment ρ extended with x a, i.e. ρ_{x a} y a if y x and ρ y otherwise. The interpretation ⟦t⟧_{ρ} of closed terms t will not depend on the environment, and we omit the subscript ρ.

5.2 Interpretation of Expressions

The interpretation of the logical framework is as in [9]:

⟦Set⟧ V_{𝔦_{0}} ⟦Type⟧ V_{𝔦_{1}}

⟦ x A B⟧_{ρ} Π_{y ⟦A⟧_{ρ}}⟦B⟧_{ρ_{y x}} ⟦λx A.e⟧_{ρ} λy ⟦A⟧_{ρ}.⟦e⟧_{ρ_{y x}}

⟦ x A B⟧_{ρ} Σ_{y ⟦A⟧_{ρ}}⟦B⟧_{ρ_{y x}} ⟦ a, b ⟧_{ρ} ⟦a⟧_{ρ}, ⟦b⟧_{ρ}
⟦0⟧ 0  ⟦1⟧ 1  ⟦2⟧ 2  ⟦ ⟧ 0  ⟦tt⟧ 0  ⟦ff⟧ 1

⟦if x then a else b⟧_{ρ}  ;  ;  ;  ;  ;  ;  ;  ;  ;  ; ⟦a⟧_{ρ}  if ⟦x⟧_{ρ} 0 ⟦b⟧_{ρ}  if ⟦x⟧_{ρ} 1 undefined otherwise

⟦!_{A}⟧_{ρ} unique inclusion ι_{⟦A⟧} ⟦A⟧_{ρ}

To interpret terms containing SP_{A}, SP_{B}, Arg_{A}, Arg_{B}, Index_{B}, IH_{A}, IH_{B}, mapIH_{A}, mapIH_{B}, nil_{A}, nonind, A-ind, B-ind, nil_{B} and B_{n}-ind, we first define ⟦SP_{A}⟧, ⟦SP_{B}⟧, ⟦Arg_{A}⟧, … and interpret

⟦SP_{A} A_{ref}, B_{ref} ⟧_{ρ} ⟦SP_{A}⟧ ⟦A_{ref}⟧_{ρ}, ⟦B_{ref}⟧_{ρ}
⟦Arg_{A} …, γ, A, … ⟧_{ρ} ⟦Arg_{A}⟧ …, ⟦γ⟧_{ρ}, ⟦A⟧_{ρ}, …
⟦nonind K, γ ⟧_{ρ} ⟦nonind⟧ ⟦K⟧_{ρ}, ⟦γ⟧_{ρ}
etc.

In all future definitions, if we are currently defining ⟦F ⟧ where F D E, say, let F d if d ⟦D⟧.

⟦SP_{A}⟧ D, D^{}is defined as the least set such that

⟦SP_{A}⟧ D, D^{}1 _{K ⟦Set⟧} K ⟦SP_{A}⟧ D, D^{}_{K ⟦Set⟧}⟦SP_{A}⟧ D K, D^{}

_{K ⟦Set⟧} _{h K D} ⟦SP_{A}⟧ D, D^{}K .

By the inaccessibility of 𝔦_{1}, there is a regular cardinal κ 𝔦_{1} such that for all K ⟦Set⟧, we have that the cardinality of K, A_{ref}, B_{ref}, A_{ref} K, K A_{ref} , B_{ref} K is less than κ. If we now iterate an appropriate operator κ times, we get our solution, which must be an element of ⟦Type⟧ V_{𝔦_{1}} by the inaccessibility of 𝔦_{1}.

⟦nil_{A}⟧ 0, 0 ⟦B-ind K, h, γ ⟧ 3, K, h, γ
⟦nonind K, γ ⟧ 1, K, γ ⟦A-ind K, γ ⟧ 2, K, γ

⟦SP_{B}⟧ and ⟦nil_{B}⟧, ⟦B_{n}-ind⟧ are defined analogously. ⟦Arg_{A}⟧, ⟦Arg_{B}⟧, ⟦Index_{B}⟧, ⟦IH_{A}⟧, ⟦IH_{B}⟧, ⟦mapIH_{A}⟧ and ⟦mapIH_{B}⟧ are defined according to their equations, e.g.

⟦Arg_{A}⟧ A_{ref}, B_{ref}, ⟦nil_{A}⟧, rep_{A}, rep_{index}, rep_{B}  1
⟦Arg_{A}⟧ A_{ref}, B_{ref}, ⟦nonind⟧ K, γ , rep_{A}, rep_{index}, rep_{B}
_{k K}⟦Arg_{A}⟧ A_{ref}, B_{ref}, γ k , rep_{A}, rep_{index}, rep_{B}
⟦Arg_{A}⟧ A_{ref}, B_{ref}, ⟦A-ind⟧ K, γ , rep_{A}, rep_{index}, rep_{B}
_{j K A}⟦Arg_{A}⟧ A_{ref} K, B_{ref}, γ, rep_{A} j, rep_{index}, rep_{B}
⟦Arg_{A}⟧ A_{ref}, B_{ref}, ⟦B-ind⟧ K, h, γ , rep_{A}, rep_{index}, rep_{B}

_{j Π_{k K}B rep_{A} h k} ⟦Arg_{A}⟧ A_{ref}, B_{ref} K, γ, rep_{A}, rep_{index} rep_{A} h , rep_{B} j .

Finally, we have to interpret A_{γ_{A},γ_{B}}, B_{γ_{A},γ_{B}}, intro_{A}, intro_{B}, R_{A} and R_{B} . Let

⟦A_{γ_{A},γ_{B}}⟧ A^{𝔦_{0}} , ⟦B_{γ_{A},γ_{B}}⟧ a B^{𝔦_{0}} a , ⟦intro_{A}⟧ a a , ⟦intro_{B}⟧ b b ,

⟦R_{A}⟧ R_{A}^{𝔦_{0}} ⟦R_{B}⟧ R_{B}^{𝔦_{0}}

where A^{α}, B^{α} and R_{A}^{α}, R_{B}^{α} are simultaneously defined by recursion on α as

A^{α} ⟦Arg_{A}^{}⟧ γ_{A}, A^{α}, B^{α} ,
B^{α} a b b ⟦Arg_{B}^{}⟧ γ_{A}, γ_{B}, A^{α}, { \atop B^{α}} ⟦Index_{B}^{}⟧ γ_{A}, γ_{B}, A^{α}, { \atop B^{α}}, b a .

and

R_{A}^{α} g, h, a g a, mapIH_{A}^{}γ_{A}, ⟦A⟧, ⟦B⟧, E, E^{},
R_{A}^{α} g, h , R_{B}^{α} g, h , a
R_{B}^{α} g, h, a, b h b, mapIH_{B}^{}γ_{A}, γ_{B}, ⟦A⟧, ⟦B⟧, …, ⟦B⟧,
E, E^{}, …, E^{}, R_{A}^{α} g, h , R_{B}^{α} g, h , b

Having interpreted all terms, we finally interpret contexts as sets of environments:

⟦ ⟧  ⟦Γ, x A⟧ ρ_{x a} ρ ⟦Γ ⟧ a ⟦A⟧_{ρ} .

5.3 Soundness of the Rules

Theorem 1 (Soundness).

(i) If Γ context, then ⟦Γ ⟧ . (ii) If Γ A E, then ⟦Γ ⟧ , and for all ρ ⟦Γ ⟧, ⟦A⟧_{ρ} ⟦E⟧_{ρ}, and also ⟦E⟧_{ρ}

⟦Type⟧ if E Type. (iii) If Γ A B E, then ⟦Γ ⟧ , and for all ρ ⟦Γ ⟧, ⟦A⟧_{ρ} ⟦B⟧_{ρ}, ⟦A⟧_{ρ} ⟦E⟧_{ρ}

and also ⟦E⟧_{ρ} ⟦Type⟧ if E Type. (iv) a 0.

The proof of the soundness theorem is rather straightforward. For the verification that ⟦A_{γ_{A},γ_{B}}⟧ ⟦Set⟧ and ⟦B_{γ_{A},γ_{B}}⟧ ⟦A_{γ_{A},γ_{B}}⟧ ⟦Set⟧, one first verifies ⟦Arg_{A}^{}⟧, ⟦Arg_{B}^{}⟧, ⟦Index_{B}^{}⟧ are monotone in the following sense:

One can then prove some useful facts about A^{α} and B^{α} by induction on α:

Lemma 2.

(i) For α 𝔦_{0}, A^{α} ⟦Set⟧ and B^{α} A^{α} ⟦Set⟧. (ii) For α β, A^{α} A^{β} and B^{α} a B^{β} a for all a A^{α}. (iii) There is κ 𝔦_{0} such that for all α κ, A^{α} A^{κ} and B^{α} a B^{κ} a for all

a A^{α}.

The cardinal κ from (iii) can be found by considering a regular cardinal of cardinality greater than that of all index sets which starts an inductive argument. By the inaccessibility of 𝔦_{0}, κ 𝔦_{0}. With these lemmas, we are done, since ⟦A_{γ_{A},γ_{B}}⟧ A^{𝔦_{0}} A^{κ} ⟦Set⟧ and similarly for ⟦B_{γ_{A},γ_{B}}⟧.

6 Conclusions and Future Work

We have introduced and formalised a new principle, namely induction-induction, for defining sets in Martin-Löf type theory. The principle allows us to simultaneously introduce A Set and B A Set, both defined inductively. This principle is used in recent formulations of the meta-theory of type theory in type theory [5, 4].

In the future, the relationship between the principle presented here and what is implemented in Agda will be investigated further. Agda implements arbitrary number of levels, i.e. we can have A Set, B A Set, C a A B a Set etc., and induction-induction can be used in conjunction with inductionrecursion (with the side effect of a self-referring universe). Apart from this, we speculate that our theory covers what can be defined in Agda. However, just as for ordinary induction, we do not expect dependent pattern matching to follow from our elimination rules without the addition of Streicher’s Axiom K [16].

On the theoretical side, work is underway to show that inductive-inductive definitions can be reduced to indexed inductive definitions. This would show that the proof theoretical strength does not increase compared to ordinary induction. Normalisation, decidability of type checking and a categorical semantics similar to initial algebra semantics for ordinary inductive types are other topics left for future work.

References

1. Aczel, P.: On relating type theories and set theories. LNCS 1657, 1–18 (1999)

2. Backhouse, R., Chisholm, P., Malcolm, G., Saaman, E.: Do-it-yourself type theory. Formal Aspects of Computing 1(1), 19–84 (1989)

3. Benke, M., Dybjer, P., Jansson, P.: Universes for generic programs and proofs in dependent type theory. Nordic Journal of Computing 10, 265–269 (2003)

4. Chapman, J.: Type theory should eat itself. Electronic Notes in Theoretical Computer Science 228, 21–36 (2009)

5. Danielsson, N.: A formalisation of a dependently typed language as an inductiverecursive family. LNCS 4502, 93–109 (2007)

6. Dybjer, P.: Inductive families. Formal aspects of computing 6(4), 440–465 (1994)

7. Dybjer, P.: Internal type theory. LNCS 1158, 120–134 (1996)

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

9. Dybjer, P., Setzer, A.: A finite axiomatization of inductive-recursive definitions. In: Girard, J. (ed.) Typed lambda calculi and applications, LNCS, vol. 1581, pp. 129–146. Springer Verlag (1999)

10. Dybjer, P., Setzer, A.: Induction–recursion and initial algebras. Annals of Pure and Applied Logic 124(1-3), 1–47 (2003)

11. Dybjer, P., Setzer, A.: Indexed induction–recursion. Journal of logic and algebraic programming 66(1), 1–49 (2006)

12. Martin-Löf, P.: Intuitionistic type theory. Bibliopolis Naples (1984)

13. Morris, P.: Constructing Universes for Generic Programming. Ph.D. thesis, University of Nottingham (2007)

14. Nordvall Forsberg, F., Setzer, A.: Formalisation of induction-induction in Agda.

    http://cs.swan.ac.uk/~csfnf/induction-induction/indind.agda (2010)

15. Palmgren, E.: On universes in type theory. In: Sambin, G., Smith, J. (eds.) Twenty five years of constructive type theory. pp. 191 – 204. Oxford University Press (1998)

16. Streicher, T.: Investigations into intensional type theory. Habilitiation Thesis (1993)

17. The Agda Team: The Agda wiki. http://wiki.portal.chalmers.se/agda/ (2010)