HoTT/book — pull request #455 by cangiuli (2013-08-23 01:19:24+00:00)
Title: Fixing Section 2.9, closing #446.

We say "...given...p as before", and it was correctly annotated in the previous occurrence. Thus my fix was to simply remove the part where we repeated the assumption of p (with the wrong type!).