< [[nlab:Sandbox]] Back to neutral constructive foundations. $$\ostar$$ A proposition consists of a boolean-valued type family $b:\mathrm{bool} \vdash P(b)$ such that * for all booleans $b:\mathrm{bool}$, $P(b)$ is a subsingleton * the dependent product type $\prod_{b:\mathrm{bool}} P(b)$ is empty. [[!redirects Sandbox > history]]