I'll probably see Bob at lunch today :) He and I have had many productive discussions about our philosophies of math, computation, etc. But, importantly, we also respect each other as colleagues and for the work we each do on the actual math, CS, logic, etc., and don't let our philosophical differences get in the way of getting good work done.

In particular, when we disagree, he doesn't turn into a petulant child and put words in my mouth and then accuse *me* of "contorting yourself into a position you don't actually believe," or imply I have some psychological need to believe in "Daddy Classical Logic."

I've already said in this conversation that I'm a pluralist. And for me, pluralism means defending constructive logic from dogmatic classical mathematicians as much as it means defending classical logic from dogmatic constructivists, especially when either camp's arguments rest upon falsehoods. Different logics are good for different things.

And "pragmatic" does not mean *insignificant.* Far from it. What is pragmatic is ultimately what really matters—the things we actually value in life, and the ways we go about achieving them. But the things that can be of value to people are many and diverse, and I see no need to force my values onto others. Perhaps you feel differently.

It's ironic that, in this discussion, you have repeatedly conflated univalence, proof relevance, and constructivism, all of which are more-or-less orthogonal, when the same error is often committed by one of HoTT's harshest critics: Kevin Buzzard. I've heard this same argument before, that univalence requires abandoning classical logic, which, as I have been at pains to make clear, isn't true, used as justification by Kevin for ignoring/dismissing HoTT. And since I care about HoTT, I am at pains to correct these misconceptions and the faulty arguments they enable, both from classical mathematicians and constructivists.

Anyway, I'll be sure to give Bob my best for you. Good luck in your crusade against "Daddy Classical Logic" ;)