[auggierose]

I already read the introduction a couple of months ago, pretty much on the day when they officially announced that the book is available.

From what I understand: If you are a type theorist / constructivist, then certain constructions will not be provably equivalent, although their classical counterparts are. Some of those classically trivial equivalences might be recovered though via the univalence axiom. Is that correct or totally wrong? Furthermore it seems to me from the discussions with fmap, that if I am a classical mathematician, I cannot use HoTT (unless I am willing to compromise and give up some of my power).

[ek]

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.