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?



Does this "mixable" property have a standard name in constructive mathematics?
According to [this proposition](https://ncatlab.org/nlab/show/flabby+sheaf#characterization_using_the_internal_language), the property in question is (by "a typical argument with Zorn's lemma") equivalent to flabbiness for sheaves on topological spaces. Thus, the term "flabby" is sometimes used more generally inside constructive mathematics for sets with this property.


