How do you visualize $\mathcal{P}(1)$ in constructive mathematics? If I understand correctly, constructive mathematics doesn't prove that the powerset $\mathcal{P}(X)$ of a set $X$ is a Boolean algebra; in general, all we can say is that its a Heyting algebra. This seems a little paradoxical, because I can "prove" that $\mathcal{P}(X)$ is always a Boolean algebra. In particular, let $\mathbb{B} = \{0,1\}$. Then $\mathbb{B}$ can be made into a boolean algebra in the usual way. This means that for all sets $X$, the set of all functions $X \rightarrow \mathbb{B}$ becomes a boolean algebra under the pointwise operations; lets denote it $\mathbb{B}^X$. Hence, using the isomorphism between $\mathbb{B}^X$ and the powerset $\mathcal{P}(X),$ it follows that $\mathcal{P}(X)$ is a Boolean algebra.
Lets play the role of the detective: which line murders the proof? The only part of the proof that seems even slightly dodgy is the correspondence between $\mathbb{B}^X$ and $\mathcal{P}(X)$. So on this basis, it would seem that the correspondence between subsets and predicates doesn't hold constructively. My guess is that what's happening is that, constructively, we have an injective homomorphism $\mathbb{B}^X \rightarrow \mathcal{P}(X)$ defined by $P \mapsto \{x \in X \mid P(x)=1\}$, but that, in general, this homomorphism needn't be surjective. I guess this basically means that the ordered-pair $(\mathbb{B},1)$ fails to be a subobject classifier in the constructive category of sets.
At this point, I'm feeling pretty good about my ability to understand the very basics of constructive mathematics. Then I find this article, and I realize that I know nothing. In particular, consider the case $X = 1$, where $1$ is defined as the set $\{0\}$. This gives us a canonical homomorphism $\mathbb{B}^1 \rightarrow \mathcal{P}(1),$ or in other words $\mathbb{B} \rightarrow \mathcal{P}(1)$. Then rehashing what that article seems to be saying, it would seem that...

this function $\mathbb{B} \rightarrow \mathcal{P}(1)$ still isn't surjective! Or rather, it isn't surjective "in the strong sense." But, it is surjective "in the weak sense."
Definitions:
  
  
*
  
*Surjective in the strong sense: for all $y \in Y$, there exists $x \in X$ such that $f(x) = y$.
  
*Surjective in the weak sense: its not the case that there exists $y \in Y$ such that for all $x \in X$, we have $f(x) \neq y$.

So $\mathcal{P}(1)$ has precisely two elements "in the weak sense," but not "in the strong sense."
Woah!
What?
Hmmm.
Okay....
..I don't get it.

Question. How do you visualize a set that has two elements "in the weak sense" but not "in the strong sense"? More precisely, how do you visualize (or otherwise understand) $\mathcal{P}(1)$ in constructive mathematics?

Also, is it true that $\mathcal{P}(1)^X$ is isomorphic to $\mathcal{P}(X)$ constructively?
 A: Sufficiently constructive mathematics has semantics in a topos. In a topos there is on the one hand the subobject classifier $\Omega$, and on the other hand the coproduct $2 = 1 + 1$ of two copies of the terminal object. I believe the inclusion $1 \to 1 + 1$ of, say, the left copy of $1$ is a monomorphism in a topos, and hence it is classified by a map $2 \to \Omega$. There is no reason this map should be an isomorphism in general. 
Consider, for example, the topos $\text{Sh}(X)$ of sheaves of sets on some topological space $X$. The subobject classifier $\Omega$ turns out to be the sheaf of continuous functions to the Sierpinski space, which I will also denote by $\Omega$; that is, it assigns to an open $U$ the set of continuous functions $U \to \Omega$, or equivalently the set of open subsets of $U$. 
The coproduct $2 = 1 + 1$ of two copies of the terminal object is the sheaf of continuous functions to the discrete two-point space, which I will also denote by $2 = 1 + 1$; that is, it assigns to an open $U$ the set of continuous functions $U \to 2$, or equivalently the set of clopen subsets of $U$. These are clearly not the same in general. 
Okay, now let's talk about elements. The elements of a sheaf $F$ are the morphisms $1 \to F$, or equivalently the global sections. Hence the elements of $1 + 1$ are the clopen subsets of $X$, and the elements of $\Omega$ are the open subsets of $X$; in particular there are, externally, elements besides $\emptyset$ and $X$. But this is different from there being elements besides $\emptyset$ and $X$ internally, as follows. (I think. I'm not an expert, so what follows might be the wrong semantics, and if someone corrects me then they're probably right.) 
The elements of $\Omega$ form a Heyting algebra (the Heyting algebra of open subsets of $U$), and in this Heyting algebra $\neg U$ is the interior of the complement of $U$. Hence the statement $\neg U$ is true iff $U^c$ has empty interior. The statement "it's false that $U = \emptyset$, and false that $U = X$" is $(\neg U) \cap (\neg \neg U)$, and so the statement "it's false that (it's false that $U = \emptyset$ and false that $U = X$)" is
$$\neg (\neg U \cap (\neg \neg U)).$$
This evaluates to true (equivalently, $X$)! This is because $\neg U$ and $\neg \neg U$ are disjoint. The constructive proof is that given $\neg U$ and $\neg \neg U$ we can deduce $\bot$ (false, or $\emptyset$), and by definition $\neg P$ means that from $P$ we can deduce $\bot$. In other words, it's still true constructively that $P$ and $\neg P$ imply $\bot$, hence that $P \cap \neg P \Rightarrow \bot$, hence that $\neg (P \cap \neg P)$. But constructively this is no longer equivalent to $\neg P \cup P$. 
