Quotient Inductive-Inductive Type

Idea

A quotient inductive-inductive type (QIIT) is a simultaneous inductive definition of multiple sorts, where later sorts may be indexed by earlier ones, and the definition may include path constructors imposing specified equalities between terms of any sort. QIITs combine inductive-inductive types and quotient inductive types.

The motivating examples are the well-typed syntax of Martin-Löf Type Theory — where contexts and types over contexts are defined simultaneously with equations governing substitution — and the Cauchy Real Numbers, where the Cauchy sequence type and its truncation are defined together.

Signature

A QIIT signature $\Sigma$ extends an IIT signature with path constructors. It consists of:

• sort symbols ${\dot{A}}_i$ for $i\in [s]$, with index types ${\Theta }_i[{\dot{A}}_{<i}],$ each depending only on previously defined sorts, so that the intended sort is $A_i:{\Theta }_i[A_{<i}]\to \mathcal{U};$
• for each point constructor $i\in [m]$: a target sort ${\mathrm{sort}}_i\in [s]$, a strictly positive telescope ${\Phi }_i[{\dot{A}}_{\ast }]$, and a target index ${\tau }_i:{\Phi }_i[A_{\ast }]\to {\Theta }_j[A_{<j}],j:={\mathrm{sort}}_i;$
• for each path constructor $j\in [n]$: a target sort $k:={\mathrm{psort}}_j\in [s]$, a telescope ${\Psi }_j[{\dot{A}}_{\ast }]$, a target index ${\upsilon }_j$, and two endpoint terms $\psi :{\Psi }_j[{\dot{A}}_{\ast }]⊢l_j(\psi ),r_j(\psi ):{\dot{A}}_k({\upsilon }_j(\psi )).$

This generates point constructors $c_i:(\phi :{\Phi }_i[A_{\ast }])\to A_j({\tau }_i(\phi )),j:={\mathrm{sort}}_i,$ and path constructors $p_j:(\psi :{\Psi }_j[A_{\ast }])\to l_j(\psi ){=}_{A_k({\upsilon }_j(\psi ))}{r}_j(\psi ),k:={\mathrm{psort}}_j.$

Outside a UIP setting, a set-level QIIT usually also includes truncation constructors ${\mathsf{trunc}}_i:(x:{\Theta }_i[A_{<i}])\to \mathsf{isSet}(A_i(x))$ for each sort $i$.

Algebras

An algebra for a QIIT signature $\Sigma$ consists of:

• for each sort $i\in [s]$, a type family $A_i:{\Theta }_i[A_{<i}]\to \mathcal{U};$
• for each point constructor $i\in [m]$, an operation $c_i^A:(\phi :{\Phi }_i[A_{\ast }])\to A_j({\tau }_i(\phi ));$
• for each path constructor $j\in [n]$, a proof ${\pi }_j^A:(\psi :{\Psi }_j[A_{\ast }])\to l_j^A(\psi ){=}_{A_k({\upsilon }_j^A(\psi ))}{r}_j^A(\psi ).$

A morphism of $\Sigma$-algebras from $(A_i,c_i^A,{\pi }_j^A)$ to $(B_i,c_i^B,{\pi }_j^B)$ consists of a family of maps $f_i:(x:{\Theta }_i[A_{<i}])\to A_i(x)\to B_i({\Theta }_i[f_{<i}](x))$ commuting with all point and path constructors.

The section induction principle — the elimination rule for QIITs — states that for any displayed algebra over the QIIT $(A_i)$, there exists a section. This is equivalent to initiality of the QIIT in the category of $\Sigma$-algebras. The equivalence between initiality and the section induction principle was established in Altenkirch et al. 2016.

Examples

Well-typed syntax of type theory

The canonical example is the intrinsic syntax of Martin-Löf Type Theory. The two sorts are $\mathrm{Con}:\mathcal{U},\mathrm{Ty}:\mathrm{Con}\to \mathcal{U}.$ Point constructors include the empty context, context extension, and type formers: $\diamond :\mathrm{Con},▹:(\Gamma :\mathrm{Con})\to \mathrm{Ty}(\Gamma )\to \mathrm{Con}.$ Substitution is added as a further family of operations, with path constructors enforcing equations such as $\mathrm{Ty}(\Gamma ▹A)[\sigma ]=\mathrm{Ty}(\Gamma [\sigma ]▹A[{\sigma }^{+}])$ that hold between terms of the second sort $\mathrm{Ty}$.

Cauchy reals

The Cauchy Real Numbers can be presented as a QIIT with two sorts: the type $\mathbb{R}$ of Cauchy reals and a proof-relevant apartness or equality relation. Path constructors express Cauchy completeness and the quotient condition identifying equivalent sequences.

Relationship to QITs and IITs

QIITs strictly generalise both QITs and IITs:

• Restricting to a single sort ($s=1$, no sort indexing) recovers a QIT.
• Removing all path constructors recovers an IIT.

The combination of the two features is non-trivial: the path constructors may now target any sort at any index, so equations can relate terms of different sorts or terms in fibres over identified base elements.

Constructability

The initial-algebra semantics for finitary QIITs was developed in Altenkirch et al. 2016 using dialgebras, extending earlier work on IITs. A general type-theoretic construction of finitary QIITs from a theory of signatures — a universe of codes for QIIT signatures together with an interpretation — was given in Kaposi et al. 2019.

Large and infinitary QIITs, where constructor arities may range over large types or infinite families, were treated in Kovács and Kaposi 2020.

Agda provides partial native support for inductive-inductive definitions. General QIITs are currently encoded via the theory of signatures rather than supported as a primitive.

Related Concepts

• Inductive-Inductive Type
• Quotient Inductive Type
• Higher Inductive Type
• Initial Algebra
• Dialgebra

References

altenkirch2016-qiit kaposi2019-constructing-qiit kovacs2020-infinitary-qiit dijkstra2017-thesis-qiit kaposi2017-qiit-codes altenkirch2021-container-model altenkirch2011-inductive-inductive-semantics