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.