@DanDoel I don't think I understand what you are saying there. Do you agree that even in an intuitionistic meta-theory, the set $\{0,1\}$ and the set $\{\varnothing,\{1\}\}$ are isomorphic? In that case the important point is that we don't get to assume we have proofs about statements like $M(p) = y$. Re-interpreting the co-domain of $M$ in some other form seems like a matter of style.

The powerset of $\{1\}$ is just two values, so it seems the same as using $\{0,1\}$. Why is it important to use the powerset?

Thanks, the de Swart dissertation seems interesting.

I tried to semi-formalize the first part of your answer, as far as I understood it, and updated my question with the results. Can you let me know if I said anything wrong, or if I didn't get your meaning properly? Thanks.