Post #1846835
2026-04-28 06:54 UTC
@jonmsterling Wait, what's the problem with congruence of equality? https://www.xn--pdrot-bsa.fr/articles/quotett.pdf does have the J eliminator, no?
@mevenlennonbertrand @jpoiret @carloangiuli
Replies (2)
-
@jeanas@mathstodon.xyz 2026-04-28 06:57
@jonmsterling Or did you mean congruence of definitional equality and specifically the xi rule / conversion under lambda? Pédrot's paper achieves it, unlike previous attempts. @mevenlennonbertrand @jpoiret @carloangiuli
-
@jonmsterling@mathstodon.xyz 2026-04-28 07:44
@jeanas @mevenlennonbertrand @jpoiret @carloangiuli Thanks for sharing this! I think I haven’t seen it yet.