> 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.
I don't think the principles that HoTT wants to take as axiomatic are actually fundamental or ontologically basic enough to be made axiomatic. Is that so shocking?
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.