Given a *specific* isomorphism, in HoTT you get  a *specific* element of the identity type. 

Let me say this explicitly: equality in HoTT is not truth-valued. It collects all the possible ways to identify things. In the case of equality of types, the identity type collects the equivalences between them (rather than being the truth value expressing whether they are equivalent).

In fact, canonicity is at the heart of the univalence axiom: there is a canonical one-to-one correspondence between elements of the equality type (i.e. the identity type) and elements of the types of equivalences.

So, the univalence axiom just says that the elements of the good, old identity type can be understood to be precisely the equivalences. 

You may wonder what the bonus of this is. This is the content of my last two bullet points in my message.

Martin