markusdeEverybody gangsta about being correct by construction until they hear about grade school arithmetic
Max S. New ⚜️@markusde I think this post is designed in a lab to piss me off and yet I am too zen to take the bait
bhakti@bhaktishh @markusde do your worst
bhakti (@[email protected])
dumb category theory question that might not even make sense. I am incapable of thinking about arrows without thinking about them as functions on sets so that’s probably where is coming from So the identity arrow is the identity on composition, but can you ever construct an arrow that obeys the compositional identity but isn’t “truly” the identity? Or is there no notion of “true” identity for an abstract object as there is for a set (ie mapping each thing to itself)
@maxsnew maybe it won’t piss you off but will certainly make you wonder if I really know any category theory at all
@bhaktishh I almost dropped out of being a math major because I couldn't understand wtf was going on in my abstract algebra class so I have personal experience with these kind of questions.
@maxsnew unrelated but I *did* drop out of being a math major because I couldn’t understand why we cared about any part of real analysis. Maybe if I had the chance to take algebra before analysis I would have made it through … or not … we’ll never know
@bhaktishh @maxsnew Physics, reality, etc?
@bhaktishh @maxsnew I did do math but I didn't really start caring about analysis until I started working with verified probability stuff, where describing even exact programs that only involve integers can still need real numbers
Cody
Koz Ross
Morgan Arnold@bhaktishh @markusde @maxsnew you can do a whole lot of real analysis without believing in the real numbers! i say this as someone who does analysis and also doesn't tend to believe in the real numbers. errett bishop wrote an excellent book on real analysis from the constructivist point of a view.
a lot of classical theorems from analysis don't hold anymore (i.e. the intermediate value theorem), but it turns out that you can recover fairly similar constructive analogues of a lot of these theorems! and a lot of classical theorems should still work just fine constructively! off the top of my head, the picard-lindelhöf theorem and the weierstrass approximation theorems should still hold
@bhaktishh @markusde @maxsnew i also know that within my discipline of differential geometry there have been some really cool ideas which could be used to put the whole field on constructive footing, like locales as constructive analogues of topological spaces, or the synthetic differential geometry of lawvere. unfortunately, these ideas were discovered by category theorists, who don't seem to write down their ideas in a manner which is accessible to non-category theorists
@mra @bhaktishh @maxsnew OK I can never really tell if you're joking on here but people who unironically use the phrase "belief" when it comes to mathematical foundations then you belong in viXra prison with NJ Wildberger.
Do you really do purely synthetic differential geometry in your research? Love that for you if true but consider me skeptical.
zwarich@markusde @mra @bhaktishh @maxsnew I first got interested in topos theory long ago because of this promise of synthetic mathematics. In practice, it seems to be the sort of thing you consider after proving both results rather than using one to derive the other. And even in theory, composing distinct synthetic perspectives seems very difficult. I had hoped that proof assistants might lead to more uses of these techniques, but it hasn’t yet to come to pass.
Another sort of alternative mathematics with a transfer principle is Robinson-style nonstandard analysis, and despite many of the analogous problems being more subdued in that setting (it is much easier to include things built from the reals in a nonstandard superstructure), it alo has essentially no real usage.