HoTT/book — pull request #693 by ahorn (2014-07-05 16:06:08+00:00)
Title: Fix ind(D,d,x,y,p) in (i), (ii) and (iii) of Lemma 2.1.4

If I understand Section 1.12.1 (Path induction) correctly, ind(D,d) : \Pi_{x,y : A} \Pi_{p : x = y} D(x,y,p) where d : \Pi_{x : A} D(x,x,refl_x). There may be some convention that I have overlooked on my first reading of the book but I thought in reviewing the proof of Lemma 2.1.4 (i), (ii) and (iii) that it would require a small fix to be consistent with the path induction principle given in Section 1.12.1.

With kind regards,
Alex