What are the possible kinds of type theories or logics with quotients?

Question

As described in this answer, one of the differences between Coq and Lean is the presence of definitional quotients in the latter. By contrast, the absence of definitional quotients in Coq forces one to use setoids, as explained in this answer.

I'm wondering if there are any pen-and-paper type systems or logics that have definitional quotients in them; and papers describing such systems.

The motivation for this question is to understand the design space for quotients.

---

What follows is a clarifying example.

---

As an example only, I will take multi-sorted relational first-order logic (henceforth RFOL) and add something resembling quotients as naively as possible, giving us RFOL'.

In RFOL, we have constant symbols $c_1, c_2, \cdots$ and relation symbols $R_1, R_2, \cdots$. Each relation symbol has a type signature $S_{a_1} \cdots S_{a_n} \to 2$ where $S_{a_1} \cdots S_{a_n}$ is a sequence of sorts.

Let $R$ be any binary relation with type signature $S \times S \to 2$.

I define $S/R$ as a new sort. In an interpretation $M$, the interpretation of $S/R$ is the interpretation of $S$ partitioned into equivalence classes by the transitive symmetric reflexive closure of $R$.

For every constant $c$ of type $S$, I add a fresh constant symbol $c'$ of type $S/R$ whose interpretation is the equivalence class generated by $[\![c]\!]_S$.

I will also, for convenience, add many new predicate symbols $\in$ with type signature $\in : S \times S/R \to 2$ that holds if and only if its left argument is in the equivalence class on the right.

An RFOL' structure $M'$ is just an RFOL structure $M$ constrained to satisfy the following rule:

For all sorts $S$ and all relations symbols $R : S \times S \to 2$, $[\![S/R]\!]$ is equal to $[\![S]\!]$ partitioned by the transitive, symmetric, reflexive closure of $[\![R]\!]$.

Answer 1

If I may advertise me and my coauthor's own work, our paper Observational Equality : Now for Good describes $\mathrm{TT}^{\mathrm{obs}}$, a relatively simple dependent type theory that is a variation on Observational Type Theory.

The paper features a section about native quotients, with their typing rules (that are reminiscent of your example), computational behavior and their integration in the meta-theory.

---

Edited to add more details: the quotients we obtain are quotients for the propositional equality, which means that if $xEy$ then $\pi(x) =_{A/E} \pi(y)$ where $\pi : A \to A/E$ is the quotient map, but the equivalence classes are generally not convertible.

As Andrej's answer explains, this allows us to preserve computational properties of the theory. However, allowing the formation of quotients by any proof-relevant relation (which might be a quotiented type itself) quickly leads to difficult coherence problems. Homotopy Type Theory embraces these higher coherences, while $\mathrm{TT}^{\mathrm{obs}}$ chooses to stay clear of them by only allowing quotients by a proposition whose proofs are all convertible.

Answer 2

I do not have specific suggestions for what type theories with quotients one might look at, but I would like to explain what sort of obstacle one faces when designing a proof assistant with quotients.

Suppose we are in some setting that supports the formation of the quotient $A/E$ of a type $A$ by an equivalence relation $E$. Let $q_E : A \to A/E$ be the canonical quotient map. We call $q_E(a)$ the equivalence class of $a$. Furthermore, let us assume that $$\frac{\vdash a \, E \, b}{\vdash q_E(a) \equiv_{A/E} q_E(b)}, \tag{1}$$ which is to say that equivalent elements of $A$ map to judgementally equal equivalence classes. We have lost decidable equality checking. To see this, let $A$ be the type of terms of a combinatory algebra,

data A : Set where
  K : A
  S : A
  app : A → A → A 

and let $E$ be the least equivalence relation generated by the equations $K \, x \, y = x$ and $S \, x \, y \, z = (x \, z)\, (y \, z)$. It is well known that $E$ is semidecidable but not decidable. Therefore, there can be no equality checking algorithm that decides equality (of closed terms) on the quotient $A/E$.

(If the ambient formalism does not support the definition of A, we may similarly cook up semidecidable equivalence relations on $\mathbb{N}$ that will do the job. Or we could take a finitely presented semigroup with an undecidable word problem.)

What shall we do about this? There are two obvious choices, both of which have been tried:

1. Keep the quotients and sacrifice decidability of equality checking.
2. Keep decidable equality and sacrifice (1) above.

The first option has serious ramifications on the design of the proof assistant.

The second option usually amounts to replacing (1) with a weaker version, say one that uses the identity type: $$\Pi(a, b : A) \,.\, a \, E \, b \to \mathsf{Id}_{A/E}(q_E(a), q_E(b)). \tag{2}$$ This is the approach taken in homotopy type theory and related systems. To distinguish between the two kinds of quotients, let me temporarily call those satisfying (1) judgemental quotients and those satisfying (2) propositional quotients.

There are at least two further reasonable design choices, which however I would not describe as “type theory with quotients“, as follows.

Thirdly, we can simulate quotients inside a type theory that does not provide them natively. One way of doing this is to use setoids, for example.

Fourthly, we might keep (1) but limit quotients to those formed by decidable equivalence relations. I am not aware of any explorations in this direction. I am not sure where this could lead, since quotients by decidable relations often exist “for free“, for example, a decidable equivalence relation $E$ on $\mathbb{N}$ has a propositional quotient already in a fairly weak type theory (something like Martin-Löf with sufficient amount of extensionality principles). What do we gain by postulating judgemental quotients by decidable equivalence relations?

Answer 3

Apart from observational type theory, the XTT type theory (https://arxiv.org/abs/2003.01491) also supports quotients via higher inductive types from cubical type theory.

In XTT, everything is set-truncated, so the quotient type does not need a truncation constructor, which is more convenient than the cubical type theoretical version.

The native cubical type theory also supports quotients, but IMO if you're not looking for higher-dimensional things, it will not be very useful (compared to OTT/XTT).