Post #1846810
2026-04-26 16:10 UTC
Replies (5)
-
@jonmsterling@mathstodon.xyz 2026-04-26 16:11
@carloangiuli I would put this in the same category as the other Padova school objections ;-)
-
@MartinEscardo@mathstodon.xyz 2026-04-26 16:14
@carloangiuli asks "Cursed follow-up: How many people think function extensionality *isn't* neutral?" In the same cursed talk I mentioned neutrality, I characterized function extensionality as "unavoidable" instead. See slide #5 https://martinescardo.github.io/.talks/escardo-venice2026-stone-types.pdf In any case, I wish I had never mentioned neutrality, because this turned out to be a big distraction from what I actually said and wanted to discuss. It backfired badly. @jonmsterling
-
@totbwf@types.pl 2026-04-26 16:41
@carloangiuli @jonmsterling I see a lot of confusion on this one from computer scientists who think that function extensionality removes the ability to distinguish between, say merge-sort and insertion sort. However, this is a question about the *codes* of functions, not the functions themselves.
-
@jpoiret@types.pl 2026-04-27 22:05
@carloangiuli @jonmsterling count me in the "funext isn't natural" camp 😈
-
@cdrichards@mathstodon.xyz 2026-04-28 17:05
@carloangiuli @jonmsterling filing this thread under “Dr. Funext, or: How I Learned to Stop Worrying and Love the Xi Rule”