Does this “mixable” property have a standard name in constructive mathematics?

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?

• So... mixable is sort of like the opposite of a system of representatives for the equality relation? – Asaf Karagila Mar 28 at 20:38
• (Or, again, if we talk about forcing, then $X$ is a rather canonical name, and for every name $S$ for a subset of $X$ and every two names which are forcing into $S$, there is some name which is already forced into $X$ which is equal to them. So sort of the construtivist version of the mixing lemma?) – Asaf Karagila Mar 28 at 20:40
• (To add on my second comment, let me point out that the mixing lemma is equivalent to AC over ZF.) – Asaf Karagila Mar 28 at 20:41
• I guess you mean that classically it is trivial that every nonempty set is mixable. – Todd Trimble Mar 28 at 21:31
• The argument in your edit is precisely what I had in mind, sorry for not spelling it out on the nLab page. By the way, most applications of Zorn in mathematical practice require a touchup by LEM, that is, they go like this: "By Zorn's lemma, there is a maximal element. Assume that it does not have the desired property. Then by <some-argument>, we can extend it to a larger element. This contradicts maximality." But here no LEM is necessary. This is relevant because if your metatheory satisfies Zorn, then so will any localic topos, while LEM is just false in most localic toposes. – Ingo Blechschmidt Mar 29 at 13:30