Post #1846812
2026-04-26 16:14 UTC
@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
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-04-26 16:15
@MartinEscardo @carloangiuli At your birthday meeting, I had a very long discussion with Milly about these issues... I did not come away convinced, but I think I got a bit closer to understanding her point of view.