Post #1846834
2026-04-28 06:44 UTC
@mevenlennonbertrand @jpoiret @carloangiuli Yes… I am also concerned about those hypothetical quoting operations because I think if you want to include them you have to give up a lot more than funext: you must give up the congruence of equality, and at that point you are NOT doing type theory, so it’s not part of this debate, which is about type theory.
Replies (1)
-
@jeanas@mathstodon.xyz 2026-04-28 06:54
@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