Post History

Can we constructively find a third element of a set $X$ satisfying $X \cong X \times X$ given two distinct elements?

Consider a set $X$ such that $X \cong X\times X$. It's quite easy to prove in a classical set theory, e.g. **ZF**, that $X$ must be the empty set or a singleton set or an infinite set. In other words, if we additionally assume that there exists $a, b \in X$ and $a \neq b$, then we know that $X$ is an infinite set. In particular, we know that there exists an element $c \in X$ such that $c \neq a$ and $c \neq b$.

### Problem

I believe that the (analogue of the) above statement does ***not*** hold in constructive set theories. Specifically, it doesn't hold in the [internal logic of an elementary topos](https://ncatlab.org/nlab/show/higher-order+logic) which is intuitionistic higher-order logic, or in something like the [Calculus of (Inductive) Constructions](https://en.wikipedia.org/wiki/Calculus_of_constructions), the type theory underlying [Coq](https://coq.inria.fr/). I'm pretty confident that it doesn't hold in many other [constructive set theories](https://en.wikipedia.org/wiki/Constructive_set_theory). Type theoretically, the claim is that $$\Pi X : \mathcal U.\Pi a, b : X. (X \cong X \times X) \land \neg (a = b) \to \Sigma c : X.\neg (c = a)\land \neg (c = b)$$ is not provably an inhabited type. I'm *not* claiming that it is *uninhabited*. Classical logic shows that it clearly can be inhabited. My claim is that it would also be consistent (albeit non-classical) to axiomatically assume that it is uninhabited.

I think the easiest way to refute the original statement would be via a countermodel, i.e. an elementary topos, that has an object that doesn't satisfy (the interpretation of) the above. Even nicer would be a (constructive) proof that the above implies the law of the excluded middle, but I don't think that's possible because I believe there are non-classical models that have inhabitants of the above type. I could be wrong though. (I'd be interested in explicit, ideally relatively simple to describe, examples of such non-classical models.) Of course, I could be wrong about the whole claim, so I would certainly also accept an inhabitant of the above type, preferably in a machine-checked system like Agda or Coq.

### Additional Context

Here's the intuition for why I don't think this statement is provable constructively.

First, you *can* constructively prove that there are more than two distinct elements of $X$. Specifically, if $f : X \times X \to X$ is one half of the isomorphism, you can constructively prove that all of $f(a, a)$, $f(a, b)$, $f(b, a)$, and $f(b, b)$ are distinct. I have a machine checked proof of this in [Agda](https://wiki.portal.chalmers.se/agda/pmwiki.php). In fact, I have a machine checked proof that under the above assumptions $X$ is not "finite" for a strong sense of "[finite](https://ncatlab.org/nlab/show/finite+set#Constructivist)", namely is isomorphic to a explicitly finite set aka "Bishop-finite". I'm pretty sure but have not proven in Agda that this is true for "finitely indexed" or "Kuratowski-finite" as well, i.e. there's a surjection from an explicitly finite set onto $X$.

Thus, the problem isn't that we can't find additional elements of $X$ constructively, *but that we have no way of knowing which of those are distinct from $a$ and $b$*. When you attempt to write a term for the above type, it quickly becomes clear that you have too little information, i.e. too few available operations on $X$, to actually show that, say, $f(a, a)$ is distinct from $a$ or $b$. Sure enough, if we *additionally* assume that $X$ has decidable equality, then we can easily provide a witness (and I have an Agda term witnessing this). This means that a counter-example along the lines I described above will need to use an object which does not have decidable equality.

I think one promising place to look for countermodels is (modified) [realizability toposes](https://ncatlab.org/nlab/show/realizability+topos) such as the [effective topos](https://ncatlab.org/nlab/show/effective+topos) or the closely related [modified realizability topos](https://www.brics.dk/RS/96/3/index.html). Power objects, e.g. $\Omega^\mathbb N$ where $\Omega$ is the subobject classifier, may be a good place to look as they readily satisfy the desired assumptions and lack decidable equality in non-classical toposes.