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?

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.