HoTT/book — pull request #694 by jledent (2014-07-09 10:09:49+00:00)
Title: sigma instead of exists in the proof of 10.5.8.(ix)

The idea is that we want A' to be the subset of A (in the sense of §3.5) such that C(f x).
So the sigma mustn't be truncated, otherwise we cannot define the inclusion i : A' -> A.

Jérémy