HoTT/book — pull request #749 by Pierre-Yves-Gaillard (2014-12-23 09:57:19+00:00)
Title: Type theoretical axiom of choice, Section 1.6

This is about lines 820 to 827 of

https://github.com/HoTT/book/blob/master/preliminaries.tex#L820.

Since there is a display ending with no punctuation mark between two complete sentences, I believe something needs to be fixed, but, even if I am right, there is probably a better fix.