Today I got to have the full #intuitionist #constructivist #maths experience.

First, somebody half-jokes that if one is a constructivist, then one's friends won't talk to them anymore.

Then, somebody else says that #constructivism is a deviant counterculture.

At this point, like a fool, I link Bauer's "five stages" paper: https://www.ams.org/journals/bull/2017-54-03/S0273-0979-2016-01556-4/S0273-0979-2016-01556-4.pdf

But alas, somebody actually reads the paper, and they think that the whole paper is a joke. They have two concrete questions, which I answer using relevant examples.

This was all in the context of #homotopy #TypeTheory, for what it's worth.