= Collection for Boolean-valued names
For a name $a$ and formula $\varphi$, 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\llbracket\varphi(u,v)\rrbracket$. 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.
Back to article page
