Return to Answer

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)$ is 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?

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?

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)$ is 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 decidable equality.
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 some quotients always 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?

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)$ is 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?

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)$ is 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 decidable equality.
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)).$$ This is the approach taken in homotopy type theory and related systems.

There is a third option, which I would not describe as “type theory with quotients“. Namely, 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.

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)$ is 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 decidable equality.
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 some quotients always 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?