There are several questions here on MO about the Cantor-Bernstein-Schröder ((C)BS) theorem, but I could not find answers to what arose to me recently.

Although I don't think I need to recall it here, the theorem states that if there are embeddings $i:A\hookrightarrow B$, $j:B\hookrightarrow A$ then there is a bijection between $A$ and $B$.

First question -

As explained in several answers to one of those questions, CBS is not constructively valid. Does validity of CBS actually imply excluded middle? If not - does CBS imply any nontrivial (say, not intuitionistically valid) **propositional** sentence?

Some motivation comes from [Diaconescu's theorem](https://en.wikipedia.org/wiki/Diaconescu%27s_theorem) that the Axiom of Choice implies excluded middle. Again, as mentioned in several of the answers to the above questions validity of CBS does not require choice, but this does not exclude the possibility that, say, the propositional part of some form of constructive set theory + CBS is strictly stronger than "mere" intuitionism. Btw, the Wikipedia article that I linked to for Diaconescu's theorem mentions that it is in a form of a Problem (Problem 2 on page 58) in Bishop's "Foundations of constructive analysis". What is said there literally is "Construct a surjection which is *not* onto", and the whole set of problems has an instruction saying that the *not* has to be understood in the sense of discussion at the end of Section 2. What is said in that discussion seems to indicate that one has to work in intuitionistic logic although I am *not* sure.

I mention all this to illustrate that there might be some subtle points involved. Anyway, here is my

Second question -

Is there a constructively valid statement that becomes equivalent to CBS under excluded middle?

Again, it might be not obvious what is precise sense of this, but let me give another piece of motivation. One might replace $B$ with $j(B)\subseteq A$, then CBS becomes equivalent to the following:

> 
> Given an injective self-map $e:A\hookrightarrow A$, for any $e(A)\subseteq A'\subseteq A$ there is a bijection between $A$ and $A'$.
> 
> 
> 

Now recall that Lawvere's notion of the object of natural numbers (NNO) can be equivalently given as the initial algebra for the functor $A^+:=A\sqcup 1$. That is, the NNO is characterized up to isomorphism as an object $N$ equipped with a map $N^+\to N$ and initial among objects with such structure. By Lambek's lemma it then follows that this $N^+\to N$ is an isomorphism. It can be also shown that **if $A^+\to A$ is mono then the induced map $N\to A$ is mono too**.

In view of this and of the above reformulation of CBS it is natural to ask what happens if one replaces 1 with some other object $T$. Similarly to the above statement in bold, if there is a mono $A\sqcup T\rightarrowtail A$ then $A$ will contain a copy of the initial $\\_\sqcup T$-algebra, in particular, a subobject $I\rightarrowtail A$ with $I\sqcup T$ isomorphic to $I$.

The latter somehow suggests a form of the above equivalent of CBS with *complemented* "remainder". Still the formulation escapes me although I have very strong feeling there must be something precise behind it.
 And although at the first glance this looks like an uninspiring weakening, the example of the NNO shows it might be interesting: $0:1\to N$ is a complemented element more or less by definition, but this does not make the notion of NNO too weak.

I realize all this does not add much clarity to the second question, but then if it would be clear to me I would not need to ask :D

**Slightly later**

Inspired by the mentions of decidability in Andrej Bauer's answer, here is a sketch of one candidate: I find it quite plausible that constructively $A\sqcup A\_1\sqcup A\_2\cong A$ implies $A\sqcup A\_1\cong A$. Is it so? In case it is, can one do better? That is, is there a still constructively valid statement obviously implying the above but not obviously equivalent to it? Somehow I feel there must also be a "less complemented" version...

...and later - Ingo Blechschmidt commented with a link to an n-category café entry which in turn had a link to ["Theme and variations: Schroeder-Bernstein"](https://sbseminar.wordpress.com/2007/10/30/theme-and-variations-schroeder-bernstein/) at the Secret Blogging Seminar; seems to be related, although I cannot find answers to the above questions there.