> It is sometimes quite useful in practice to recognize that two isomorphic objects are not literally the same. So I am skeptical of any approach that wants to blur those distinctions.

This paragraph betrays that you have not done much work at all with HoTT. Type theory would be inconsistent if distinguishable objects could be substituted. It is not accurate to say that they are treated as "literally the same". Indeed the whole point of HoTT is that substitutive equality is not the only useful kind.