Clarification about judgmental unequality

[Yosuke-Ito-345]

In Exercise 5.2, the book states:

Construct two functions on natural numbers which satisfy the same recurrence $$( e_z, e_s )$$ judgmentally, but are not judgmentally equal.

However, as far as I understand from discussions on the HoTT Zulip chat, we cannot prove judgmental unequality using only the material developed in the book. It might therefore be helpful to include some clarification about judgmental unequality, so that readers do not try in vain to prove formulas like $$f \equiv g \to 0$$.

[awodey]

I hope that no one would try to prove $$f\equiv g \rightarrow 0$$, because that's not even a formula/type, since judgmental equality is not one. : - ) But you are right that the book doesn't provide any way to show that a judgmental equality is not provable (except maybe to show that it's false), and if the ``recurrences'' are judgmentally equal, then that should not be the case. So something should indeed be fixed here. Who wrote that exercise, and what did they have one mind?

[Yosuke-Ito-345]

@awodey
Thanks for your comment. To be honest, I tried quite hard to prove $f \equiv g \to 0$, although I may be an exception.
By the way, I did not know that judgmental equality is neither a type nor a term. Is it something like a meta-level symbol? I also read the Appendix A, but I still do not fully understand what judgemental equality is.

[mikeshulman]

I don't know who wrote the exercise. It might even have been me. But (as I said on Zulip) I think the most straightforward fix is to change the exercise to say something like "not obviously judgmentally equal", which I suspect is basically what the author had in mind.

[mikeshulman]

As for what judgmental equality is... it's a judgment! (-:O

[Yosuke-Ito-345]

Thank you for sharing the document. I did not expect to find such detailed material explaining the concept of "judgment".

[awodey]

Good n-lab explanation - I hadn’t seen that. Thanks!