HoTT/book — pull request #419 by zhenlin (2013-07-15 05:08:10+00:00)
Title: Fix a couple of typos in §5.3.

The textual description of sup contradicts the displayed type of sup in §5.3 (p. 195 in the ebook edition of version 207-g21ac918): sup should take a term of dependent sum type as input, not a term of dependent product type. The textual description also has a variable shadowing problem.