Post #1846827
2026-04-27 22:30 UTC
@jpoiret @carloangiuli Well, we said “neutral” not “natural”. But of course it’s both: otherwise it wouldn’t be the mathematics of functions. A formalism serves mathematics, not the other way around.
Replies (1)
-
@jpoiret@types.pl 2026-04-27 22:46
@jonmsterling @carloangiuli oops, i guess it's getting late and i misread the word! In any case, I'm very much intensionally-minded: while you can't distinguish extensionally equal functions internally, when i prove that two functions are equal I do mean to say that they are implemented in the same way. Otherwise I would be proving that they are extensionally equal. If you add funext, this distinction isn't possible anymore, which mean you trade nuance for convenience. Don't get me wrong, convenience can be very nice, but I also like having this precise tool for specific applications!