News for hackers. Stuff that matters.
Re:With Category Theory, Mathematics Escapes from Equality (... by spekcular on Sunday March 27, 2022 @02:02AM (#30818081)
I understand this desire but I think people who believe this should develop a new word or description for what you're attempting to do. See my comment here: https://news.ycombinator.com/item?id=30817964

I want to emphasize I'm not policing semantics just for the sake of being ornery. My reaction is approximately the same as it would be to someone who sends me a graph theory paper and calls it number theory. These distinctions are useful.

Re:With Category Theory, Mathematics Escapes from Equality (... by jules on Sunday March 27, 2022 @07:24AM (#30819426)
Wouldn't it be amusing if a common english word like "foundation", usually referring to the thing on which buildings are constructed, is uniquely reserved for the all the kinds of things on which you can theoretically build all of mathematics, but where none of the people involved are actually trying to do that, and a different word has to be invented for a similar thing, because you got banned out of the club for trying to actually build mathematics on top of it.
Re:With Category Theory, Mathematics Escapes from Equality (... by Twisol on Sunday March 27, 2022 @02:07AM (#30818106)
Yes, I don't especially disagree; I also think words are most useful when they mean something consistent and precise. Nonetheless, I think it's worth separating the merely terminological disagreement from the deeper semantic disagreement. Please do see the article I found(!) in a cousin comment, by Penelope Maddy. I think it provides a very enlightening perspective on the ways in which ZFC and HoTT/UF both purport to be "foundations" and yet seek to perform different duties.
Re:With Category Theory, Mathematics Escapes from Equality (... by spekcular on Sunday March 27, 2022 @02:18AM (#30818155)
Thanks. I enjoyed the article you linked. I think the description on page 16 is a good summary of what most people working in foundations take the purpose of foundations to be.