[tel]

I would like to see more clarification of why you'd call HoTT OO. I have no doubt you can encode those things, but I find it strange to try to argue that it doesn't have more in common with the FP tribe than the OO tribe. Given that neither term is terrifically well-defined, I think that's the best you could argue.