Abstract
Quotient inductive-inductive types (QIITs) are generalisations of inductive types in type theory. QIITs may consist of multiple sorts which can be indexed over each other. They also support equality constructors. In this paper we present a type of codes for QIITs along with interpretation functions which specify constructors, eliminators and computation rules for the encoded types. This is analogous to containers which act as codes for W-types. We present an internal syntax of a type theory with a universe and restricted function types. A code for a QIIT is a context in this type theory. The internal syntax is formalised as a QIIT itself. We consider a metatheory with unique identity proofs, hence we interpret codes as quotient instead of general higher inductive types. Some of the contents of this paper were formalised in the proof assistant Agda. Showing that the given QIITs exist is left as future work.