In reading the HoTT book, I have found that it is easy to become bogged down in detail and hard to tell the general 'big picture' of what is going on. I hope to get some general answer to the following two questions.
I know the statement of the univalence axiom, which is, for types $A$ and $B$ in some universe $\mathcal{U}$ $$ (A = B) \simeq (A \simeq B). $$ This is usually written down along with an interpretation something like "If A and B are equivalent as types then they are equal as types", but this doesn't seem quite right - it's only true up to equivalence. Why do we ignore the equivalence in the axiom, and treat the two as if they were actually the same?
I know what path induction says, and how it is used. What I don't know is its 'status': is it a theorem? an axiom? Something else that's familiar to type theorists but doesn't have an easy interpretation for a mathematician? I know that path induction is 'the induction principle for identity types', but does that mean that it is bundled up as part of the definition of identity?
Any help appreciated.
idtoequiv
takes an equivalence and returns an element of (A = B), i.e. a witness to the fact that they are propositionally equal? In which case, why is it important for the axiom thatidtoequiv
is an equivalence? Wouldn't it be enough merely to have a function from $A \simeq B$ to $A = B$. $\endgroup$