I hope this question isn't too obfuscated (or easy)!


Given a set $S$, let $S\_\perp$ denote $\{X \in \mathcal P(S) \mid \forall x, y \in X.\, x=y\}$, the elements of which are *subsingletons*. In the following $Y\_\perp^X$ means $(Y\_\perp)^X$.


The question is: *does a partial map between $X$ and $Y$ that doesn't have $\emptyset$ in its image determine a subsingleton of maps between $X$ and $Y$ which is non-empty?*


The same thing written more accurately with symbols: Assume that we have an element $F$ of $Y\_\perp^X$ that doesn't have $\emptyset$ in its image. Can we conclude that there exists an element $F'$ of $(Y^X)\_\perp$ such that $F' \neq \emptyset$ and $\forall f' \in F'.\,\forall x \in X.\,f'(x) \in F(x)$?


In the presence of Excluded Middle, this question is easy. In its absence, it seems much harder.




---


**This is my main lead right now:**


We assume the the Axiom of Unique Choice.


We need to prove that $$\begin{align}
\forall x\in X. (\forall y, y'. \phi(x,y) \wedge \phi(x,y') \implies y=y') \wedge (\neg\neg\exists y \in Y. \phi(x,y)) \tag{1}
\end{align}$$
implies
$$\begin{align}
\neg\neg \exists f \in Y^X. \phi(x,f(x)). \tag 2
\end{align}$$


We can use the fact that $p \implies q$ implies $\neg\neg p \implies \neg\neg q$, and the Principle of Unique Choice. The calculations seem quite difficult. We would need to get (1) into the form
$$\begin{align}
\neg\neg(\forall x\in X. (\forall y, y'. \phi(x,y) \wedge \phi(x,y') \implies y=y') \wedge \exists y \in Y. \phi(x,y)) \tag{1'}
\end{align}$$



Does a map over subsingletons determine a subsingleton over maps?
Under Unique Choice, this implies ¬¬LEM.


Let $X=\Omega$ be the set of truth values, let $Y=2\subseteq\Omega$, and let $\phi$ be equality.


Then $\phi$ is a partial function, and $\neg \neg (x = \bot \lor x = \top)$ holds for any $x$, so the statement would imply that $\neg\neg \exists f:2^\Omega.\forall x:\Omega.x=f(x)$, so $\neg\neg\forall x:\Omega.x=\bot \lor x=\top$, which is ¬¬LEM.


