indInd_model.tex

\documentclass{schwicht}

\usepackage{proof}
\usepackage{mathtools}
\usepackage{amsthm}
\usepackage{amssymb}
\usepackage{amsmath}

\usepackage{graphicx}
\usepackage{varwidth}

\usepackage{MnSymbol}
\usepackage{stmaryrd}

\usepackage{enumerate}
\usepackage{microtype}

\usepackage{color}

\usepackage{hyperref}

%\overfullrule=10pt

\title{A finite axiomatisation of inductive-inductive definitions}
\author{Fredrik Nordvall Forsberg and Anton Setzer \thanks{Both authors
    are supported by EPSRC grant EP/G033374/1, Theory and applications
    of induction-recursion.}}

\input macros.tex

\begin{document}

\altmaketitle

\begin{abstract}
  \noindent 
  Induction-induction is a principle for mutually defining data types
  $A : \Set$ and $B : A \to \Set$. Both $A$ and $B$ are defined
  inductively, and the constructors for $A$ can refer to $B$ and vice
  versa. In addition, the constructor for $B$ can refer to \emph{the
    constructor} for $A$. Induction-induction occurs in a natural way
  when formalising dependent type theory in type theory.  We give some
  examples of inductive-inductive definitions, such as the set of
  surreal numbers. We then give a new finite axiomatisation of the
  principle of induction-induction, and prove its consistency by
  constructing a model.
\end{abstract}

\section{Introduction}
\label{sec:introduction}

When using Martin-L\"of type theory~\cite{martinlof1984bibliopolis}
for programming and theorem proving, one soon notices the need for
more complex data types which are syntactically closer to their intended
meaning. Examples include indexing data types with extra information
in order to express properties of their elements, or constructing a
universe in order to quantify over a large collection.

The programming language and proof assistant
Agda~\cite{norell2007thesis} supports many such data types, however
without a complete theoretical foundation. The proof assistant
Coq~\cite{coq}, on the other hand, does not at present support some of
the more advanced data types that Agda does. With the current article,
we wish to address both these issues for a form of data type which we
call \emph{inductive-inductive definitions}, for reasons that will
become clear below. Inductive-inductive definitions have been used by
several researchers in different areas -- see
Section~\ref{sec:examples} for some examples.

Let us now look at some examples of inductive definitions, such as the
natural numbers, lists, well-orderings, the identity set, finite sets,
and a universe \`a la Tarski. These examples can be categorised as
different kinds of inductive definitions.

The first few (up to well-orderings) are just ordinary inductive
definitions, where a single set is defined inductively. A typical
example is the type $W(A, B)$ of well-orderings, parameterised by $A :
\Set$, $B : A \to \Set$. The introduction rule is:
\[
\infer{\Wsup(a, f) : W(A, B)}{a : A & \quad f : B(a) \to W(A, B)}
\]
Here $a : A$ is a \emph{non-inductive} argument, whereas $f : B(a) \to
W(A, B)$ is an \emph{inductive} argument because of the occurrence of
$W(A, B)$. Note how the later argument depends on the earlier
non-inductive argument.

The identity type and the finite sets are examples
%not of ordinary inductive definitions, but 
of inductive families, where a family $X : I \to \Set$ for some fixed
index set $I$ is defined inductively
simultaneously~\cite{dybjer1994indfam}. For the family $\Fin : \Nat
\to \Set$ of finite sets, the index set is $\Nat$, and we have
introduction rules
\[
\infer{\finzero{n} : \Fin(n + 1)}{n : \Nat} \qquad
\infer{\finsucc{n}{m} : \Fin(n + 1)}{n : \Nat & \quad m : \Fin(n)}
\]
Thus the type $\Fin(n+1)$ has $n + 1$ elements $\finzero{n}$,
$\finsucc{n}{\finzero{n-1}}$,
$\finsucc{n}{\finsucc{n-1}{\finzero{n-2}}}$ up to
$\finsucc{n}{\finsucc{n-1}{\cdots\finsucc{1}{\finzero{0}}}}$.
%Each constructor constructs elements in $\Fin(k)$ for some $k : \Nat$,
%and 
The type of the inductive argument $m : \Fin(n)$ of the second rule
has index $n$, which is different from the index $n + 1$ of the type
of the constructed element. Thus the whole family has to be defined
simultaneously.

The universe \`a la Tarski is an example of an inductive-recursive
definition, where a set $U$ is defined inductively together with a
recursive function $T : U \to \Set$~\cite{dybjer2000IR}.  The
constructors for $U$ may depend negatively on $T$ applied to elements
of $U$, as is the case if $U$, for example, is closed under dependent
function spaces:
\[
\infer{\pi(a, b) : U}{a : U & \quad b : T(a) \to U}
\]
with $T(\pi(a, b)) = (x : T(a)) \to T(b(x))$.\footnote{The notation
  for the dependent function space and other type-theoretical
  constructs is explained in Section~\ref{sec:preliminaries}.}

Here, $T : U \to \Set$ is defined recursively. Sometimes, however, one
might not want to give $T(u)$ completely as soon as $u : U$ is
introduced, but instead define $T$ inductively as well. This is the
principle of \emph{induction-induction}. A set $A$ is inductively
defined simultaneously with an $A$-indexed set $B$, which is also
inductively defined, and the introduction rules for $A$ may also refer
to $B$. Typical introduction rules might take the form
\[ \infer{\intro{A}(a, b, \ldots) : A}{a : A &b : B(a) & \ldots} \quad
\infer{\intro{B}(a_0, b, a_1, \ldots) : B(a_1)}{a_0 : A &
&b : B(a_0) & a_1 : A & \ldots} \]

Notice that 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 (see Section \ref{sec:indind-vs-IR} for the difference).

Coq does at present not support inductive-inductive
definitions, whereas Agda does, without a theoretical foundation.
Working towards a justification of Agda's inductive-inductive
definitions, and an inclusion of such definitions in Coq, we give a
new finite axiomatisation of a type theory with inductive-inductive
definitions. It differs from our earlier
axiomatisation~\cite{nordvallforsbergSetzer2010indind} in that it is
finite, and is hopefully easier to understand.  The current article is
also somewhat different in scope from our CALCO
paper~\cite{nordvallforsbergAltenkirchMorrisSetzer2011catsemindind},
which focuses on a categorical semantics and shows that the
elimination rules (not treated here) are equivalent to the initiality
of certain algebras.
%This is a nice theoretical result, but not a basis for an
%implementation as the current article could be.

%The price we have to
%pay for this simplicity is that the natural full function space
%set-theoretical model construction becomes slightly more involved.

%Schemas and universes of descriptions.

%External schemas for general inductive sets and inductive families
%have been given by  respectively.

%this has been internalised by 

%Inductive-recursive
%definitions have also been used for generic programming in dependent
%type theory \cite{benke2003universes}.

\paragraph{Related work}
\label{sec:related-work}

Backhouse et.\ al.~\cite{backhouse1989diytt,backhouse1988meaning} and
Dybjer \cite{dybjer1994indfam,dybjer2000IR} gave external schemas for
ordinary inductive sets, inductive families and inductive definitions,
which later Dybjer and
Setzer~\cite{dybjersetzer1999finax,dybjersetzer2003inalg,dybjersetzer2006IIR}
internalised. This is where we take most of our inspiration from.
Recently, Ghani and Hancock~\cite{ghaniHancock2012algIR} have shed new
light on this construction.

The idea of a universe of data types is also present in Epigram
2~\cite{mcbride2010levitation}, and has previously been used by
Altenkirch, Ghani, Morris and McBride to study strictly positive
types~\cite{morrisAltenkirchMcBride2006regularTreeTypes} and strictly
positive families~\cite{morrisAltenkirchGhani2009SPFjournal} (see also
Morris' thesis~\cite{morris2007thesis}). Here data types are given a
more semantic account via the theory of
containers~\cite{abbottAltenkirchGhani2005containers} and indexed
containers~\cite{altenkirchMorris2009indexedCont}.

% Benke, Dybjer and Jansson~\cite{benke2003universes} use Dybjer and
% Setzer style universes of data types for generic programming.



\subsection{Examples of inductive-inductive definitions}
\label{sec:examples}

In this section, we give some examples of inductive-inductive
definitions, starting with the perhaps most important one:

\begin{example}[Contexts and types]
\label{ex:ctxt-type}

Danielsson \cite{danielsson2007formalisation} and Chapman
\cite{chapman2009eatitself} model the syntax of dependent type theory
in the theory itself by inductively defining contexts, types (in a
given context) and terms (of a given type). To see the
inductive-inductive nature of the construction, it is enough to
concentrate on contexts and types.

Informally, we have an empty context $\emptyCtxt$, and if we have any
context $\Gamma$ and a valid type $\sigma$ in that context, then we
can extend the context with a fresh variable $x : \sigma$ to get a new
context $\Gamma, x : \sigma$. This is the only way contexts are
formed. We end up with the following inductive definition of the set
of contexts (with $\consCtxt{\Gamma}{\sigma}$ meaning $\Gamma, x :
\sigma$ since we are using de Bruijn indices):
\[
\infer{\emptyCtxt : \Ctxt}{} \qquad
\infer{\consCtxt{\Gamma}{\sigma} : \Ctxt}{\Gamma : \Ctxt & \sigma : \Ty(\Gamma)}
\]

Moving on to types, we have a base type $\baseTy{}$ (valid in any
context) and dependent function types: if $\sigma$ is a type in
context $\Gamma$, and $\tau$ is a type in $\Gamma, x : \sigma$ ($x$ is
the variable from the domain), then $\Pi(\sigma, \tau)$ is a type in
the original context. This leads us to the following inductive
definition of $\Ty : \Ctxt \to \Set$:
\[
\infer{\baseTy{\Gamma} : \Ty(\Gamma)}{\Gamma : \Ctxt} \qquad
\infer{\piTy{\Gamma}{\sigma}{\tau} : \Ty(\Gamma)}{\Gamma : \Ctxt
                    & \sigma : \Ty(\Gamma)
                    & \tau : \Ty(\consCtxt{\Gamma}{\sigma})}
\]

Note that the definition of $\Ctxt$ refers to $\Ty$, so both sets have
to be defined simultaneously. Note also how the introduction rule for
$\Pi$ explicitly focuses on a specific constructor in the index of the
type of $\tau$. 
\blackqed
\end{example}

Often, one wishes to define a set $A$ where all elements of $A$
satisfy some property $P : A \to \Set$. If $P$ is inductively defined,
one can define $A$ and $P$ simultaneously and achieve that every
element of $A$ satisfies $P$ by construction. One example of such a
data type is the type of sorted lists:

\begin{example}[Sorted lists]
\label{ex:sorted-list}

Let us define a data type consisting of sorted lists (of natural
numbers, say). With induction-induction, we can simultaneously define
the set $\SortedList$ of sorted lists and the predicate $\lessList :
(\Nat \times \SortedList) \to \Set$ with $n \lessList \ell$ true if
$n$ is less than or equal to every element of $\ell$.

The empty list is certainly sorted, and if we have a proof $p$ that
$n$ is less than or equal to every element of the list $\ell$, we can
put $n$ in front of $\ell$ to get a new sorted list
$\consList{n}{\ell}{p}$. Translated into introduction rules, this becomes:
\[
\infer{\nilList : \SortedList}{} \qquad
\infer{\consList{n}{\ell}{p} : \SortedList}{n : \Nat \quad & \ell : \SortedList \quad & p : n \lessList \ell}
\]
For $\lessList$, we have that every $m : \Nat$ is trivially smaller
than every element of the empty list, and if $m \leq n$ and
inductively $m \lessList \ell$, then $m \lessList \consList{n}{\ell}{p}$:
\[
\infer{\nilLess{m} : m \lessList \nilList}
%{m : \Nat}
{} \qquad
\infer{\consLess{n}{\ell}{p}{m}{q}{p_{m, \ell}}\ : m \lessList \consList{n}{\ell}{p}}
%      {m, n : \Nat \quad & \ell : \SortedList \quad & p : n \lessList \ell \quad &
       {q : m \leq n \quad & p_{m, \ell} : m \lessList \ell}
\]
This makes sense even if the order $\leq$ is not transitive. If it is
(as the standard order on the natural numbers is, for example), the
argument $p_{m, \ell} : m \lessList \ell$ can be dropped from the
constructor $\consLessbare$, since we already have $q : m \leq n$ and
$p : n \lessList \ell$, hence by transitivity we must have $m
\lessList \ell$.

Of course, there are also many alternative ways to define such a data
type using ordinary induction (or using e.g.\ induction-recursion,
similarly to C. Coquand's definition of fresh lists as reported by
Dybjer~\cite{dybjer2000IR}).
%, but the inductive-inductive one seems
% natural and might be more convenient for some purposes.
\blackqed
\end{example}

\begin{example}[Conway's surreal numbers]
\label{ex:surreal}

Conway \cite{conway2001ONAG} informally uses induction-induction (but
couched in ZF set theory, not type theory) in order to define his
\emph{surreal numbers}. The class \footnote{The surreal numbers form a
  class, not a set, since they contain the class of ordinals. This can
  be avoided by referring to a universe.} of surreal numbers is
defined inductively, together with an order relation on surreal
numbers which is also defined inductively:

\begin{itemize}
\item A surreal number $X = (X_\mathrm{L}, X_\mathrm{R})$ consists of
  two sets $X_\mathrm{L}$ and $X_\mathrm{R}$ of surreal numbers, such
  that no element from $X_\mathrm{L}$ is greater than any element from
  $X_\mathrm{R}$.
\item A surreal number $Y = (Y_\mathrm{L}, Y_\mathrm{R})$ is greater
  than another surreal number $X = (X_\mathrm{L}, X_\mathrm{R})$, $X \Surleq Y$, if and
  only if
  \begin{itemize}
  \item there is no $x \in X_\mathrm{L}$ such that $Y \Surleq x$, and
  \item there is no $y \in Y_\mathrm{R}$ such that $y \Surleq X$.
  \end{itemize}
\end{itemize}

Both rules can be understood as inductive definitions. Notice how the
second definition only makes sense in the presence of the first
definition, and how the first definition already refers to the second.

As an inductive definition, the negative occurrence of $\leq$ in the
definition of the class of surreal numbers is problematic. We can get
around this by simultaneously defining the class $\Sur : \Set$
together with two relations $ \Surleq {} : \Sur \to \Sur \to \Set$ and
${ \Surnleq {} : \Sur \to \Sur \to \Set}$ as follows:

\begin{itemize}
\item If $X_\mathrm{L}$ and $X_\mathrm{R}$ are sets of surreal
  numbers, and for all $x \in X_\mathrm{L}$, $y \in X_\mathrm{R}$ we
  have $x \Surnleq y$, then $(X_\mathrm{L}, X_\mathrm{R})$ is a surreal number.

\item Assume $X = (X_\mathrm{L}, X_\mathrm{R})$ and $Y = (Y_\mathrm{L}, Y_\mathrm{R})$ are surreal numbers.
 If 
 \begin{itemize}
 \item for all $x \in X_\mathrm{L}$ we have $Y \Surnleq x$, and
 \item for all $y \in Y_\mathrm{R}$ we have $y \Surnleq X$,
 \end{itemize}
then $X \Surleq Y$.

\item Assume $X = (X_\mathrm{L}, X_\mathrm{R})$ and $Y = (Y_\mathrm{L}, Y_\mathrm{R})$ are surreal numbers.
 \begin{itemize}
 \item If there exist $x \in X_\mathrm{L}$ such that $Y \Surleq x$, then $X \Surnleq Y$.
 \item If there exist $y \in Y_\mathrm{R}$ such that $y \Surleq X$, then $X \Surnleq Y$.
 \end{itemize}
\end{itemize}
We see that $\Sur : \Set$ together with ${ \Surleq, \Surnleq : \Sur
  \to \Sur \to \Set}$ are defined inductive-inductively.


Mamane~\cite{mamane2004surrealCoq} develops the theory of surreal
numbers in the proof assistant Coq, using an encoding to reduce the
inductive-inductive definition to an ordinary inductive one.
\blackqed
\end{example}

Note that these examples strictly speaking refer to extensions of
inductive-inductive definitions as presented in this article. Example
\ref{ex:ctxt-type} in full would be an example of a defining of a
telescope $A : \Set$, $B : A \to \Set$, $C : (x : A) \to B(x) \to
\Set$, \ldots inductive-inductively. In Example \ref{ex:sorted-list},
$A : \Set$ and $B : A \to I \to \Set$ for some previously defined set
$I$ is defined, and Example \ref{ex:surreal} gives an
inductive-inductive definition of $A : \Set$, $B, B' : A \to A \to
\Set$. In the future, we plan to publish an axiomatisation which
captures all these examples in full. For pedagogical reasons, we think
it is preferable to first only treat the simpler case $A : \Set$, $B :
A \to \Set$ as in the current article.

\subsection{Inductive-inductive definitions versus inductive-recursive definitions}
\label{sec:indind-vs-IR}

%todo: rewrite

In both an inductive-inductive and an inductive-recursive definition,
a set $U$ and a family $T : U \to \Set$ are defined
simultaneously. The difference between the two principles is how $T$
is defined: inductively or recursively. We discuss in the following
first the difference between an inductive and a recursive definition.
To exemplify this difference, consider the following two definitions
of a data type $\Vecbare : \Nat \to \Set$ of non-empty lists of a
certain length (with elements from a set $A$):

\begin{description}
\item[Inductive definition] The singleton list $\singleVec{a}$ has length 1, and if $a$ is
  an element, and the list $\ell$ has length $n$, then
  $\consVec{a}{\ell}$ is a list of length $n + 1$. As an inductive
  definition, this becomes
\[
\infer{\singleVec{a} : \Vecind(1)}{a : A} \qquad \infer{\consVec{a}{\ell} :
  \Vecind(n + 1)}{a : A & \quad \ell : \Vecind(n)}
\]
Notice that there is no constructor which constructs elements in the
set $\Vecind(0)$.

\item[Recursive definition] If the recursive definition of the data
  type, we define the set $\Vecrec(n)$ for every natural number:
  \begin{align*}
    \Vecrec(0) &= \zero \\
    \Vecrec(1) &= A \\
    \Vecrec(n + 2) &= A \times \Vecrec(n + 1)
  \end{align*}

\end{description}

In the recursive definition, $\Vecrec(k)$ is defined in one go,
whereas the inductively defined $\Vecind(k)$ is built up from
below. In order to prove that $\Vecind(0)$ is empty, one has to carry
out a proof by induction over $\Vecind$.

This difference is now carried over to an
inductive-recursive/inductive-inductive definition of $U : \Set$, $T :
U \to \Set$.
In an inductive-inductive definition, $T$ is generated
inductively, i.e.\ given by a constructor $\intro{T} : (x : F(U, T))
\to T(i(x))$ for some (strictly positive) functor
$F$. %todo: mention i : F(U, T) \to U?
In an inductive-recursive definition, on the other hand, $T$ is
defined by recursion on the way the elements of $U$ are
generated. This means that $T(\intro{U}(x))$ must be given completely
as soon as the constructor $\intro{U} : G(U, T) \to U$ is introduced.

% To exemplify the difference, we consider two definitions of a data
% type of sorted lists. An inductive-inductive definitions has already
% been given in Example \ref{ex:sorted-list}.

There are some practical differences between the two approaches. An
inductive-inductive definition gives more freedom to describe the data
type, in the sense that many different constructors for $T$ can
contribute to the set $T(\intro{U}(x))$.  However, because of the
inductive generation of $T$, $T$ can only occur positively in the type
of the constructors for $U$ (and $T$), whereas $T$ can occur also
negatively in an inductive-recursive definition.

\section{Type-theoretical preliminaries}
\label{sec:preliminaries}

We work in a type theory with at least two universes $\Set$ and
$\TYPE$, with $\Set : \TYPE$ and $\Set$ a subuniverse of $\TYPE$,
i.e.\ if $A : \Set$ then $A : \TYPE$. Both $\Set$ and $\TYPE$ are
closed under dependent function types, written $(x : A) \to B$, where
$B$ is a set or type depending on $x: A$. Abstraction is written as
$\lambda x : A . e$, where $e : B$ depending on $x : A$, and
application as $f(x)$. Repeated abstraction and application are
written as $\lambda x_1 : A_1 \ldots x_k : A_k . e$ and $f(x_1,
\ldots, x_k)$. If the type of $x$ can be inferred, we simply write
$\lambda x.e$ as an abbreviation.  Furthermore, both $\Set$ and
$\TYPE$ are closed under dependent products, written $(x : A) \times
B$, where $B$ is a set or type depending on $x: A$, with pairs
$\langle a , b \rangle$, where $a : A$ and $b : B[x \coloneqq a]$.
% and projections $\pi_1$, $\pi_2$
We also have $\beta$- and $\eta$-rules for both dependent function types
and products.

We add an empty type $\zero : \Set$, with elimination ${\magic{A} : \zero
  \to A}$ for every $A : \Set$ (we will write $\magicOmit{}$ for $\magic{A}$ if $A$ can
be inferred from the context). We also add a unit type $\one : \Set$,
with unique element $\oneelt : \one$ and an $\eta$-rule stating that
if $x : \one$, then $x = \oneelt : \one$. Moreover, we include a two
element set $\two : \Set$, with elements $\twott : \two$, $\twoff :
\two$ and elimination constant $\IF~\cdot~\THEN~\cdot~\ELSE~\cdot :$
$(a : \two) \to A(\twott) \to A(\twoff) \to A(a)$ where $i : \two
\Rightarrow A(i) : \TYPE$. It satisfies the obvious computation rules,
i.e.\ $\IF~\twott~\THEN~a~\ELSE~b = a$ and $\IF~\twoff~\THEN~a~\ELSE~b
= b$.

With $\IF~\cdot~\THEN~\cdot~\ELSE~\cdot$ and dependent products, we can now
% as in \cite[A.2]{dybjersetzer2006IIR}
define the disjoint union of two sets $A + B \coloneqq$ ${(x : \two)}
\times (\IF~x~\THEN~A~\ELSE~B)$ with constructors $\inl = \lambda {a :
  A} . \langle \twott , a \rangle$ and $\inr = \lambda {b : B}
. \langle \twoff , b \rangle$, and prove the usual formation,
introduction, elimination and equality rules. Importantly, we get
large elimination for sums, since we have large elimination for
$\two$. We can define the eliminator ${[f, g] : {(c : A + B)} \to C(c)}$, where
$x : A + B \Rightarrow C(x) : \TYPE$ and $f : (a : A) \to C(\inl(a))$,
$g : (b : B) \to C(\inr(b))$, satisfying the definitional equalities
\begin{align*}
[f, g](\inl(a)) &= f(a) \enspace , \\
[f, g](\inr(b)) &= g(b) \enspace .
\end{align*}
%We write $\bigplus_{k = 0}^n A_k$ for the iterated sum $A_0 + (A_1 +
%(\ldots + A_n)\cdots)$ and $[f_0, f_1, \ldots, f_n]$ for the iterated
%case distinction $[f_0, [f_1, [\ldots , f_n]]\cdots]$.

Intensional type theory in Martin-L\"of's logical framework extended with
dependent products and $\zero$, $\one$, $\two$
%and $\Nat$
 has all the features we
need. Thus, our development can be seen as an extension of
the logical framework.

\section{A finite axiomatisation}
\label{sec:axiomatisation}
 
%TODO: rewrite

In this section, we give a finite axiomatisation of a type theory with
inductive-inductive definitions. This axiomatisation differs slightly
from our previous
axiomatisation~\cite{nordvallforsbergSetzer2010indind}, and is
hopefully easier to understand. However, the definable sets should
be the same for both axiomatisations.

The main idea, following Dybjer and Setzer's axiomatisation of
inductive-recursive definitions~\cite{dybjersetzer1999finax}, is to
construct a universe consisting of codes for inductive-inductive
definitions, together with a decoding function, which maps a code
$\varphi$ to the domain of the constructor for the inductively defined
set represented by $\varphi$.  We will actually use two universes; one
to describe the constructors for the index set $A$, and one to
describe the constructors of the second component $B : A \to \Set$.
Just as the constructors for $B : A \to \Set$ can depend on the
constructors for the first set $A$, the universe $\SPBp : \SPAp \to
\TYPE$ of codes for the second component will depend on the universe
$\SPAp$ of codes for the first.

\subsection{Dissecting an inductive-inductive definition}
\label{sec:dissect-ind}

We want to formalise and internalise an inductive-inductive definition
given by constructors
\[
\introA : \Phi_{\mathrm{A}}(A, B) \to A
\]
and
\[
\introB : (x : \Phi_{\mathrm{B}}(A, B, \introA)) \to B(\theta(x))
\]
for some $\Phi_{\mathrm{A}}(A, B) : \Set$, $\Phi_{\mathrm{B}}(A, B,
\introA) : \Set$ and $\theta : \Phi_{\mathrm{B}}(A, B, \introA) \to
A$.
Here, $\theta(x)$ is the \emph{index} of $\introB(x)$, i.e.\ the element $a :
A$ such that $\introB(x) : B(a)$.

Not all expressions $\Phi_{\mathrm{A}}$ and $\Phi_{\mathrm{B}}$ give
rise to acceptable inductive-inductive definitions. It is well known,
for example, that the theory easily becomes inconsistent if $A$ or $B$ occur
in negative positions in $\Phi_{\mathrm{A}}$ or $\Phi_{\mathrm{B}}$
respectively. Thus, we restrict our attention to a class of strictly
positive functors.

These are based on the following analysis of what kind of premises can
occur in a definition. A premise is either \emph{inductive} or
\emph{non-inductive}. A non-inductive premise consists of a previously
constructed set $K$, on which later premises can depend. An inductive
premise is inductive in $A$ or $B$. If it is inductive in $A$, it is
of the form $K \to A$ for some previously constructed set $K$%
%(this is also called a \emph{generalized} inductive premise, with
%the special case $K = \one$ being called an \emph{ordinary} inductive
%premise)
. Premises inductive in $B$ are of the form $(x : K) \to
B(i(x))$ for some $i : K \to A$. 

If $K = \one$, we have the special case of a single inductive
premise. In the case of $B$-inductive arguments, the choice of $i :
\one \to A$ is then just a choice of a single element $a = i(\oneelt)
: A$ so that the premise is of the form $B(a)$.

%If $K = \one$ we get in case of $A$-inductive arguments
%single inductive arguments
%and in case of $B$-inductive arguments, if we choose 
%$i : \one \to A$, $i = \lambda \oneelt\,.\,a$
%inductive-arguments referring to $B(a)$

%In the case of an ordinary inductive
%premise, $K = \one$ so that $i : \one \to A$ just amounts to a choice
%of an index $a = i(\oneelt)$ such that the inductive argument comes
%from $B(a)$.

%todo: improve

\subsection{The axiomatisation}
\label{sec:formal-axiomatisation}

We now give the formal rules for an inductive-inductive definition of
$A : \Set$, $B : A \to \Set$. These consists of a set of rules for the
universe $\SPAp$ of descriptions of the set $A$ and its decoding
function $\ArgAp$, a set of rules for the universe $\SPBp$ and its
decoding function $\ArgBp$, and formation and introduction rules for
$A: \Set$, $B: A \to \Set$ defined inductive-inductively by a pair of
codes $\gammaA : \SPAp$, $\gammaB : \SPBp(\gammaA)$.

\subsubsection{The universe $\SPAp$ of descriptions of $A$}
\label{sec:SPA}
  
We introduce the universe of codes for the index set with the
formation rule
\[
\infer{\SPA(\Aref) : \TYPE}{\Aref : \Set}
\]
The set $\Aref$ should be thought of as the elements of $A$ that we
can refer to in the code that we are defining. To start with, we
cannot refer to any elements in $A$, and so we define $\SPAp \coloneqq
\SPA(\zero)$. After introducing an inductive argument $a : A$, we can
refer to $a$ in later arguments, so that $\Aref$ will be extended to
include $a$ as well for the construction of the rest of the code.

The introduction rules for $\SPA$ reflects the informal discussion in
Section~\ref{sec:dissect-ind}. The rules are as follows (we suppress
the global premise $\Aref : \Set$):
\[
\infer{\nilA : \SPA(\Aref)}{}
\]
%
The code $\nilA$ represents a trivial constructor $c : \one \to A$ (a base case).
%
\[
\infer{\nonindA(K, \gamma) : \SPA(\Aref)}{K : \Set & \quad \gamma : K \to \SPA(\Aref)}
\]
%
The code $\nonindA(K, \gamma)$ represents a non-inductive argument $x
: K$, with the rest of the arguments given by $\gamma(x)$.
%
\[
\infer{\AindA(K, \gamma) : \SPA(\Aref)}{K : \Set & \quad \gamma : \SPA(\Aref + K)}
\]
%
The code $\AindA(K, \gamma)$ represents an inductive argument with
type $K \to A$, with the rest of the arguments given by
$\gamma$. Notice that $\gamma : \SPA(\Aref + K)$, so that the
remaining arguments can refer to more elements in $A$ (namely those
introduced by the inductive argument).
%
\[
\infer{\BindA(K, \hindex, \gamma) : \SPA(\Aref)}{K : \Set & \quad \hindex : K \to \Aref & \quad \gamma : \SPA(\Aref)}
\]
%
Finally, the code $\BindA(K, \hindex, \gamma)$ represents an inductive
argument with type $(x : K) \to B(i(x))$, where the index $i(x)$ is
determined by $\hindex$, and the rest of the arguments are given by
$\gamma$.
%

\begin{example}
  The constructor $\consCtxtbare : ((\Gamma : \Ctxt) \times \Ty(\Gamma))
  \to \Ctxt$ is represented by the code
\[
\gamma_{\consCtxtbare} = \AindA(\one, \BindA(\one, \lambda (\oneelt : \one)\,.\,\widehat{\Gamma}, \nilA)) \enspace ,
\]
where $\widehat{\Gamma} = \inr(\oneelt)$ is the representation of $\Gamma$ in $\Aref = \zero + \one$.
\blackqed
\end{example}

We now define the decoding function $\ArgA$, which maps a code to the
domain of the constructor it represents. In addition to a set $\Xref$
and a code $\gamma : \SPA(\Xref)$, $\ArgA$ will take a set $\A$ and a
family $\B : \A \to \Set$ as arguments to use as $A$ and $B$ in the
inductive arguments. These will later be instantiated by the sets
defined inductive-inductively. We also require a function $\repA :
\Xref \to \A$ which we think of as mapping a ``referable'' element to
the element it represents in $\A$. Thus, $\ArgA$ has the
following formation rule:
%
\[
\infer{\ArgA(\Xref, \gamma, \A, \B, \repA) : \Set}{\Xref : \Set
                                         & \quad \gamma : \SPA(\Xref)
                                         & \quad \A : \Set
                                         & \quad \B : \A \to \Set
                                         & \quad \repA : \Xref \to \A}
\]
%
Notice that if $\gamma : \SPAp$, i.e.\ if $\Xref = \zero$, then we can
choose $\repA = {} \magic{\A} : \zero \to \A$ (indeed, extensionally,
this is the only choice), so that we can define
\[
\ArgAp : \SPAp \to (\A : \Set) \to (\B : \A \to \Set) \to \Set
\]
by $\ArgAp(\gamma, \A, \B) = \ArgA(\zero, \gamma, \A, \B, \magic{X})$.

The definition of $\ArgA$ follows the informal description of what the
different codes represent above\footnote{For readability, we have
  replaced arguments which are simply passed on with ``$\omitt$'' in
  the recursive call, and likewise on the left hand side if the
  argument is not used otherwise.}:
%
%\resizebox{\textwidth}{!}{%
%\begin{minipage}{\textwidth}
\begin{align*}%
%  \ArgA(\Xref, \nilA, \A, \B, \repA) &= \one \\
  \ArgA(\omitt, \nilA, \omitt, \omitt, \omitt) &= \one \\
%  \ArgA(\Xref, \nonindA(K, \gamma), \A, \B, \repA) &= (x : K) \times \ArgA(\Xref, \gamma(x), \A, \B, \repA) \\
  \ArgA(\omitt, \nonindA(K, \gamma), \omitt, \omitt, \omitt) &= (x : K) \times \ArgA(\omitt, \gamma(x), \omitt, \omitt, \omitt) \\
%  \ArgA(\Xref, \AindA(K, \gamma), \A, \B, \repA) &=  \\
%\multispan{2}{\hfill $(j : K \to \A) \times \ArgA(\Xref + K, \gamma, \A, \B, [\repA, j])$} \\
  \ArgA(\Xref, \AindA(K, \gamma), \A, \omitt, \repA) &=  \\
\multispan{2}{\hfill $(j : K \to \A) \times \ArgA(\Xref + K, \gamma, \omitt, \omitt, [\repA, j])$} \\
%  \ArgA(\Xref, \BindA(K, \hindex, \gamma), \A, \B, \repA) &= \\
%\multispan{2}{\hfill $((x : K) \to \B((\repA \circ \hindex)(x))) \times \ArgA(\Xref, \gamma, \A, \B, \repA)$}
  \ArgA(\omitt, \BindA(K, \hindex, \gamma), \omitt, \B, \repA) &= \\
\multispan{2}{\hfill $((x : K) \to \B((\repA \circ \hindex)(x))) \times \ArgA(\omitt, \gamma, \omitt, \omitt, \omitt)$}
\end{align*}
%\end{minipage}
%}


\begin{example}
  Recall the code $\gamma_{\consCtxtbare} = \AindA(\one, \BindA(\one,
  \lambda (\oneelt : \one)\,.\,\inr(\oneelt), \nilA))$ for the
  constructor $\consCtxtbare : ((\Gamma : \Ctxt) \times \Ty(\Gamma)) \to
  \Ctxt$. We have 
\[
\ArgAp(\gamma_{\consCtxtbare}, \Ctxt, \Ty) = (\Gamma : \one \to \Ctxt)
\times (\one \to \Ty(\Gamma(\oneelt))) \times \one
\]
which, thanks to the $\eta$-rules for $\one$, $\times$ and $\to$, is isomorphic to the
domain of $\consCtxtbare$. 
\blackqed
\end{example}

\subsubsection{Towards descriptions of $B$} %todo: rename
\label{sec:towards-SPB}

As we have seen in Example \ref{ex:ctxt-type}, it is important that
the constructor $\introB$ for the second set $B : A \to \Set$ can
refer to the constructor $\introA$ for the first set $A$. This means
that inductive arguments might be of type $B(\introA(\overline{a}))$
for some $\overline{a} : \ArgAp(\gammaA, A, B)$ or even
$B(\introA(\ldots\introA\ldots(\overline{a})))$ for some $\overline{a}
: \ArgAp(\gammaA, \ldots \ArgAp(\gammaA, A, B)\ldots, B')$. Thus, we
need to be able to represent such indices in the descriptions of the
constructor $\introB$.

First, it is no longer enough to only keep track of the referable
elements $\Xref$ of $\A$ -- we need to be able to refer to elements of
$B$ as well, since they could be used as arguments to $\introA$. We
will represent the elements of $\B$ we can refer to by a set $\Yref$,
together with functions $\repIndex : \Yref \to \A$ and $\repB : (x :
\Yref) \to \B(\repIndex(x))$ ; the function $\repIndex$ gives the index
of the represented element, and $\repB$ the actual element.

We want to represent elements in $\ArgAp(\gammaA, \A, \B)$. We claim that
the elements in $\ArgAp(\gammaA, \Xref + \Yref, [\lambda x\,.\,\zero,
\lambda x\,.\,\one])$ are suitable for this purpose. To see this,
first observe that we can define functions
\[
f : \Xref + \Yref \to \A \enspace ,
\]
%
%and
%
\[
g : (x : \Xref + \Yref) \to
    [\lambda x\,.\,\zero, \lambda x\,.\,\one](x)
      \to \B(f(x))
\]
%
by $f = [\repA, \repIndex]$ and $g = [\lambda x\,.\,\magicOmit{\B \circ
  \repA}, \lambda x \oneelt\,.\, \repB(x)]$. Then, we can lift these
functions to a function
%
\[
\ArgAp(\gammaA, f, g) : \ArgAp(\gammaA, \Xref +\Yref, [\lambda x\,.\,\zero, \lambda x\,.\,\one]) \to
                       \ArgAp(\gammaA, \A, \B)
\]
%
by observing that $\ArgAp(\gammaA)$ is functorial:

\begin{lemma}
  For each $\gamma : \SPAp$, $\ArgAp(\gamma)$ extends to a functor from
  families of sets to sets, i.e.\ given $f : \A \to \A'$ and $g : (x :
  \A) \to \B(x) \to \B'(f(x))$, one can define $\ArgAp(\gamma, f, g) :
  \ArgAp(\gamma, \A, \B) \to \ArgAp(\gamma, \A', \B')$.
\end{lemma}
\begin{remark}
  In extensional type theory, one can also prove that $\ArgAp(\gamma,
  f, g) : \ArgAp(\gamma, \A, \B) \to \ArgAp(\gamma, \A', \B')$
  actually is a functor, i.e.\ that identities and compositions are
  preserved, but that will not be needed for the current development.
\end{remark}
\begin{proof}
  This is straightforward in extensional type theory. In intensional
  type theory without propositional identity types, we have to be more
  careful. The function $\ArgAp(\gamma, f, g)$ is defined by induction
  over $\gamma$. In order to do this, we need to refer inductively to
  the case when $\Xref$ is no longer $\zero$. Hence, we need to
  consider the more general case where $\A$, $\B$, $\A'$, $\B'$, $f$
  and $g$ have types as above, and $\Xref, : \Set$, $\repA : \Xref \to
  \A$, $\repA' : \Xref \to \A'$. One expects the equality $f(\repA(x))
  = \repA'(x)$ to hold for all $x : \Xref$. In order to avoid the use
  of identity types, we state this in a form of Leibniz equality,
  specialised to the instance we actually need;  we require a term
  \[
  p : (x : \Xref) \to \B'(f(\repA(x))) \to \B'(\repA'(x)) \enspace .
  \]
  %
  Thus we define
  % 
  \[
  \ArgA(\gamma, f, g, p) : %(p : (x : \Xref) \to \B'(f(\repA(x))) \to \B'(\repA'(x))) \to
  \ArgA(\Xref, \gamma, \A, \B, \repA)
  \to \ArgA(\Xref, \gamma, \A', \B', \repA')
  \]
  % 
  by induction over $\gamma$:
  \begin{align*}
    \ArgA(\nilA, f, g, p, \oneelt) &= \oneelt\\
    \ArgA(\nonindA(K, \gamma), f, g, p, \pair{k}{y}) &= \pair{k}{\ArgA(\gamma(k), f, g, p, y)}\\
    \ArgA(\AindA(K, \gamma), f, g, p, \pair{j}{y}) &= \pair{f \circ j}{\ArgA(\gamma, f, g, [p, \lambda x\,.\,\id], y)}\\
    \ArgA(\BindA(K, \hindex, \gamma), f, g, p, \pair{j}{y}) &= \\
    \pair{\lambda k\,.\,p(\hindex(k), g(\repA(&\hindex(k)), j(k)))}{\ArgA(\gamma, f, g, p, y)}
  \end{align*}
  
  Finally, we can define $\ArgAp(\gamma, f, g) : \ArgAp(\gamma, A, B) \to
  \ArgAp(\gamma, A', B')$ by
  \[
  \ArgAp(\gamma, f, g) \coloneqq \ArgA(\gamma,f, g, \magicOmit{B'(f(\repA(x))) \to B'(\repA'(x))}) \enspace . \qedhere
  \]
\end{proof}

Recall that we want to use the lemma to represent elements in
$\ArgAp(\gammaA, \A, \B)$ by elements in $\ArgAp(\gammaA, \Xref
+\Yref, [\lambda x\,.\,\zero, \lambda x\,.\,\one])$. We can actually
do better, and represent arbitrarily terms built from elements in $\A$
and $\B$ with the use of a constructor $\introA : \ArgAp(\gammaA, \A,
\B) \to \A$. For this, define the set $\Aterm(\gammaA, \Xref, \Yref)$
of terms ``built from $\introA$, $\Xref$ and $\Yref$'' with
introduction rules
%
\[
\infer{\termAref(x) : \Aterm(\gammaA, \Xref, \Yref)}{x : \Xref}
\]
%
%
\[
\infer{\termBref(x) : \Aterm(\gammaA, \Xref, \Yref)}{x : \Yref}
\]
%
%
\[
\infer{\termArg(x) : \Aterm(\gammaA, \Xref, \Yref)}{x : \ArgAp(\gammaA, \Aterm(\gammaA, \Xref, \Yref), \Bterm(\gammaA, \Xref, \Yref))}
\]
Here, $\Bterm(\gammaA, \Xref, \Yref) : \Aterm(\gammaA, \Xref, \Yref) \to \Set$ is defined by
\[
\begin{tabular}{lcr}
$\Bterm(\gammaA, \Xref, \Yref, \termAref(x))$ & $=$ & $\zero$ \\
$\Bterm(\gammaA, \Xref, \Yref, \termBref(x))$ & $=$ & $\one$  \\
$\Bterm(\gammaA, \Xref, \Yref, \termArg(x))$  & $=$ & $\zero$
\end{tabular}
\]
Note that this is formally an inductive-recursive definition.
The intuition behind the definition of $\Bterm$ is that all elements of
$\B$ we know are represented in $\Yref$, and only in $\Yref$. 

All elements in $\Aterm(\gammaA,\Xref, \Yref)$ represents elements in
$\A$, given that we have a function $\introA : \ArgAp(\gammaA, \A, \B) \to
\A$ and the elements of $\Xref$ and $\Yref$ represents elements of $\A$
and $\B$ respectively (i.e.\ we have $\repA : \Xref \to \A$, $\repIndex
: \Yref \to \A$ and $\repB : (x : \Yref) \to \B(\repIndex(x))$).
Formally, we can simultaneously define the following two functions:
%
\[ 
\resizebox{\textwidth}{!}{%
$
\infer{\deduce{\repBbar(\ldots) : (x : \Aterm(\gammaA, \Xref, \Yref)) \to \Bterm(\gammaA, \Xref, \Yref, x) \to \B(\repAbar(\ldots, x))}
              {\repAbar(\ldots) : \Aterm(\gammaA, \Xref, \Yref) \to \A}}
      {\gammaA : \SPAp & \quad
       \introA : \ArgAp(\gammaA, \A, \B) \to \A & \quad
              %{\deduce{\B : \A \to \Set}
              %        {\A : \Set}} & \quad
       \deduce{\repB : (x : \Yref) \to \B(\repIndex(x))}
              {\deduce{\repIndex : \Yref \to \A}
                      {\repA : \Xref \to \A}}}
$
}
\]
%
The definition of $\repAbar$ is straightforward. The interesting case
is $\termArg(x)$, where we make use of the constructor $\introA$, the
functoriality of $\ArgAp$ and the mutually defined $\repBbar$:
\begin{align*}
  \repAbar(\gammaA, \introA, \repA, \repIndex, \repB, \termAref(x)) &= \repA(x) \\
  \repAbar(\gammaA, \introA, \repA, \repIndex, \repB, \termBref(x)) &= \repIndex(x) \\
  \repAbar(\gammaA, \introA, \repA, \repIndex, \repB, \termArg(x)) &= \\
\multispan{2}{\hfill $\introA(\ArgAp(\gammaA, \repAbar(\ldots), \repBbar(\ldots), x))$}
\end{align*}
%
The simultaneously defined $\repBbar$ is very simple:
%
\begin{align*}
  \repBbar(\gammaA, \introA, \repA, \repIndex, \repB, \termAref(x), y) &=\ \magicOmit{\B \circ \repAbar(\ldots)}(y) \\
\repBbar(\gammaA, \introA, \repA, \repIndex, \repB, \termBref(x), \oneelt) &= \repB(y) \\
\repBbar(\gammaA, \introA, \repA, \repIndex, \repB, \termArg(x), y) &=\ \magicOmit{\B \circ \repAbar(\ldots)}(y) \\ \\
\end{align*}

\begin{example}
  We define some terms in $\Aterm(\gamma_{\consCtxtbare}, \Xref, \Yref)$, where
  \[
  \gamma_{\consCtxtbare} = \AindA(\one, \BindA(\one,
  \lambda (\oneelt : \one)\,.\,\inr(\oneelt), \nilA))
  \]
  is the code for the constructor
  \[
  \consCtxtbare : \big((\Gamma : \one \to A) \times (\one \to B(\Gamma(\oneelt))) \times \one\big) \to A \enspace .
  \]
  Suppose that we have $\hat{a} : \Xref$ with $\repA(\hat{a}) = a : A$
  and $\hat{b} : \Yref$ with $\repIndex(\hat{b}) = a$ and
  $\repB(\hat{b}) = b : B(a)$. We then have 
  \begin{itemize}
  \item $\termAref(\hat{a}) : \Aterm(\gamma_{\consCtxtbare}, \Xref, \Yref)$ with
  $\repAbar(\gamma_{\consCtxtbare}, \consCtxtbare, \ldots, \hat{a}) =
  a$ (so elements from $\Xref$ are terms).
\item $\termBref(\hat{b}) : \Aterm(\gamma_{\consCtxtbare}, \Xref,
  \Yref)$ with $\repAbar(\gamma_{\consCtxtbare}, \consCtxtbare,
  \ldots, \termBref(\hat{b})) = a$ (so elements from $\Yref$ are
  terms, representing the index of the element in $B$ they
  represent). Furthermore $\repBbar(\gamma_{\consCtxtbare}, \consCtxtbare, \ldots, \termBref(\hat{b}),
  \oneelt) = b$.
\item  $\widehat{a,b} \coloneqq \termArg(\langle (\lambda \oneelt.\,\termBref(\hat{b})) ,
  \langle (\lambda \oneelt.\,\oneelt), \oneelt\rangle\rangle) :
  \Aterm(\gamma_{\consCtxtbare}, \Xref, \Yref)$ with
  \[
      \repAbar(\gamma_{\consCtxtbare}, \consCtxtbare, \ldots, \widehat{a,b})
    = \consCtxt{(\repIndex(\hat{b}))}{(\repB(\hat{b}))} 
    = \consCtxt{a}{b} \enspace .
  \]
\blackqed
\end{itemize}
\end{example}

\subsubsection{The universe $\SPBp$ of descriptions of $B$}
\label{sec:SPB}

We now introduce the universe $\SPB$ of descriptions
for $B$. It has formation rule
%
\[
\infer{\SPB(\Aref, \Bref, \gammaA) : \TYPE}{\Aref, \Bref : \Set & \quad \gammaA : \SPAp}
\]
%
Again, we are interested in codes which initially do not refer to
any elements and define $\SPBp : \SPAp \to \TYPE$ by $\SPBp(\gammaA)
\coloneqq \SPB(\zero, \zero, \gammaA)$.

The introduction rules for $\SPB$ are similar to the ones for $\SPA$.
However, we now need to specify an index for the codomain of the
constructor, and indices for arguments inductive in $B$ can be
arbitrary terms built up from $\introA$ and elements we can refer to.

\[
\infer{\nilB(a) : \SPB(\Aref, \Bref, \gammaA)}{a : \Aterm(\gammaA, \Aref, \Bref)}
\]
%
The code $\nilB(\widehat{a})$ represents a trivial constructor $c :
\one \to B(a)$ (a base case), where the index $a$ is encoded by
$\widehat{a} : \Aterm(\gammaA, \Aref, \Bref)$.
%
\[
\infer{\nonindB(K, \gamma) : \SPB(\Aref, \Bref, \gammaA))}{K : \Set & \quad \gamma : K \to \SPB(\Aref, \Bref, \gammaA)}
\]
%
The code $\nonindB(K, \gamma)$ represents a non-inductive argument $x: K$, with the rest of the arguments given by $\gamma(x)$.
%
\[
\infer{\AindB(K, \gamma) : \SPB(\Aref, \Bref, \gammaA)}{K : \Set & \quad \gamma : \SPB(\Aref + K, \Bref, \gammaA)}
\]
%
The code $\AindB(K, \gamma)$ represents an inductive argument with
type $K \to A$, with the rest of the arguments given by
$\gamma$.
%
\[
\resizebox{\textwidth}{!}{
\infer{\BindB(K, \hindex, \gamma) : \SPB(\Aref, \Bref, \gammaA)}{K : \Set & \quad \hindex : K \to \Aterm(\Aref, \Bref, \gammaA) & \quad \gamma : \SPB(\Aref, \Bref + K, \gammaA)}
}
\]
%
At last, the code $\BindB(K, \hindex, \gamma)$ represents an inductive
argument with type $(x : K) \to B(i(x))$, where the index $i(x)$ is
determined by $\hindex$, and the rest of the arguments are given by
$\gamma$. Notice how the index is now encoded by arbitrary terms in
$\Aterm(\Aref, \Bref, \gammaA)$.
%
\begin{example}
  The constructor
  % 
  \[
  \Pi : \big((\Gamma : \Ctxt) \times (\sigma : \Ty(\Gamma)) \times \Ty(\consCtxt{\Gamma}{\sigma})\big)\to \Ty(\Gamma)
  \]
  % 
  is represented by the code
  % 
  \[
  \gamma_{\Pi} = \AindB(\one,
                  \BindB(\one, \lambda \oneelt\,.\,\widehat{\Gamma}, 
                    \BindB(\one, \lambda \oneelt\,.\,\widehat{\text{in}\pair{\Gamma}{\sigma}},
                      \nilB(\widehat{\Gamma}))))
  \]
  %
  where $\widehat{\Gamma} = \termAref(\inr(\oneelt))$ is the element
  representing the first argument $\Gamma : \Ctxt$ and
  $\widehat{\text{in}\pair{\Gamma}{\sigma}} = \termArg(\langle
  (\lambda \oneelt.\termBref(\inr(\oneelt))), \langle \lambda
  \oneelt.\oneelt, \oneelt\rangle\rangle)$ is the element representing
  $\consCtxt{\Gamma}{\sigma}$. 

\hfill \blackqed
\end{example}

The definition of $\ArgB$ should now not come as a surprise. First, we have a formation rule:
%
\[
\resizebox{\textwidth}{!}{%
$
%\mathclap{%
\infer{\ArgB(\Xref, \Yref, \gammaA, \A, \B, \introA, \repA, \repIndex, \repB, \gamma) : \Set}
             {\deduce{\gamma : \SPB(\Xref, \Yref, \gammaA)}
                     {\deduce{\Xref, \Yref : \Set}{\gammaA : \SPAp}}
      & \quad \deduce{\introA : \ArgA(\gammaA, \A, \B) \to \A}
                     {\deduce{\B : \A \to \Set}{\A : \Set}}
              & \quad \deduce{\repB: (x : \Yref) \to \B(\repIndex(x))}
                             {\deduce{\repIndex : \Yref \to \A}
                                     {\repA : \Xref \to \A}}}
%}
$
}
\]
%
The definition can be simplified for codes in $\SPBp(\gammaA)$:
\[
\ArgBp(\gammaA, \A, \B, \introA, \gamma) \coloneqq
   \ArgB(\zero, \zero, \gammaA, \A, \B, \introA, \magicOmit{\A}, \magicOmit{\A}, \magicOmit{\B \circ \magicOmit{\A}}, \gamma)
\]
%
We define\footnote{Once again, we have for readability
  replaced arguments which are simply passed on with ``$\omitt$'' in
  the recursive call, and likewise on the left hand side if the
  argument is not used otherwise.}:
%
\begin{align*} 
%&  \ArgB(\Xref, \Yref, \gammaA, \A, \B, \introA, \repA, \repIndex, \repB, \nilB(a)) = \one \\
&  \ArgB(\omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \nilB(a)) = \one \\
%&  \ArgB(\Xref, \Yref, \gammaA, \A, \B, \introA, \repA, \repIndex, \repB, \nonindB(K, \gamma)) \\  
%&\quad= (x : K) \times \ArgB(\Xref, \Yref, \gammaA, \A, \B, \introA, \repA, \repIndex, \repB, \gamma(x)) \\
&  \ArgB (\omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \nonindB(K, \gamma)) 
= (x : K) \times \ArgB(\omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \gamma(x)) \\
%&  \ArgB(\Xref, \Yref, \gammaA, \A, \B, \introA, \repA, \repIndex, \repB, \AindB(K, \gamma)) \\
%&\quad=  (j : K \to \A) \times \ArgB(\Xref + K, \Yref, \gammaA, \A, \B, \introA,  [\repA, j], \repIndex, \repB, \gamma) \\
&  \ArgB(\Xref, \omitt, \omitt, \A, \omitt, \omitt, \repA, \omitt, \omitt, \AindB(K, \gamma)) \\
&\quad=  (j : K \to \A) \times \ArgB(\Xref + K, \omitt, \omitt, \omitt, \omitt, \omitt,  [\repA, j], \omitt, \omitt, \gamma) \\
&  \ArgB(\omitt, \Yref, \gammaA, \omitt, \B, \introA, \repA, \repIndex, \repB, \BindB(K, \hindex, \gamma)) \\
&\quad= (j : (x : K) \to \B((\repAbar(\gammaA, \introA, \repA, \repIndex, \repB) \circ \hindex)(x))) \times {} \\ 
& \qquad\qquad\ \    \ArgB(\omitt, \Yref + K, \omitt, \omitt, \omitt, \omitt, \omitt, [\repIndex, \repAbar(\ldots) \circ \hindex], [\repB, j], \gamma)
%&  \ArgB(\Xref, \Yref, \gammaA, \A, \B, \introA, \repA, \repIndex, \repB, \BindB(K, \hindex, \gamma)) \\
%&\quad= (j : (x : K) \to \B((\repAbar(\gammaA, \introA, \repA, \repIndex, \repB) \circ \hindex)(x))) \times {} \\ 
%& \qquad     \ArgB(\Xref, \Yref + K, \gammaA, \A, \B, \introA, \repA, [\repIndex, \repAbar(\ldots) \circ \hindex], [\repB, j], \gamma)
\end{align*}


Finally, we need the function $\IndexBp(\ldots) : \ArgB(\gammaA, \gammaB, \A, \B,
\introA) \to \A$ which to each $b : \ArgB(\gammaA, \gammaB, \A, \B,
\introA)$ assigns an index $a : \A$ such that the element constructed
from $b$ is in $\B(a)$.
%
\[
\resizebox{\textwidth}{!}{%
$
\infer{\IndexB(\Xref, \Yref, \gammaA, \A, \B, \introA, \repA, \repIndex, \repB, \gamma) : \ArgB(\ldots) \to \A}
             {\deduce{\gamma : \SPB(\Xref, \Yref, \gammaA)}
                     {\deduce{\Xref, \Yref : \Set}{\gammaA : \SPAp}}
      & \quad \deduce{\introA : \ArgA(\gammaA, \A, \B) \to \A}
                     {\deduce{\B : \A \to \Set}{\A : \Set}}
              & \quad \deduce{\repB: (x : \Yref) \to \B(\repIndex(x))}
                             {\deduce{\repIndex : \Yref \to \A}
                                     {\repA : \Xref \to \A}}}
$
}
\]

For codes in $\SPBp(\gammaA)$, we define $\IndexBp : \ArgBp(\gammaA,
\A, \B, \introA, \gammaB) \to \A$ by $\IndexBp(\gammaA, \A, \B,
\introA, \gammaB) \coloneqq \IndexB(\zero, \zero, \gammaA, \A, \B,
\introA, \magicOmit{\A}, \magicOmit{\A}, \magicOmit{\B \circ
  \magicOmit{\A}}, \gammaB)$.

The equations by neccessity follows the same pattern as the equations
for $\ArgB$. For the base case $\gammaB = \nilB(a)$, we use
$\repA(\ldots, a)$, and for the other cases, we just do a recursive
call\footnote{Simply passed on and otherwise not used arguments have
  been replaced with ``$\omitt$'' for readability.}
%
\begin{align*} 
&  \IndexB(\omitt, \omitt, \gammaA, \omitt, \omitt, \introA, \repA, \repIndex, \repB, \nilB(a), \oneelt) \\
&\quad= \repAbar(\gammaA, \introA, \repA, \repIndex, \repB, a) \\
&  \IndexB(\omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \nonindB(K, \gamma), \pair{k}{y}) \\
&\quad= \IndexB(\omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \omitt, \gamma(k), y) \\
&  \IndexB(\Xref, \omitt, \omitt, \A, \omitt, \omitt, \repA, \omitt, \omitt, \AindB(K, \gamma), \pair{j}{y}) \\
&\quad=  \IndexB(\Xref + K, \omitt, \omitt, \omitt, \omitt, \omitt,  [\repA, j], \omitt, \omitt, \gamma, y) \\
&  \IndexB(\omitt, \Yref, \gammaA, \omitt, \B, \introA, \repA, \repIndex, \repB, \BindB(K, \hindex, \gamma), \pair{j}{y}) \\
& \quad=   \IndexB(\omitt, \Yref + K, \omitt, \omitt, \omitt, \omitt, \omitt, [\repIndex, \repAbar(\ldots) \circ \hindex], [\repB, j], \gamma, y)
\end{align*}

\begin{example} 
  The constructor $\Pi : \big((\Gamma : \Ctxt) \times (\sigma : \Ty(\Gamma))
  \times \Ty(\consCtxt{\Gamma}{\sigma})\big) \to \Ty(\Gamma)$ from Example
\ref{ex:ctxt-type} is represented by the code
%
\[
\gamma_{\Pi} = \AindB(\one, \BindB(\one, (\lambda \oneelt.\,\widehat{\Gamma}),\BindB(\one,
(\lambda \oneelt.\,\widehat{\consCtxt{\Gamma}{\sigma}}, \nilB(\widehat{\Gamma}))))) : \SPBp(\gamma_{\consCtxtbare}) \enspace ,
\]
  where $\widehat{\Gamma} = \termAref(\inr(\oneelt)) : \Aterm(\zero +
  \one, \zero, \gamma_{\consCtxtbare})$ and
  \[
  \widehat{\consCtxt{\Gamma}{\sigma}} = \termArg(\langle (\lambda
  \oneelt.\termBref(\inr(\oneelt))), \langle \lambda \oneelt.\oneelt,
  \oneelt\rangle\rangle) : \Aterm(\zero + \one, \zero + \one,
  \gamma_{\consCtxtbare}) \enspace .
  \]
%
We have 
\begin{multline*}
  \ArgBp(\gamma_{\consCtxtbare}, \Ctxt, \Ty, \consCtxtbare,
  \gamma_{\Pi}) = \\
 (\Gamma : \one \to \Ctxt) \times (\sigma : \one \to
  \Ty(\Gamma(\oneelt))) \times (\one \to
  \Ty(\consCtxt{\Gamma(\oneelt)}{\sigma(\oneelt)}) \times \one
\end{multline*}
and $\IndexBp(\gamma_{\consCtxtbare}, \Ctxt, \Ty, \consCtxtbare,
\gamma_{\Pi}, \langle \Gamma, \sigma, \tau, \oneelt\rangle) =
\Gamma(\oneelt)$.
\blackqed
\end{example}

\subsubsection{Formation and introduction rules}
\label{sec:intro}

We are now ready to give the formation and introduction rules for $A$
and $B$. They all have the common premises $\gammaA : \SPAp$, $\gammaB
: \SPBp(\gammaA)$, which will be omitted.

Formation rules:
%
\[
A_{\gammaAB} : \Set \qquad\quad
B_{\gammaAB} : A_{\gammaAB} \to \Set
\]
%
Introduction rule for $A_{\gammaAB}$:
%
\[ 
\infer{\intro{A_{\gammaAB}}(a) : A_{\gammaAB}}{a : \ArgAp(\gammaA, A_{\gammaAB}, B_{\gammaAB})}
\]
%
Introduction rule for $B_{\gammaAB}$:
%
\[
\infer{\intro{B_{\gammaAB}}(a) : B_{\gammaAB}(\IndexBp(\gammaA, A_{\gammaAB}, B_{\gammaAB}, \intro{A_{\gammaAB}}, \gammaB, a))}{a : \ArgBp(\gammaA, A_{\gammaAB}, B_{\gammaAB}, \intro{A_{\gammaAB}}, \gammaB)}
\]
%

\subsubsection{Elimination rules by example}
\label{sec:elim}

Elimination rules can also be
formulated~\cite{nordvallforsbergAltenkirchMorrisSetzer2011catsemindind}. Here,
we just give the elimination rules for the data type of sorted lists
(Example~\ref{ex:sorted-list}) as an example, and show how one can use
them to define a function which inserts a number into a sorted
list.\footnote{The inductive-inductive definition of the data type of
  sorted lists falls outside the axiomatisation presented in this
  article, as remarked at the end of Section~\ref{sec:examples}. We
  still include this example, as it shows the use of elimination rules
  in a real computer science example.}

\begin{example}
  The elimination rules for sorted lists and the $\lessList$ predicate
  state that functions $\elim_{\SortedList}$ and $\elim_{\lessList}$
  with the following types exist:
  \begin{align*}
    \elim_{\SortedList} :\ & (P : \SortedList \to \Set) \to \\
                       & (Q : (n : \Nat) \to (\ell : \SortedList) \to n \lessList \ell \to P(\ell) \to \Set) \to \\
                       & (\stepind{\nilList} : P(\nilList)) \to \\
                       & \big(\stepind{\consListbare} : (n : \Nat) \to (\ell : \SortedList) \to (p : n \lessList \ell) \to (\stepindarg{\ell} : P(\ell)) \\
                       & \qquad \to Q(n, \ell, p, \stepindarg{\ell}) \to P(\consList{n}{\ell}{p})\big) \to \\
                       & \big(\stepind{\nilLess{}} : (m : \Nat) \to Q(m, \nilList, \nilLess{n}, \stepind{\nilList})\big) \to \\
                       & \big(\stepind{\consLessbare} : (m : \Nat) \to (n : \Nat) \to (\ell : \SortedList) \to (p : n \lessList \ell) \\
                       & \qquad \to (q : m \leq n) \to (p' : m \lessList \ell) \to
                       (\stepindarg{\ell} : P(\ell)) \\ 
                       & \qquad \to (\stepindarg{p} : Q(n, \ell,p, \stepindarg{\ell}))
                       \to (\stepindarg{p'} : Q(m, \ell, p', \stepindarg{\ell})) \\
                       & \qquad \to Q(m,\consList{n}{\ell}{p}, \consLess{m}{n}{\ell}{p}{q}{p'}, \stepind{\consListbare}(n, \ell, p, \stepindarg{\ell}, \stepindarg{p}))\big) \to \\
                       & (\ell : \SortedList) \to P(\ell) \enspace , \\
  \end{align*}
  \begin{align*}
% 
     \elim_{\lessList} :\ & (P : \SortedList \to \Set) \to \\
                       & (Q : (n : \Nat) \to (\ell : \SortedList) \to n \lessList \ell \to P(\ell) \to \Set) \to \\
                       & (\stepind{\nilList} : \ldots) \to \\
                       & \big(\stepind{\consListbare} : \ldots\big) \to \\
                       & \big(\stepind{\nilLess{}} : \ldots\big) \to \\
                       & \big(\stepind{\consLessbare} : \ldots\big) \to \\
                       & (n : \Nat) \to (\ell : \SortedList) \to (p : n \lessList \ell) \\
                       & \qquad \to Q(n, \ell, p, \elim_{\SortedList}(\ldots, \ell)) \enspace .
  \end{align*}
with computation rules
%
\[
\elim_{\SortedList}(P, Q, \stepind{\nilList}, \stepind{\consListbare}, \stepind{\nilLess{}}, \stepind{\consLessbare}, \nilList) = \stepind{\nilList}
\]
and
\begin{multline*}
\elim_{\SortedList}(P, Q, \stepind{\nilList}, \stepind{\consListbare}, \stepind{\nilLess{}}, \stepind{\consLessbare}, \consList{n}{\ell}{p}) \\
= \stepind{\consListbare}(n, \ell, p, \elim_{\SortedList}(\ldots, \ell), 
\elim_{\lessList}(\ldots, n, \ell, p))  
\end{multline*}
%
for $\elim_{\SortedList}$, and
\[
\elim_{\lessList}(P, Q, \stepind{\nilList}, \stepind{\consListbare}, \stepind{\nilLess{}}, \stepind{\consLessbare}, m, \nilList, \nilLess{m}) = \stepind{\nilLess{}}(m)
\]
and
\begin{multline*}
\elim_{\lessList}(P, Q, \stepind{\nilList}, \stepind{\consListbare}, \stepind{\nilLess{}}, \stepind{\consLessbare}, m, \consList{n}{\ell}{p}, \consLess{m}{n}{\ell}{p}{q}{p'}) \\
= \stepind{\consLessbare}(m, n, \ell, p, q, p', \elim_{\SortedList}(\ldots, \ell), \\
\elim_{\lessList}(\ldots, n, \ell, p), \elim_{\lessList}(\ldots, m, \ell, p'))
\end{multline*}
for $\elim_{\lessList}$. Notice how the computation rules for
$\elim_{\lessList}$ are well-typed because of the computation rules
for $\elim_{\SortedList}$.

Now, suppose that we want to define a function $\Listinsert :
\SortedList \to \Nat \to \SortedList$ which inserts a number $m$ into
its appropriate place in a sorted list $\ell$ to create a new sorted
list. From a high-level perspective, this is easy: the elimination
rules allows us to make case distinctions between empty and non-empty
lists, so it suffices to handle these two cases separately. The empty
list is easy to handle, and for non-empty lists, we compare $m$ with
the first element $n$ of the list $\ell = [n, \ldots]$, which is
possible since $\leq$ on natural numbers is decidable. If $m \leq n$,
the result should be $[m, n, \ldots]$, otherwise we recursively insert
$m$ into the tail of the list.

In detail, we choose $P(\ell) = \Nat \to \SortedList$ and, in our
first attempt, we choose $Q(n, \ell, p, \stepindarg{\ell}) = \one$,
since we are only interested in getting a function
$\elim_{\SortedList}(\ldots) : \SortedList \to \Nat \to
\SortedList$. We need to give functions $\stepind{\nilList} : (m :
\Nat) \to \SortedList$ and $\stepind{\consListbare}(n, \ell, p) :
%(n : \Nat) \to (\ell : \SortedList) \to (p : n \lessList \ell) \to
(\stepindarg{\ell} : \Nat \to \SortedList) \to Q(n, \ell, p,
\stepindarg{\ell}) \to (m : \Nat) \to \SortedList$ to use when
inserting into the empty list or the list $\consList{n}{\ell}{p}$
respectively. The argument $\stepindarg{\ell} : \Nat \to \SortedList$
gives the result of a recursive call on $\ell$.

The function $\stepind{\nilList}$ is easy to define: it should be
\[
\stepind{\nilList}(m) = \consList{m}{\nilList}{\nilLess{m}}
\]
For $\stepind{\consListbare}$, the decidability of $\leq$ (combined
with the fact that $\leq$ is total) allows us to distinguish between
the cases when $m \leq n$ and $n \leq m$, and we are entitled to a
proof $q : m \leq n$ or $q : n \leq m$ of this fact. We try:
%
\begin{multline*}
\stepind{\consListbare}(n, \ell, p, \stepindarg{\ell}, \oneelt, m) \\ = 
\begin{cases}
  \consList{m}{\consList{n}{\ell}{p}}{\consLess{m}{n}{\ell}{p}{q}{\lessListtrans{q}{p}}} & \text{where $q : m \leq n$} \\
  \consList{n}{\stepindarg{\ell}(m)}{\SHED} & \text{where $q : n \leq m$} 
\end{cases}
\end{multline*}
%
Here, $\lessListtransbare : m \leq n \to n \lessList \ell \to m
\lessList \ell$ witnesses a kind of transitivity of $\leq$ and
$\lessList$. It can be straightforwardly defined with the elimination
rules. The question is what we should fill the hole $\SHED$ with. We
need to provide a proof that $n \lessList \stepindarg{l}(m)$, i.e.\
that $n \lessList \Listinsert(l, m)$ if we remember that
$\stepindarg{l}$ is the result of the recursive call on $\ell$. We
need to prove this simultaneously as we define $\Listinsert$!
Fortunately, this is exactly what the elimination rules allow us to do
if we choose a more meaningful $Q$.

Thus, we try again, but this time with 
\[
Q(n, \ell, p,\stepindarg{\ell})
   = (m : \Nat) \to n \leq m \to n \lessList \stepindarg{l}(m) \enspace .
\]
The argument $\oneelt : \one$ to $\stepind{\consListbare}$ in our
first attempt has now been replaced with the argument $\stepindarg{p}
: (m : \Nat) \to n \leq m \to n \lessList \stepindarg{l}(m)$, and we can define
\begin{multline*}
\stepind{\consListbare}(n, \ell, p, \stepindarg{\ell}, \stepindarg{p}, m) \\=
\begin{cases}
  \consList{m}{\consList{n}{\ell}{p}}{\consLess{m}{n}{\ell}{p}{q}{\lessListtrans{q}{p}}} & \text{where $q : m \leq n$} \\
  \consList{n}{\stepindarg{\ell}(m)}{\stepindarg{p}(m, q)} & \text{where $q : n \leq m$} 
\end{cases}
\end{multline*}
%
Now we must also define $\stepind{\nilLess{}} : (n : \Nat) \to Q(n,
\nilList, \nilLess{n}, \stepind{\nilList})$ and
$\stepind{\consLessbare}$ with type as above for our choice of $P$ and
$Q$. This presents us with no further difficulties. For
$\stepind{\nilLess{}}$, expanding $Q(n, \nilList, \nilLess{n},
\stepind{\nilList})$ and replacing $\stepind{\nilLess{}}$ with its
definition, we see that we should give a function of type
\[
\stepind{\nilLess{}} : (n : \Nat) \to (m : \Nat) \to n \leq m \to n
\lessList \consList{m}{\nilList}{\nilLess{m}} \enspace ,
\]
so we can define $\stepind{\nilLess{}}(n, m, p) = {}
\consLess{n}{m}{\nilList}{\nilLess{m}}{p}{\nilLess{n}}$. The
definition of $\stepind{\consLessbare}$ follows the pattern of $\stepind{\consListbare}$
above. Rather than trying to explain it, we just give the definition:
\[
\stepind{\consLessbare}(m, n, \ell, p, q, p', \stepindarg{\ell}, \stepindarg{p}, \stepindarg{p'}, x, r) =
\begin{cases}
  \consLess{m}{x}{\consList{n}{\ell}{p}}{\consLess{m}{n}{\ell}{p}{s}{\lessListtrans{s}{p}}}{r}{\consLess{m}{n}{\ell}{p}{q}{p'}} & \text{where $s : m \leq n$} \\
  \consLess{m}{n}{p'}{\stepindarg{p}(x, s)}{q}{\stepindarg{p'}(x, r)} & \text{where $s : n \leq m$} 
\end{cases}
\]
%
With all pieces in place, we can now define $\Listinsert : \SortedList
\to \Nat \to \SortedList$ as $\Listinsert = \elim_{\SortedList}(P, Q,
\stepind{\nilList}, \stepind{\consListbare}, \stepind{\nilLess{}},
\stepind{\consLessbare})$.
\blackqed
\end{example}

\subsection{The examples revisited}
\label{sec:examples-revisited}

We show how to find \gammaAB{} for some well-known sets, including the
examples in Section~\ref{sec:examples}.

\subsubsection{Encoding multiple constructors into one}
\label{sec:comb-constructors}

The theory we have presented assumes that both $A$ and $B$ have
exactly one constructor each. This is no limitation, as multiple
constructors can always be encoded into one by using non-inductive
arguments. Suppose that $\intro{0} : F_0(A, B) \to A$ and $\intro{1} :
F_1(A, B) \to A$ are two constructors for $A$. Then we can combine
them into one constructor
\[
\intro{0 + 1} : \big((i : \two) \times F_i(A, B)\big) \to A
\]
by defining $\intro{0 +1}(i, x) = \intro{i}(x)$.

If $\intro{0}$ is described by the code $\gamma_0$ and $\intro{1}$ by
$\gamma_1$, then $\intro{0 + 1}$ is described by the code
\[
\gamma_0 \plOP \gamma_1 \coloneqq
\nonindA(\two, \lambda x.\IF~x~\THEN~\gamma_0~\ELSE~\gamma_1) \enspace .
\]


\subsubsection{Examples of codes for inductive-inductive definitions}

\begin{description}
\item[Well-orderings] Ordinary inductive definitions can be
  interpreted as inductive-inductive definitions where we only care
  about the index set $A$ and not about the family $B : A \to \Set$. A
  canonical choice is to let $B$ have constructor $\introB : (x : A)
  \to B(x)$, which is described by the code $\gamma_{\text{dummy}}
  \coloneqq \AindB(\one,
  \nilB(\termAref(\inr(\oneelt))))$\footnote{Another choice is
    $\gamma_{\text{dummy}} = \nonindB(\zero, \magic{\SPBp(\gammaA)})$, which makes $B(x)$
    an empty type.}.

  For every $A : \Set$, $B : A \to \Set$, let
  \[
  \gamma_{W(A, B)} \coloneqq \nonindA(A, \lambda x\,.\,\AindA(B(x),\nilA))
  \]
  and define $W(A, B) \coloneqq A_{\gamma_{W(A, B)},
    \gamma_{\text{dummy}}}$.  Then $W(A, B)$ has constructor
  \[
  \intro{W(A, B)} : \big((x : A) \times (B(x) \to W(A, B)) \times \one\big) \to W(A, B) \enspace .
  \]

\item[Finite sets] Also indexed inductive definitions can be
  interpreted as inductive-inductive definitions, namely those where
  the index set just is an isomorphic copy of a previously constructed
  set (i.e.\ with constructor $\introA : I \to A$ for some $I : \Set$).

  For the family $\Fin : \Nat \to \Set$ of finite sets, the index set
  is $\Nat$, so we define
  \[
  \gamma_A \coloneqq \nonindA(\Nat, \lambda n\,.\,\nilA) : \SPAp
  \]
  and
  \[
  \gamma_{\Fin} \coloneqq \gamma_{\finzeroBare} \plOP \gamma_{\finsuccBare} : \SPBp(\gammaA)
  \]
  where
  \begin{align*}
    \gamma_{\finzeroBare} &\coloneqq \nonindB(\Nat, \lambda n\,.\,\nilB(\termArg(\pair{n + 1}{\oneelt}))) \enspace ,\\
    \gamma_{\finsuccBare} &\coloneqq \nonindB(\Nat, \lambda n\,.\,\BindB(\one, (\lambda \oneelt . \termArg(\pair{n}{\oneelt})), \nilB(\termArg(\pair{n + 1}{\oneelt})))) \enspace .
  \end{align*} 

  Then the constructor $\intro{A_{\gamma_A, \gamma_{\Fin}}} : \Nat \times \one \to
  A_{\gamma_A, \gamma_{\Fin}}$ is one part of an isomorphism $\Nat
  \cong \Nat \times \one \cong A_{\gamma_A, \gamma_{\Fin}}$, and if we
  define $\Fin : \Nat \to \Set$ by 
  \[
  \Fin(n) = B_{\gamma_A, \gamma_{\Fin}}(\intro{A_{\gamma_A,  \gamma_{\Fin}}}(\pair{n}{\oneelt})) \enspace ,
  \] 
  then we can define constructors
  \begin{align*}
    \infer{\finzero{n} : \Fin(n + 1)}{n : \Nat} \qquad
\infer{\finsucc{n}{m} : \Fin(n + 1)}{n : \Nat & \quad m : \Fin(n)}
  \end{align*}
  by $\finzero{n} = \intro{B_{\gamma_A,
      \gamma_{\Fin}}}(\pair{\twott}{\pair{n}{\oneelt}})$ and
  \[
  \finsucc{n}{m} = \intro{B_{\gamma_A,
      \gamma_{\Fin}}}(\pair{\twoff}{\pair{n}{\pair{(\lambda
        \oneelt\,.\,m)}{\oneelt}}} \enspace .
  \]
% γℕ' : SPA ⊥
% γℕ' = nonind ℕ (λ n → nilA)

% γFin : SPB ⊥ ⊥ γℕ'
% γFin =     nonind ℕ (λ n → nilB (inn (suc n , _)))
%        +++ nonind ℕ (λ n → B-ind ⊤ (λ _ → inn (n , _)) (nilB (inn ((suc n) , _))))

% ℕ' : Set
% ℕ' = A γℕ' γFin

% i : ℕ -> ℕ'
% i n = introA (n , _)

% Fin : ℕ -> Set
% Fin n = B γℕ' γFin (i n)

% fz : (n : ℕ) -> Fin (suc n)
% fz n = introB (tt , (n , _))

% fsuc : (n : ℕ) -> Fin n -> Fin (suc n)
% fsuc n m = introB (ff , n , ((λ _ → m) , _))


\item[Contexts and types]

The codes for the contexts and types from Example \ref{ex:ctxt-type} are as follows: \vskip
0.2cm
\begin{tabular}{lcl}
$\gamma_{\Ctxt}$ &$=$& $\nilA \plOP \AindA(\one, \BindA(\one, (\lambda \oneelt .\,\inr(\oneelt)),
\nilA)) : \SPAp$ \\
$\gamma_{\baseTybare}$ &$=$& $\AindB(\one, \nilB(\termAref(\inr(\oneelt))))$ \\
$\gamma_{\Pi}$ &$=$& $\AindB(\one, \BindB(\one, (\lambda \oneelt.\,\termAref(\inr(\oneelt))),\BindB(\one,$ \\
&& \qquad\quad $(\lambda \oneelt.\termArg(\langle \twoff, \langle (\lambda
\oneelt.\termBref(\inr(\oneelt))),$ 
 $\langle \lambda \oneelt.\oneelt, \oneelt\rangle\rangle\rangle),$ \\
&& \qquad\qquad $\nilB(\termAref(\inr(\oneelt))))))$ \\
$\gamma_{\Ty}$ &$=$& $\gamma_{\baseTybare} \plOP \gamma_{\Pi} : \SPBp(\gamma_{\Ctxt})\enspace .$
\end{tabular}
\vskip 0.2cm \noindent
We have $\Ctxt = A_{\gamma_{\Ctxt}, \gamma_{\Ty}}$ and $\Ty =
B_{\gamma_{\Ctxt}, \gamma_{\Ty}}$
and we can define the usual constructors by
\vskip 0.2cm
\begin{tabular}{l@{\qquad}l}
  $\emptyCtxt : \Ctxt$ & $\baseTybare : (\Gamma : \Ctxt) \to \Ty(\Gamma)$ \\
  $\emptyCtxt = \intro{A_{\gamma_{\Ctxt}, \gamma_{\Ty}}}(\langle \twott, \oneelt\rangle)\enspace ,$ & $\baseTy{\Gamma} = \intro{B_{\gamma_{\Ctxt}, \gamma_{\Ty}}}(\langle \twott, \langle (\lambda \oneelt.\Gamma), \oneelt\rangle\rangle)\enspace ,$\\
\end{tabular}
\vskip 0.2cm
\begin{tabular}{l}
  $\consCtxtbare : (\Gamma : \Ctxt) \to \Ty(\Gamma) \to \Ctxt$ \\
  $\consCtxt{\Gamma}{\sigma} = \intro{A_{\gamma_{\Ctxt}, \gamma_{\Ty}}}(\langle \twoff, \langle (\lambda \oneelt.\Gamma), \langle (\lambda \oneelt.\sigma), \oneelt\rangle \rangle\rangle)$ \enspace ,\\
\end{tabular}
\vskip 0.2cm
\begin{tabular}{l}
$\Pi : (\Gamma : \Ctxt) \to (\sigma : \Ty(\Gamma)) \to \Ty(\consCtxt{\Gamma}{\sigma}) \to
\Ty(\Gamma)$ \\
$\Pi(\Gamma, \sigma, \tau) = \intro{B_{\gamma_{\Ctxt}, \gamma_{\Ty}}}(\langle \twoff, \langle (\lambda
    \oneelt.\Gamma), \langle (\lambda \oneelt.\sigma),\langle (\lambda \oneelt. \tau) , \oneelt\rangle\rangle \rangle\rangle)$\enspace .
\end{tabular}
\end{description}

\section{A set-theoretic model}
\label{sec:model}

Even though $\SPA$ and $\SPB$ themselves 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
the theory of inductive-inductive definitions \emph{can} be reduced to
the theory of indexed inductive definitions with a bit of more
work, and plan to do this in the future.)
To make sure that our theory is consistent, it is thus necessary 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 by Dybjer and
Setzer~\cite{dybjersetzer1999finax,dybjersetzer2006IIR} for
induction-recursion.
See Aczel \cite{aczel1999typesandsets} for a more detailed treatment
of interpreting type theory in set theory.



\subsection{Preliminaries}

We will be working informally in ZFC extended with the existence of two
strongly inaccessible cardinals $\cardz < \cardi$,
and will be using standard set theoretic constructions, e.g.
{\allowdisplaybreaks %give latex a chance to break the page
\begin{align*}
\langle a, b\rangle &\coloneqq \{ \{ a \}, \{ a, b \}\} \enspace , \\
\lambda x \in a.b(x) &\coloneqq \{\langle x, b(x)\rangle\,|\,x \in a \} \enspace ,\\
\Pi_{x \in a}b(x) &\coloneqq \{ f : a \to \bigcup_{x \in a}b(x)\ |\ \forall x \in a.f(x) \in b(x)\} \enspace , \\
\Sigma_{x \in a}b(x) &\coloneqq \{ \langle c , d\rangle\ |\ c \in a \land d
\in b(c) \} \enspace , \\
0 &\coloneqq \emptyset, 1 \coloneqq \{0\}, 2 \coloneqq \{0, 1\} \enspace , \\
a_0 + \ldots + a_n &\coloneqq \Sigma_{i \in \{0, \ldots, n\}}a_i
\end{align*}
%
and the cumulative hierarchy $V_{\alpha} \coloneqq
\displaystyle\bigcup_{\beta < \alpha} \mathcal{P}(V_{\beta})$. Whenever we
introduce sets $A^{\alpha}$ indexed by ordinals $\alpha$, let \[A^{< \alpha}
\coloneqq \displaystyle\bigcup_{\beta < \alpha}A^{\beta}.\]
}

For every expression $A$ of our type theory, we will give an interpretation
$\sem{A}_\rho$, regardless of whether $A : \TYPE$ or $A : B$ or not. Interpretations
might however be undefined, written $\sem{A}_\rho\uparrow$. If $\sem{A}_\rho$
is defined, we write $\sem{A}_\rho\downarrow$. We write $A \simeq B$ for
partial equality, i.e.\ $A \simeq B$ if and only if $A\downarrow
\Leftrightarrow B\downarrow$ and if $A\downarrow$, then $A = B$. We write $A
\colonsimeq B$ if we define $A$ such that $A \simeq B$.

Open terms will be interpreted relative to an environment $\rho$, i.e.\ a
function mapping variables to terms. Write \rhoextend{x}{a} for the
environment $\rho$ extended with $x \mapsto a$, i.e.\ $\rhoextend{x}{a}(y) = a$
if $y = x$ and $\rho(y)$ otherwise. The interpretation $\sem{t}_{\rho}$ of closed
terms $t$ will not depend on the environment, and we omit the subscript $\rho$.

\subsection{Interpretation of Expressions}
\noindent 
The interpretation of the logical framework is as in
\cite{dybjersetzer1999finax}:
\begin{gather*}
\sem{\Set} \colonsimeq V_{\cardz} \qquad \sem{\TYPE} \colonsimeq V_{\cardi} \\
\sem{(x : A) \to B}_\rho \colonsimeq \Pi_{y \in
  \sem{A}_\rho}\sem{B}_{\rhoextend{y}{x}} \qquad
\sem{\lambda x:A.e}_\rho \colonsimeq \lambda y \in
\sem{A}_\rho.\sem{e}_{\rhoextend{y}{x}} \\
\sem{(x : A) \times B}_\rho \colonsimeq \Sigma_{y \in
  \sem{A}_\rho}\sem{B}_{\rhoextend{y}{x}} \qquad
\sem{\langle a, b \rangle}_\rho \colonsimeq \langle \sem{a}_\rho ,
\sem{b}_\rho\rangle \\
\sem{\zero} \colonsimeq 0 \qquad \sem{\one} \colonsimeq 1 \qquad
\sem{\two} \colonsimeq 2 \qquad \sem{\oneelt} \colonsimeq 0 \qquad \sem{\twott} \colonsimeq 0 \qquad
\sem{\twoff} \colonsimeq 1\\
\sem{\IF~x~\THEN~a~\ELSE~b}_\rho \colonsimeq
\begin{cases}
\sem{a}_\rho & \text{if $\sem{x}_\rho = 0$} \\
\sem{b}_\rho & \text{if $\sem{x}_\rho = 1$} \\
\text{undefined} & \text{otherwise} \\
\end{cases} \\
\sem{\magic{A}}_\rho \colonsimeq \emptyset \text{ (the unique inclusion $\emptyset \to \sem{A}_\rho$ )}
\end{gather*}

To interpret terms containing $\SPA$, $\SPB$, $\ArgA$, $\ArgB$,
$\IndexB$, and the codes $\nilA$, $\nonindA$, $\AindA$ and
$\BindA$, we first define $\sem{\SPA}$, $\sem{\SPB}$, $\sem{\ArgA}$,
$\sem{\nilA}$, $\sem{\nonindA}$, \ldots and interpret
{\allowdisplaybreaks
\begin{align*}
\sem{\SPA(\Xref)}_\rho &\coloneqq \sem{\SPA}(\sem{\Xref}_\rho) \\
\vdots \\
\sem{\ArgA(\Xref, \gamma, X, Y, \repA)}_\rho &\coloneqq
\sem{\ArgA}(\sem{\Xref}_\rho, \sem{\gamma}_\rho, \sem{X}_\rho, \sem{Y}_\rho, \sem{\repA}_\rho) \\
\vdots \\
\sem{\nonindA(K, \gamma)}_\rho &\coloneqq \sem{\nonindA}(\sem{K}_\rho,
\sem{\gamma}_\rho) \\
\vdots & \text{\quad etc.}
\end{align*}
In all future definitions, if we are currently defining $\sem{F}_{\rho}$ where $F : D
\to E$, say, let $\sem{F}_{\rho}(d)\uparrow$ if $d \notin \sem{D}_{\rho}$.
}

$\sem{\SPA}(\Xref)$ is defined as the least set such that
\begin{align*}
\sem{\SPA}(\Xref) &= 1 + \sum_{K \in \sem{\Set}}(K \to \sem{\SPA}(\Xref))
  + \sum_{K \in \sem{\Set}}\sem{\SPA}(\Xref + K) \\
 & {} + \sum_{K \in \sem{\Set}}\sum_{h : K \to \Xref}\sem{\SPA}(\Xref) \enspace .
\end{align*}
%
The constructors are then interpreted as
%
\begin{align*}
 \sem{\nilA} \colonsimeq \langle 0, 0\rangle \quad
 \sem{\BindA}(K, h, \gamma) \colonsimeq \langle 3 , \langle K, \langle h, \gamma \rangle\rangle\rangle
   \\
  \sem{\nonindA}(K, \gamma) \coloneqq \langle 1 , \langle K, \gamma
  \rangle\rangle \quad \sem{\AindA}(K, \gamma) \colonsimeq \langle 2 , \langle K, \gamma \rangle\rangle
\end{align*}
$\sem{\SPB}$ and its constructors are defined analogously. The
functions $\sem{\ArgA}$, $\sem{\ArgB}$ and $\sem{\IndexB}$ are defined
according to their equations, e.g.\
\begin{align*}
  \sem{\ArgA}(\Xref, \sem{\nilA}, X, Y, \repA) &\colonsimeq 1 \\
\sem{\ArgA}(\Xref, \sem{\nonindA}(K, \gamma), X, Y, \repA) &\colonsimeq
  \sum_{k \in K} \sem{\ArgA}(\Xref, \gamma(k), X, Y, \repA) \\
\sem{\ArgA}(\Xref, \sem{\AindA}(K, \gamma), X, Y, \repA) &\colonsimeq\!\!\!\!\!
  \sum_{j : K \to A}\!\!\!\sem{\ArgA}(\Xref + K, \gamma, X, Y, [\repA, j])\!\!\!\!\!\!\!\! \\
\sem{\ArgA}(\Xref, \sem{\BindA}(K, h, \gamma), X, Y, \repA) &\colonsimeq
  \sum_{\mathclap{j \in \Pi_{k \in K} B(\repA (h(k)))}}\sem{\ArgA}(\Xref, \gamma, X, Y, \repA).
\end{align*}

Finally, we have to interpret $A_{\gammaAB}$, $B_{\gammaAB}$,
$\intro{A_{\gammaAB}}$ and $\intro{B_{\gammaAB}}$.  The high-level
idea is to iterate $\ArgAp$ until a fixed point is reached, then apply
$\ArgBp$ once, and repeat. This is necessary since $\ArgBp$ expects an
argument $\introA : \ArgAp(\gammaA, A, B) \to A$, which can be chosen
to be the identity if $A$ is a fixed point of $\ArgAp(\gammaA, A, B)$
(with $B$ fixed). In more detail, let
\begin{gather*}
\sem{A_{\gammaAB}} \colonsimeq A^{\cardz} \enspace\! , \quad\!\!
\sem{B_{\gammaAB}}(a) \colonsimeq B^{\cardz}(a)\enspace\! , \quad\!\! \\
\sem{\intro{A_{\gammaAB}}}(a) \colonsimeq a \enspace\! ,\quad\!\!
\sem{\intro{B_{\gammaAB}}}(b) \colonsimeq b \enspace\! ,
\end{gather*}  \noindent 
where $A^{\alpha}$ and $B^{\alpha}$ are
simultaneously defined by recursion on $\alpha$ as
\begin{align*}
  A^{\alpha} & \coloneqq  \text{least fixed point containing $A^{< \alpha}$ of }
       \lambda X\,.\, \sem{\ArgAp}(\gamma_A, X, B^{< \alpha}) \enspace ,\\
  B^{\alpha}(a) & \coloneqq \{b\ |\ b \in \sem{\ArgBp}(\gamma_A, A^{\alpha},
  B^{< \alpha}, \id, \gamma_B) \\
  & \quad \land \sem{\IndexBp}(\gamma_A,
  A^{\alpha}, B^{< \alpha}, \id, \gamma_B, b) = a \}\enspace \hspace{-2.47968pt} .
\end{align*}

The (graph of the) eliminators can then be built up in the same
stages.

Having interpreted all terms, we finally interpret contexts as sets of environments:
\begin{align*}
  \sem{\emptyset} \colonsimeq \emptyset && \sem{\Gamma, x : A} \colonsimeq \{
  \rhoextend{x}{a} \ |\ \rho \in \sem{\Gamma} \land a \in \sem{A}_\rho\}.
\end{align*}

\subsection{Soundness of the Rules}

A detailed verification of the soundness of all the rules falls
outside the scope of this paper. The main difficulty lies in proving
that $\sem{\SPA}$ and $\sem{\SPB}$ are well-defined, and that
$\sem{A_{\gamma_A, \gamma_B}} \in \sem{\Set}$ and $\sem{B_{\gamma_A,
    \gamma_B}} : \sem{A_{\gamma_A, \gamma_B}} \to \sem{\Set}$. Full
details of the proof will be provided in a future publication (in
preparation).

$\sem{\SPA}$ is obtained by iterating the appropriate operator $\Gamma
: (\sem{\Set} \to \sem{\Set}) \to (\sem{\Set} \to \sem{\Set})$ up to
$\cardz$ times. Since $\Xref \in \sem{\Set}$, we have $(\Xref + K)$,
$(K \to \Xref)$ $\in \sem{\Set}$ for all $K \in \sem{\Set} =
V_{\cardz}$ by the inaccessibility of $\cardz$. Hence all
``premisses'' have cardinality at most $\cardz$, which is regular, so
that the operator has a fixed point after $\cardz$ iterations, which
must be an element of $\sem{\TYPE} = V_{\cardi}$ by the
inaccessibility of $\cardi$.

To see that $\sem{A_{\gamma_A, \gamma_B}} \in \sem{\Set}$ and
$\sem{B_{\gamma_A, \gamma_B}} : \sem{A_{\gamma_A, \gamma_B}} \to
\sem{\Set}$, one first verifies that $\sem{\ArgAp}$, $\sem{\ArgBp}$,
$\sem{\IndexBp}$ are monotone in the following sense:
  %
\begin{lemma}
  \label{thm:Arg-monotone}
  For all $\gammaA \in \sem{\SPAp}$ and $\gammaB \in \sem{\SPBp}(\gammaA)$:
  \begin{enumerate}[(i)]
  \item If $A \subseteq A'$ and $B(x) \subseteq B'(x)$ then
    $\sem{\ArgAp}(\gammaA, A, B) \subseteq \sem{\ArgAp}(\gammaA, A', B')$.
  \item If in addition $\introA(x) = \introA'(x)$ for all $x \in \ArgAp(\gammaA, A, B)$, then
    \[
    \sem{\ArgBp}(\gammaA, A, B, \introA, \gammaB) \subseteq \sem{\ArgBp}(\gammaA, A', B', \introA', \gammaB)
    \]
    and
    \[    
    \sem{\IndexBp}(\gammaA, A, B, \introA, \gammaB, x) = \sem{\IndexBp}(\gammaA, A', B', \introA', \gammaB, x)
    \]
    for all $x \in \sem{\ArgBp}(\gammaA, A, B, \introA, \gammaB)$. \qed
  \end{enumerate}
\end{lemma}

We can then adapt the standard results~\cite{aczel1977indDef} about
monotone operators. First, we note that one application of
$\sem{\ArgAp}$ and $\sem{\ArgBp}$ is not enough to take us outside of
$\sem{\Set}$:


\begin{lemma}
  For all $\gammaA \in \sem{\SPAp}$ and $\gammaB \in \sem{\SPBp}(\gammaA)$:
  \begin{enumerate}[(i)]
  \item If $X \in \sem{\Set}$ and $Y(x) \in \sem{\Set}$ for each $x \in X$, then $\sem{\ArgAp}(\gammaA, X, Y) \in \sem{\Set}$.
  \item If $X \in \sem{\Set}$ and $Y(x) \in \sem{\Set}$ for each $x \in X$, $\sem{\ArgBp}(\gammaA, X, Y, \intro{X}, \gammaB) \in \sem{\Set}$. \qed
  \end{enumerate}
  \end{lemma}


  We then iterate, using $A^{\alpha}$ and $B^{\alpha}$, in order to
  reach a fixed point. This uses that fact that both $\sem{\ArgAp}$
  and $\sem{\ArgBp}$ are $\kappa$-continuous for large enough
  $\kappa$:

\begin{lemma} \mbox{}
\label{thm:A-in-Set}
  \begin{enumerate}[(i)]
  \item For $\alpha < \cardz$, $A^{\alpha} \in \sem{\Set}$ and $B^{\alpha} :
    A^{\alpha} \to \sem{\Set}$. 
  \item For $\alpha < \beta$, $A^{\alpha} \subseteq A^{\beta}$ and  $B^{\alpha}(a) \subseteq
    B^{\beta}(a)$ for all $a \in A^{\alpha}$. 
  \item There is $\kappa < \cardz$ such that for  all $\alpha \geq \kappa$,
    $A^{\alpha} = A^{\kappa}$ and $B^{\alpha}(a) =  B^{\kappa}(a)$ for all $a
    \in A^{\alpha}$. \qed 
  \end{enumerate}
\end{lemma}

Now we are done, since %by Lemma~\ref{thm:A-in-Set}
$\sem{A_{\gamma_A, \gamma_B}} = A^{\cardz} = A^{\kappa} \in
\sem{\Set}$, and similarly for $\sem{B_{\gamma_A, \gamma_B}}$.

\bibliographystyle{alpha}
\bibliography{schwichtenberg}
%\bibliography{../../references/biblio}


\end{document}