Path induction

I tried to correct a few typos.

Independently of the changes proposed in this pull request, I think we might insert a sentence before the "Define" on line 1759 https://github.com/HoTT/book/blob/master/preliminaries.tex#L1759 to introduce the element a:A, the family C(y,p):U, and the element c:C(a,refl_a).