Post #1846820
2026-04-26 16:41 UTC
@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.
Replies (1)
-
@carloangiuli@mathstodon.xyz 2026-04-26 16:45
@totbwf @jonmsterling Absolutely. Plus, omitting funext from ITT does not actually allow us to prove that mergesort and insertion sort have different properties!