Two questions on homotopy type theory
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.
The univalence axiom is not intended to compress or ignore the type of equivalences between two types by telling that they can only come from an identification. Its effects go rather the other way around. It explains you what the identity type of a universe is by telling that finding an equivalence is the exact thing you have to do to find an identification between two types. For all you know (and as you mention), a universe which does not satisfy univalence could be a set. So you could take the point of view that rather than ignoring equivalences the univalence axiom is inflating identity types in a very precise way.
There is a very good reason to require univalence, and it is to find lots of families types. Taking the point of view that a type family over a type is expressing a property of that type, it would be a shame if we couldn't be expressive using type families. A family of types can be seen as a function into the universe. Since functions have to preserve identifications and since you sometimes have to prove explicitly that your construction of the type family preserves identifications (for example, when your making a family over a HIT), then the univalence axiom comes in very handy because now you know that you can find an identification between two types by finding an equivalence instead.
To answer your second question: in homotopy type theory, identity types have the status of a basic type constructor (as is the status of dependent function types, too) and the induction principle (or dependent elimination rule) comes with them. So they are simply assumed to be present. That's it, as far as the book is concerned.
But there are people looking for models of type theory with identity types. For instance, Awodey interpreted identity types by means of a factorization of the diagonal $A\to A\times A$ into a trivial cofibration followed by a fibration (this would be the `easy' interpretation for a mathematician, at least if (s)he's working with Quillen model structures). Showing that the object through which this diagonal factors indeed has the induction principle of identity types is a theorem.
The univalence axiom is best understood as defining what it means for two types to be equal. Under the propositions-as-types principle, a term of type $A = B$ is a "proof" that $A$ and $B$ are equal; and most mathematicians would say that such a "proof" is precisely an equivalence (or isomorphism) between $A$ and $B$.
Since path induction yields a canonical function $(A = B) \to (A \simeq B)$, it is natural to ask that this function be an equivalence. We do not simply ask for a function $(A \simeq B) \to (A = B)$ because we want to know that the two constructions are mutually inverse (up to some further equalities), so that the type $A = B$ is determined (up to equivalence).
It's worth pointing out that, in the absence of univalence, it is possible that the only term of type $A = B$ is (propositionally) equal to $\mathsf{refl}$ (and in particular, having a term of type $A = B$ implies $A \equiv B$).
As for path induction in ordinary (i.e. proof-irrelevant) mathematics: in some sense it corresponds to the indiscernibility of identicals, but that is so obvious as to be almost meaningless.