Your understanding of univalence seems essentially correct to me.
At this point we are mostly debating what "can use" means -- it's probably enough to say that unless you reframe your thinking, perhaps radically, probably it will be hard for you to be able to use HoTT to get work done. It is possible to do classical mathematics within HoTT, in the normal way, but it would not be very fun.
At this point we are mostly debating what "can use" means -- it's probably enough to say that unless you reframe your thinking, perhaps radically, probably it will be hard for you to be able to use HoTT to get work done. It is possible to do classical mathematics within HoTT, in the normal way, but it would not be very fun.