# Meaning of the univalence axiom on plain data types

I'm trying to wrap my head around HoTT and can't figure out the intuitive meaning and validity of the univalence axiom. IIUC this axiom says:

UA: ∀ A,B:Type . (A = B) ≃ (A ≃ B)


where X ≃ Y is a shorthand for (X → Y) ∧ (Y → X).

When I take A and B to be propositions, this makes a lot of sense: it basically gives my that two equivalent propositions can be considered as equal, and given some form of proof irrelevance it makes perfect sense.

But how can it make sense when A and B are, say nat and bool, for example? I can trivially define a function of type nat → bool as well as a function of type bool → nat, yet it doesn't make sense to me to state that nat = bool. So is there some detail of the definition of UA that prevents its use on things like nat/bool, or does it really also apply in this case, in which case does it mean that the usual understanding of the refl elimination needs to be refined so it's not just a sort of type-cast any more but has potentially non-trivial computational content?

• Your definition of X ≃ Y is wrong, see the correct definition. – Andrej Bauer May 15 '15 at 21:42
• Aha! Thank you, Andrej. That all makes a lot more sense now. – Stefan May 16 '15 at 13:18