Post #1846821
2026-04-26 16:45 UTC
@totbwf @jonmsterling Absolutely. Plus, omitting funext from ITT does not actually allow us to prove that mergesort and insertion sort have different properties!
Replies (1)
-
@jonmsterling@mathstodon.xyz 2026-04-26 16:49
@carloangiuli @totbwf When I was inventing the cost-aware-logical-framework together with Yue Niu, one of my goals was to show that type theory WITH funext was a good place to study the difference between mergesort and insertion sort. I remember that certain people looked at me funny, like how can that possibly work... LOL