Post #1846828

2026-04-27 22:46 UTC

@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!

Replies (2)

@jonmsterling@mathstodon.xyz 2026-04-27 22:49

@jpoiret @carloangiuli I would say you are free to do what you want, but I also think it’s not correct usage to speak this way of functions. Why not instead speak to algorithms and codes, which are also mathematical objects very much worthy of study alongside functions? Is it mandatory, to maintain complete omertà when it comes to the mathematical notion of functions? It isn’t right say that this is a matter of trading nuance with convenience. We can walk and talk at the same time. Functions and their code are different mathematical objects. We should be able to talk clearly and precisely about both.

Open ##1846829
@maxsnew@types.pl 2026-04-28 03:12

@jpoiret > I also like having this precise tool for specific applications! I'm curious to know what specific applications you have in mind. @jonmsterling @carloangiuli

Open ##1846839