 Collection for Boolean-valued names

For a name $a$ and formula $\phi$, form the set of pairs $(u,p)$ with $u$ in the immediate domain of $a$, $p$ a Boolean truth value, and some name $v$ satisfying $p\le a(u)\wedge [[\phi (u,v)]]$. Full separation makes this a set, and intuitionistic collection gives a set of witness names covering all its pairs. A name with these witnesses in its domain collects the entire Boolean value of every existential assertion over $a$, without selecting one witness whose value is top. No choice or maximum principle is used.