/sci/ - Science & Math

Can someone explain all of HoTT to me, or at least the general idea?

I've read about half of it, I still don't understand what path induction is.
How can you form a judgement about an identity type x = y solely by proving it for the reflexive type x = x?
The book calls it the induction principle for identity types.
Is the principle an axiom?