That said, there is a design space here and while SDG is close enough to ordinary mathematics that you can explain it to high-school students, it might not be the best fit for developing modern physics. There are several different approaches (e.g., working in the internal language of a "synthetic differential infinity-topos") which seem promising. It's an area of active research and one that is still extraordinarily difficult to get into.
This particular pair I understand only indirectly, I somewhat understand the relationship between linear logic and Lie groups and constructive mathematics and linear logic and this is a transitive relationship.
Edit: in the presentation they mention “In constructive mathematics, there can also be numbers† d such that d^2 = 0 but not necessarily d = 0.”. They are talking about alternarivity, one of the three requirements for a Lie algebra https://en.m.wikipedia.org/wiki/Lie_algebra
In regular mathematics there can be nonzero numbers whose square is zero (for example, the “dual numbers”). But I don’t see how this has anything to do with constructive vs nonconstructive mathematics.
You didn’t do the reading so hold your horses with hopelessly.
From the slides “In constructive mathematics, every function is continuous”. (From the presentation)
Sounds like Lie groups to me.
I’m aware of dual numbers funny that you bring them up as they correspond to Lie groups. I have been talking about dual quaternions nonstop on hn.
Adjoints are everywhere [1]. Referencing adjoints is indeed pretty vague. You can't make a case for why things are interesting by quoting a bunch of resources of other people making cases why things are interesting. (I guess you can, but then, why make the argument at all if it is not yours?)
You don't even need funny names to get x^2=0. This is true for any of the two elements of the group of order 2.
Linear logic is indeed having a mini revival, but so is general category theory. I don't see the particular advantage for people to evangelise certain parts of mathematics, especially if the case being made is not clear.
[1] Not attributed to me.
That’s like your opinion, man.
You conveniently ignored the continousness of both constructive mathematics and Lie groups.
Did you read the paper on chu spaces and constructive mathematics? What did it say about adjoints?