Fair enough. I just wanted to elaborate, because usually that specific phrasing justifies the opposite. I did mention you partially acknowledged the meaningfulness, but I felt like the point needed to be made stronger. The politics around foundations obfuscates a lot of their utility. I'm sure you're aware the tendency for randoms in a mathematics department to roll their eyes when you pay lip service to other foundations. Usually, it's not even about a sense of pragmatics, but irrational identity-protectionism and ZFC dogmatism. Things like HoTT, or any branch of TT, are percieved as "cute, but not something with any real usecase. Not like my perfect ZFC!"