Abstract
In this thesis we present a theory of quotient inductive-inductive definitions,
which are inductive-inductive definitions extended with constructors for
equations. The resulting theory is an improvement over previous treatments of inductive-inductive and indexed inductive definitions in that it
unifies and generalises these into a single framework. The framework can
also be seen as a first approximation towards a theory of higher inductive
types, but done in a set truncated setting.
We give the type of specifications of quotient inductive-inductive definitions mutually with its interpretation as categories of algebras. A categorical characterisation of the induction principle is given and is shown to
coincide with the property of being an initial object in the categories of algebras. From the categorical characterisation of induction, we derive a more
type theoretic induction principle for our quotient inductive-inductive definitions that looks like the usual induction principles.
The existence of initial objects in the categories of algebras associated to
quotient inductive-inductive definitions is established for a class of definitions. This is done by a colimit construction that can be carried out in type
theory itself in the presence of natural numbers, sum types and quotients
or equivalently, coequalisers.