If you accept that toposes are models of constructive set theory, then another way to answer the question is to give a (non-Boolean) topos where the CBS theorem fails; that would show that this theorem can't possibly have a constructive proof.

A simple example of such a topos is the arrow category $Set^\to$, whose objects are functions $X_0 \to X_1$ between sets and whose morphisms are commutative squares. Let $X$ be the object $f: \mathbb{N} \to \mathbb{N}$ that takes $n \in \mathbb{N}$ to $\mathrm{int}(n/2)$, where $\mathrm{int}(x)$ is the greatest integer less than or equal to $x$; let $Y$ be the object $g: \mathbb{N} \to \mathbb{N}$ that takes $n$ to $\mathrm{Int}((n+1)/2)$, where $\mathrm{Int}(x)$ is the least integer greater than or equal to $x$. It is pretty clear that $X$ and $Y$ are non-isomorphic, because $g^{-1}(0)$ has cardinality $1$ where all fibers of $f$ have cardinality $2$. But, just by drawing pictures of these objects, it is easy to construct monomophisms $i: X \to Y$ and $j: Y \to X$ (e.g., define $i_0(n) = n+1$ and $i_1(n) = n+1$ for all $n$, and define $j_0(n) = n+1$ for $n \gt 0$, $j_0(0) = 0$, and $j_1(n) = n$ for all $n$).

For people who are not used to thinking of topos theory as "constructive set theory", there is another way of considering the example above in terms of "$H$-valued sets", where $H$ is the Heyting algebra with three elements, $H = \{0 < 1/2 < 1\}$. The law of the excluded middle does not hold; one can easily calculate $\neg \neg (1/2) = 1$.

An *$H$-valued set* is a set $X$ together with a function $e_X: X \times X \to H$ which measures the extent to which elements of $X$ are considered "equal", subject to transitivity and symmetry axioms:

$$e_X(x, y) \wedge e_X(y, z) \leq e_X(x, z), \qquad e_X(x, y) = e_X(y, x).$$

We can think of $e_X(x, x)$ as measuring the extent to which $x$ "exists". An *$H$-valued relation* is a function $r: X \times Y \to H$ such that

$$e_X(x', x) \wedge r(x, y) \leq r(x', y), \qquad r(x, y) \wedge e_Y(y, y') \leq r(x, y'), \qquad r(x, y) \leq e_X(x, x) \wedge e_Y(y, y).$$

An *$H$-valued function* $f: X \to Y$ is an $H$-valued relation such that

$$f(x, y) \wedge f(x, y') \leq e_Y(y, y'), \qquad e_X(x, x) \leq \bigvee_{y \in Y} f(x, y)$$

where the first condition is an analogue of well-definedness and the second roughly says that $f(x)$ is defined to the extent $x$ exists. It turns out that the category of $H$-valued sets is equivalent to the topos $Set^\to$.

Under this equivalence, $X$ in the example above is identified with the pair $(\mathbb{N}, e_X: \mathbb{N} \times \mathbb{N} \to H)$ where $e_X(n, n) = 1$, where $e_X(m, n) = 1/2$ if $m \neq n$ but $f(m) = f(n)$, and otherwise $e_X(m, n) = 0$. There is a similar description of $Y$ in terms of $H$-valued sets. For such $H$-valued sets where $e_X(x, x') = 1$ for all precisely when $x = x'$, functional $H$-relations between them can be described as actual functions $f: X \to Y$ subject to the condition $e_X(x, x') \leq e_Y(f(x), f(x'))$ for all $x, x'$ in $X$.

The monomorphic functional relations $i: (\mathbb{N}, e_X) \to (\mathbb{N}, e_Y)$ and $j: (\mathbb{N}, e_Y) \to (\mathbb{N}, e_X)$ turn out to be given by $i(n) = n+1$ and $j(0) = 0$, $j(n) = n+1$ for $n > 0$ (i.e., the functions $i_0$ and $j_0$ in the example above). The monomorphicity amounts to the condition that $e_Y(i(x), i(x')) = e_X(x, x')$ for all $x, x'$ in $X$ (and similarly for $j$). This is easily checked.

Now one can try to run through the König proof to see what goes kaflooey. Following the Wikipedia description, every element of the disjoint union $X \sqcup Y$ unambiguously belongs to an "$X$-stopper" or to a "$Y$-stopper":

$$1_X \stackrel{i}{\mapsto} 2_Y \stackrel{j}{\mapsto} 3_X \stackrel{i}{\mapsto} \ldots$$

$$0_Y \stackrel{j}{\mapsto} 0_X \stackrel{i}{\mapsto} 1_Y \stackrel{j}{\mapsto} \ldots$$

But: when one attempts to define an isomorphism $\phi: X \to Y$ out of this by following the prescription, it immediately goes wrong. Look at what this putative function $\phi$ does to the "half-equal" elements $0_X$ and $1_X$. It sends them respectively to the not-at-all-equal elements $0_Y$ and $2_Y$. Thus it fails to respect

$$e_X(0_X, 1_X) \leq e_Y(\phi(0_X), \phi(1_X))$$

as required by law.