>>11027916I posted the LEM fact and I like category theory, but I don't think the later can practically stand on its own. Categories (let alone topoi) don't seem to have a good way of being taught and so you'll always fall back to standard algebra first.
Nonetheless, knowing that e.g. the exterior derivative d is in fact a natural transformation may help remembering or viewing rules such as pic related, i.e.
d(f* ?) = f* d?
In any case, LEM is literally not a necessity and makes live harder if you want to implement things, see e.g.
https://en.wikipedia.org/wiki/Constructive_analysis#The_intermediate_value_theoremAnd don't get me wrong, this is not to say one shouldn't study the nice theories that assume LEM. But it should be made explicit. It's a shortcut axiom that break a bunch of theories as well as symbol/computer implementation
https://en.wikipedia.org/wiki/Realizability>>11027930Most mathematicans live with the most naive pre 1900 Frege notion of extensional equality. There's a point to higher categories and not necessarily accepting artifacts of model theory.
E.g. if you take the standard definition of the ordered pair and natural numbers in the set theoreitcal foundation (Kuratowski pair and Neumann ordinals)
(a,b) := {{a},{a,b}}
0={}, 1={0}, 2={0,1},...
then you see that it's a theorem that the pair that holds the number 1 and the number 7 provably has the number 0 as an element. This accidental theorem shit doesn't happen with foundations that only use universal constructions, because things are set up relational, not material.
I'm not the promised land guy, but it's easy to argue that it's more than just a tool. At least if you're more philosophically/fundamentally inclined.
