The reason is that \(\Pi x {:} A. \Sigma y {:} B. C\) is the type of functions which map elements \(x {:} A\) to pairs \((y,z)\) with \(y {:} B\) and \(z {:} C\). The choice function \(f\) is obtained by returning the first component \(y {:} B\) of this pair.