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.
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.
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.

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”