what does it mean for a function "not to respect equality"

I disagree with the interpretation of the author's intent in the other answer. This answer by Andrej Bauer seems more relevant. I'll try to adapt it below, but I highly recommend reading the excellent Bauer post I linked.


Consider sets $X$ and $Y$ each equipped with an equivalence relation, and the axiom:

$\forall R \in |X| \times |Y| . \left[\forall x \in X \exists y \in Y . R(|x|,|y|)\right] \implies \left[\exists f \in Y^X \forall x \in X . R(|x|,|f(x)|)\right]$

where $|a|$ is the equivalence class of $a$, and $|A|$ is the set of equivalence classes of members of $A$.

If you think of $X$ and $Y$ as sets of "representations" of the "real" objects, and the quotient map to the equivalence classes as mapping representations to the objects, then the axiom states that if $R$ is total, then there exists a choice function $f$ for the representations. There is no condition that $x' \in |x|$ implies that $f(x') \in |f(x)|$.

In the context of a (suitable) type-theory, you indeed get this for free by taking $f$ to be the witness of the assumption $\forall x \in X \exists y \in Y . R(|x|,|y|)$.

In contrast, this axiom but with the addition of the condition of respecting equality is too strong: it can be used to decide the halting problem (see Bauer's answer for details).


Let's explain extensional and intensional equality with an example in an ordinary number system. Is $x(y+z)$ the same as $xy + xz$? Their outputs are the same for the given inputs, but they are technically not the "same" function. So even though they're extensionally equal (their external properties are equal to each other) they are not intensionally equal (internally the same function).

Probably the author means "respect equality" in terms of the "intensional equality" they define immediately above this, as functions which satisfy this predicate need not be equal in this sense.

Tags:

Type Theory