While thinking about constructive mathematics, I stumbled on the following notion, and I would like to know if it has a standard name, a simpler equivalent, or has appeared in the literature:
Say that a set $X$ is mixable (temporary term, for lack of a better one) when it satisfies the following property:
$$\forall S\subseteq X.(\forall u\in S.\forall v\in S.(u=v) \Rightarrow \exists x\in X.\forall y\in S.(y=x))$$
In other words, every subset $S$ of $X$ all of whose elements are equal is a subset of the singleton $\{x\}$ for a certain $x\in X$.
Classically, it is trivial that every (edit:) nonempty set is mixable.
Example: Every power set object $\mathscr{P}(Z)$ is mixable. (Indeed, given $S \subseteq \mathscr{P}(Z)$ as assumed, consider $x := \bigcup_{t\in S} t$, that is, $\{z\in Z : \exists t\in S.(z\in t)\}$. Given $y\in S$, since we have $S = \{y\}$, we have $x = \bigcup\{y\} = y$, as announced.) For the same reason, in CZF, we have: $\forall S.(\forall u\in S.\forall v\in S.(u=v) \Rightarrow \exists x.\forall y\in S.(y=x))$.
Counterexample: If $\{0,1\}$ is mixable then the Weak Law of Excluded Middle holds. (Indeed, given $p$ a truth value, consider $S := \{0 : p\} \cup \{1 : \neg p\}$. Clearly all elements of $S$ are equal. But if there is $x\in\{0,1\}$ such that $S \subseteq \{x\}$ then either $x=0$ or $x=1$, and in the first case $\neg\neg p$ while in the second $\neg p$ holds, so on the whole, $\neg p \lor \neg\neg p$.)
In sheaf semantics, saying that a sheaf $X$ on a topological space $E$ is mixable means that (†) for every section $s$ of $X$ on an open set $U$ of $E$, there is a covering of $E$ by open sets $V_i$ such that $X$ has a section $x_i$ on each $V_i$ which coincides with $s$ on $V_i \cap U$. This is the case in particular if $X$ is flabby, but I don't know if this property has a name in the sheaf context.
Edit (2019-03-29): As Mike Shulman points out in his answer, the above property of sheaves is actually equivalent to being flabby, so “flabby” is a good name for the property. Since the proof (by a “typical argument”) is not actually written out on nLab, here it is for the completeness of MathOverflow: assume the sheaf $X$ on $E$ has the property (†) described in the previous paragraph, and let $s$ be a section on $U$. Consider sections of $X$ extending $s$, partially ordered by extension: since chains of sections give rise to a single section on the union by the seaf property, Zorn's lemma implies that there is a maximal extension $s' \in X(U')$ of $s$; now apply (†) to $s'$: for any $i$, the sections $s'$ and $x_i$ glue to give a section of $X$ on $U' \cup V_i$, extending $s$, so by maximality of $s'$ we have $V_i\subseteq U'$, and since this holds for every $i$, in fact $U' = E$. Thus, $X$ is flabby.
Question: Does the above “mixable” property have a standard name or a nicer equivalent, and where might I learn more about it?
