HoTT/book — pull request #624 by JasonGross (2014-01-30 22:48:09+00:00)
Title: Finite choice

I'm not sure if I should include a note about the exercise requiring
functional extensionality, or about the exercise not requiring the
assumptions that A(x) are sets and P(x, a) are mere propositions. I'm
also not sure if I should be marking an erratum for this.

This closes #623.