HoTT/book — pull request #435 by akissinger (2013-07-29 11:29:14+00:00)
Title: Simplify type of D in proof that path induction implies based path induction

In the proof in section 1.12.2 that path induction implies based path induction, the definition of D can be simplified, because the type of C need not depend on "p : x = z". Changing to a non-dependent version matches the premise of based PI better and avoids confusion, since currently p occurs both free and bound in the definition of D.