General method for disproving possibility of judgemental equality

Question

There is a slick definition of categories (as a record type with eta-equality) such that taking the opposite category twice results in the original one judgementally. Similar tricks seems to exist for judgementally associative path concatenation etc.

However, it would be unlikely to be able to give a slick definition of, say, natural numbers that satisfies the universal property (propositionally), and come equipped with addition and multiplication which satisfy judgemental laws of semirings, inside ordinary MLTT. Usually, a way to prove this is to argue that it renders type checking undecidable, by giving a reduction of the halting problem to typechecking. However for this example it doesn't work because it seems that typechecking of MLTT + Natural numbers with primitives for addition and multiplication with said judgemental equalities is still decidable. (I haven't checked, but this looks plausible and there are similar looking results.)

Is there then a way to argue that this is indeed impossible, no matter how clever and funky the encoding is?

Answer 1

This is a really interesting question! I'll try to give some pointers to some possible answers.

One more general question you might ask is

What equivalence relations have constructive quotients?

Namely: given a type $A$ and a decidable equivalence relation $\sim$ over it, can we construct a type $\overline{A}$ and functions $$ ||\cdot|| : A \rightarrow \overline{A}$$ and $$ \mathrm{lift} : \overline{A} \rightarrow A$$

such that $$ a \sim b \Rightarrow ||a|| =_{\beta\eta} ||b||$$ and $$ ||\mathrm{lift}(a)|| =_{\beta\eta} a$$ for every $a$, $b$ of the appropriate types. One may also want the equalities to hold on open terms.

In the more general case, beyond $\beta\eta$, it is known that there are examples of (decidable!) equational systems which do not admit completion, that is that it is impossible to turn them into rewrite systems which are confluent and terminating (as is $\beta\eta$).

This suggests that there may be some decidable $\sim$ that do not admit such a nice embedding. What of the specific case you mention, where $A$ is the "free semiring" and $\sim$ is the corresponding equational theory?

Well here we do run into problems with commutativity: if we had such a $||\cdot||$ working on open terms, then any $t = ||x + y||$ needs to contain both $||x||$ and $||y||$ somehow (and therefore $x$ and $y$ themselves), and $||y + x|| = t[y/x, x/y] = t$, but this is not possible, because the position of $x$ in $t$ must be different from the position of $y$ in $t$!

Note that this argument completely disintegrates on closed terms, and for good reason.

A common solution is to use reflection to turn a term into a syntactic form that does not actually contain variables (they are replaced with, say integers which can be computed with), and in the case where $\sim$ is decidable on closed terms, compute a function which returns the appropriate $\mathrm{bool}$! And hey this is what the ring tactic does in Coq!

---

It's worth noting that there is a class of problems which admit nice embeddings for which you get the appropriate computational equalities: e.g. free monoids over finite (decidable) sets. This subject is the matter of Normalization by Evaluation, for which there is extensive literature.