# Does a map over subsingletons determine a subsingleton over maps?

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}

• Maps from $Z$ to $(Y_\bot)^X$ are in one-to-one correspondence with maps from subsets $R\subseteq Z\times X$ to $Y$, and maps to the subset of $(Y_\bot)^X$ singled out by "no $\varnothing$ in the image" corresponds to those $R$ with $\forall\ z\ \{x\mid(z,x)\in R\}\ne\varnothing$. Maps from $Z$ to $(Y^X)_\bot$ are in one-to-one correspondence with maps from subsets $Z'\times X\subseteq Z\times X$ to $Y$, where $Z'$ is any subset of $Z$, and maps to the subset of $(Y^X)_\bot$ singled out by "not $\varnothing$" corresponds to those $Z'$ with $Z'\times X\ne\varnothing$. – მამუკა ჯიბლაძე Dec 7 '19 at 20:59

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.
• $\neg \neg (p \vee \neg p)$ is an intuitionistic tautology, I think – jkabrg Dec 8 '19 at 19:59
• Assume $\neg (p \vee \neg p)$. We conclude both $p$ and $\neg p$, which is a contradiction. So it's a tautology – jkabrg Dec 8 '19 at 20:06
• ¬¬LEM is the statement that $\neg \neg \forall x:\Omega.x \lor \neg x$, and is considerably stronger than the tautology $\forall x:\Omega.\neg \neg (x \lor \neg x)$. In particular, if $\phi$ is provable classically, then ¬¬LEM implies $\neg \neg \phi$. – Jem Dec 8 '19 at 20:11