@mevenlennonbertrand@lipn.info
Post #1846833
2026-04-28 06:39 UTC
@jonmsterling @jpoiret @carloangiuli Whoop my bad I got mixed up. Indeed the "reasonable' version you need for synthetic computability is compatible. A quoting operation properly integrated in the type theory is a pretty funny thing, and that one contradicts funext, but it's arguably even more niche than CT.
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-04-28 06:44
@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.