Quotient Inductive Type

Idea

A quotient inductive type is an inductive type equipped not only with point constructors generating elements, but also with path constructors imposing specified equalities between those elements.

Signature

For a simple single-sorted presentation, a QIT signature consists of:

• a sort symbol $\dot{Q}$;
• for each point constructor $i\in [m]$, a strictly positive telescope ${\Phi }_i[\dot{Q}]$;
• for each path constructor $j\in [n]$, a strictly positive telescope ${\Psi }_j[\dot{Q}]$;
• for each path constructor $j\in [n]$, two endpoint terms $\psi :{\Psi }_j[\dot{Q}]⊢l_j(\psi ),r_j(\psi ):\dot{Q}.$

From this signature, one generates point constructors $c_i:{\Phi }_i[Q]\to Q$ and path constructors $p_j:(\psi :{\Psi }_j[Q])\to l_j(\psi ){=}_Q{r}_j(\psi ).$

Outside a UIP setting, a set-level QIT usually also includes a truncation constructor $\mathsf{trunc}:\mathsf{isSet}(Q),$ ensuring that all identity types of $Q$ are propositions.

Algebras

An algebra for a single-sorted equational QIT signature $\Sigma$ consists of:

• a carrier $A$;
• for each point constructor arity ${\Phi }_i[-]$, an operation $c_i^A:{\Phi }_i[A]\to A;$
• for each path constructor $j$, a proof ${\pi }_j^A:(\psi :{\Psi }_j[A])\to l_j^A(\psi ){=}_A{r}_j^A(\psi ).$

The point constructor operations induce interpretations of all formal terms appearing in the endpoint expressions $l_j,r_j$.

When the arities ${\Phi }_i$ are strictly positive, the point-constructor part often assembles into a signature functor $S_{\Sigma }(X)={\sum }_i{\Phi }_i[X],$ so that a QIT algebra may be viewed as an $S_{\Sigma }$-algebra equipped with proofs that the specified equations hold.

Introduction rules

Let $Q$ be the type being defined. A quotient inductive definition consists of

• point constructors

  $$\frac{\psi :{\Phi }_i[Q]}{c_i\psi :Q}(i\in [m])$$

• path constructors

  $$\frac{\psi :{\Psi }_j[Q]}{p_j\psi :l_j(\psi ){=}_Q{r}_j(\psi )}(j\in [n])$$

where each ${\Phi }_i$ and ${\Psi }_j$ is a strictly positive telescope, and

$$\psi :{\Psi }_j[Q]⊢l_j(\psi ),r_j(\psi ):Q.$$

Recursor

For any $\Sigma$-algebra $A$, there is a map ${\mathsf{rec}}_A:Q\to A$ preserving the point and path constructors. Here ${\Phi }_i[{\mathsf{rec}}_A]$ denotes the action of the telescope interpretation on the map ${\mathsf{rec}}_A$. The computation rules are: ${\mathsf{rec}}_A(c_i\psi )=c_i^A({\Phi }_i[{\mathsf{rec}}_A]\psi )$ for each point constructor $c_i$, and ${\mathsf{ap}}_{{\mathsf{rec}}_A}(p_j(\psi ))={\pi }_j^A({\Psi }_j[{\mathsf{rec}}_A](\psi ))$ for each path constructor $p_j$, where ${\pi }_j^A$ is the proof that the $j$th equation holds in the algebra $A$.

In a set-level presentation, this map is unique as a $\Sigma$-algebra morphism.

Constructability

In HoTT, set-level QITs can be seen as a subclass of HITs equipped with an $\mathsf{isSet}$ truncation constructor. Fiore et al. showed that ITT + UIP + funext + set quotients + WISC $⟹$ QWI types, a subclass of QITs. Kaposi et al. 2019 showed that a sufficiently powerful fragment of type theory supports finitary QIITs. This was later extended to large and infinitary QIITs by Kovács and Kaposi.

Open Questions

Is choice needed to construct QITs in general?

Blass 1983 showed that free algebras for infinitary equational theories cannot be constructed in ZF. Lumsdaine-Shulman 2018 concluded that because of this, no HITs that are modelled by ZF can construct these equational theories.

Related Concepts

• Fiore, Pitts and Steenkamp QW Type and QWI Type.
• Locality (QIT)
• Higher Inductive Type

Sources

• Altenkirch et al. 2016 “Quotient Inductive-Inductive Types”
• Kaposi et al. 2019 “Constructing Quotient Inductive-Inductive Types”
• Fiore et al. 2022 “Quotients, Inductive Types, and Quotient Inductive Types”
• Kovacs & Kaposi 2020 “Large and Infinitary Quotient Inductive-Inductive Types”
• Altenkirch & Kaposi 2016 “Type Theory in Type Theory using Quotient Inductive Types”
• Altenkirch 2024 “Quotient Inductive Types as Categorified Containers”
• Kaposi & Kovacs 2017 “Codes for Quotient Inductive Inductive Types?”
• Fiore et al. 2020 “Constructing Infinitary Quotient-Inductive Types”
• Dijkstra 2017 PhD Thesis “Quotient Inductive-Inductive Definitions”
• Altenkirch & Kaposi 2021 “A Container Model of Type Theory”
• Kaposi et al. 2019 “For Finitary Induction-Induction, Induction Is Enough”
• Kaposi 2016 PhD Thesis “Type Theory in a Type Theory with Quotient Inductive Types”