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)
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
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?