At the core of Martin-Löf type theory (also known as “intuitionistic type theory”) are dependent types, that is, types whose definitions depend on values; these may be used to encode logical quantification. In general, a type may represent a logical formula; the values of the type are then the possible proofs of the formula. Type theory has been developed as an alternative foundation of mathematics, but has also found practical application in advanced type systems; in particular, the languages of many proof assistants are based on type theoretical concepts.

The present paper advances the state of the art in type theory by generalizing the notions of inductive types (which provide constants and functions to construct terms of the type) and inductive-inductive types (which allow the simultaneous definition of a type and a family of types indexed over that type) to quotient inductive-inductive types (QIITs): these types simultaneously introduce multiple types where the later types can be indexed over the previous ones; furthermore, equality constructors can be used to state equalities among type constructions. The core of this paper is the definition of a type theory called “theory of signatures,” which is used to specify finitary QITTs. This theory is given a semantics by proving the existence of an initial algebra for every signature. Finally, it is shown that these algebras support the principle of induction.

While the paper is very technical in nature, an ample introduction virtuously strives to illustrate to nonexperts the core ideas via various examples of QIITs defined in the theory of signatures (however, already here, some background in type theory may be helpful). The core part of the paper is then clearly targeted to researchers in the field; even with this, to keep the paper readable, the full definitions of the main operations have been delegated to an electronic appendix. The conclusions address further work on lifting several restrictions of the theory, in particular the generalization to infinitary QIITs and the generalization to higher-order inductive-inductive types (HIITs).