HoTT/book — pull request #731 by mikeshulman (2014-10-21 05:59:27+00:00)
Title: Fix some problems with Lemma 7.5.12

The converse direction of Lemma 7.5.12 is false unless Q is fiberwise merely inhabited. Also, there was a typo in the proof. (I discovered both of these things while Coqing it.)