Error in the proof of $\textit{Sheaves in Geometry and Logic}$ Lemma VI.3.8 - Cohen Poset satisfies Countable Chain Condition Context
Chapter VI sections 1-3 in Sheaves deals with proving that there is a certain Grothendieck topos $Sh_{\neg \neg}(\mathbb{P})$ in which the continuum hypothesis is false in the internal logic.
Section 3 deals with "the preservation of cardinal inequalities". There is a canonical inclusion functor $\hat{-} : Set \to Sh_{\neg \neg}(\mathbb{P})$ which preserves monomorphisms. The preservation of cardinal inequalities states that if there is no surjection $A \to B$ (where $A$ and $B$ are infinite), then $\ulcorner$there is no epimorphism $\hat{A} \to \hat{B} \urcorner$ holds in the internal logic of the topos. Combining this with the fact that the $\hat{}$ functor preserves monomorphisms, we get that if $|A| < |B|$ is a strict cardinal inequality in the category of sets, then the strict inequality $|\hat{A}| < |\hat{B}|$ holds in the internal logic of the topos. In order to prove this, we must prove that the "countable chain condition" holds for $\mathbb{P}$.
Note that this argument contains the same mathematical content as traditional set-theoretic forcing (but it places forcing within a wider context of Grothendieck toposes and autological toposes in general, which are the sorts of toposes which can give rise to models of IZF).
Mathematical Background
We fix a set $B$.
The "Cohen poset" $\mathbb{P}$ consists of pairs $(F_p, p)$, where $F_p \subseteq B \times \mathbb{N}$ is finite and $p : F_p \to 2$. Here, $2 = \{0, 1\}$. For brevity, we often identify $(F_p, p)$ with $p$. The order is reverse inclusion.
In other words, given $p, q \in \mathbb{P}$, we have $p \leq q$ if and only if both $F_q \subseteq F_p$ and also $q = p|_{F_q}$.
The elements of $\mathbb{P}$ are known as "conditions". Two conditions $f, g \in \mathbb{P}$ are said to be "incompatible" if and only if there is no $h \in \mathbb{P}$ such that $h \leq f$ and $h \leq g$. It's easy to show that $f$ and $g$ are incompatible if and only if there is some $x \in F_f \cap F_g$ such that $f(x) \neq g(x)$.
Problem Statement + Author's Attempt at a Proof
Section 3 lemma 8 states

On the Cohen poset $\mathbb{P}$, any set of incompatible conditions is countable.

In other words, $\mathbb{P}$ satisfies the countable chain condition. This is the critical step in proving that cardinal inequalities in the category of sets are preserved in the category $Sh_{\neg \neg}(\mathbb{P})$.
However, the proof given by Mac Lane and Moerdijk has a major error.

Proof: Let $A$ be a set of incompatible conditions. Write $A_n = \{q \in A \mid |F_q| = n\}$. Then $A = \bigcup\limits_{n \in \mathbb{N}} A_n$. Since the countable union of countable sets is countable, it suffices to show that each $A_n$ is countable.
The base case $n = 0$ is immediate. Now suppose we've shown that any set of mutually incompatible conditions, each of $n - 1$ elements, is countable, and we wish to show $A_n$ is countable, where $n > 0$.
For each $m \in \mathbb{N}$, write $A_{n, m} = \{q \in A_n \mid \exists b \in B, (b, m) \in F_q\}$. Since $n > 0$, we have $A_n = \bigcup\limits_{m \in \mathbb{N}} A_{n, m}$, so it suffices to show that each $A_{n, m}$ is countable.
Pick, for each $q \in A_{n, m}$, some $b_q \in B$ such that $(b_q, m) \in F_q$. Define $A_{n, m, i} = \{q \in A_{n, m} \mid q(b_q, m) = i\}$. Since $A_{n, m} = \bigcup\limits_{i \in \{0, 1\}} A_{n, m, i}$, it suffices to show that each $A_{n, m, i}$ is countable.
Since for any $m$ and $i$, the elements of $A_{n, m, i}$ are pairwise incompatible, so is the set of their restrictions $R_{n, m, i} = \{p|_{F_p \setminus \{(b_p, m)\}} \mid p \in A_{n, m, i}\}$. $R_{n, m, i}$ is a set of countable conditions, each of which has $n - 1$ elements, so $R_{n, m, i}$ is countable by the inductive hypothesis. Therefore, $A_{n, m, i}$ is also countable. $\square$

The Problem with the Proof
The key flaw is that $R_{n, m, i}$ is not necessarily a set of incompatible conditions.
Consider, for example, $F_p = \{(x, 0), (y, 0)\}$ with $p(x, 0) = 0$ and $p(y, 0) = 1$. Consider also $F_q = \{(x, 0), (z, 0)\}$ with $q(x, 0) = 1$ and $q(z, 0) = 0$. We are supposing that $x, y, z$ are pairwise disjoint elements of $B$ here. Note that since $p(x, 0) \neq q(x, 0)$, we see that $p$ and $q$ are incompatible. Let $A = \{p, q\}$, which is a set of incompatible conditions. Then $A_{2, 0} = \{p, q\}$. We pick $b_p = x$ and $b_q = z$. Then $A_{2, 0, 0} = \{p, q\}$. But note that $q|_{F_q \setminus \{(b_q, 0)\}}$ and $p|_{F_p \setminus \{(b_p, 0)\}}$ are distinct, yet compatible (they are compatible since their domains do not overlap). Therefore, $R_{2, 0, 0}$ has two distinct compatible conditions. So the proof is incorrect.
The question now is,
Can the proof be rewritten to work?
 A: Yes, the proof can be rewritten to work.
New proof:

Lemma: for all $n$, if $A \subseteq \mathbb{P}$ is a set of incompatible conditions, and if for all $q \in A$, $|F_q| = n$, then $A$ is countable.

Proof: we proceed by induction on $n$. The base case $n = 0$ is trivial, since there is only one $q \in \mathbb{P}$ such that $|F_q| = 0$.
For the inductive step, we suppose that for all sets $B$ of incompatible conditions, each with $k$ elements, $B$ is countable.
We now consider a set $A$ of incompatible conditions, each with $k + 1$ elements. If $A$ is empty, then we're done. Otherwise, take some $p \in A$, and enumerate $F_p = \{x_0, \ldots, x_k\}$.
For each $j \leq k$, define $S_j = \{q \in A \mid x_j \in F_q$ and $q(x_j) \neq p(x_j)\}$. Then $A = \{p\} \cup \bigcup\limits_{i = 0}^k S_i$, so it suffices to show that each $S_i$ is countable.
Now for each $j \leq k$, define $R_j = \{q|_{F_q \setminus \{x_j\}} \mid q \in S_j\}$. Note that the restriction map $q \mapsto q|_{F_q \setminus \{x_j\}} : S_j \to R_j$ is a bijection, since we can recover $q$ from $q|_{F_q \setminus \{x_j\}}$ because we know that $q(x_j) \neq p(x_j)$, so there's only one possible value for $q(x_j)$. So it suffices to prove that each $R_j$ is countable.
Now given two conditions $r \neq q \in S_j$, we know that $r$ and $q$ are incompatible. Therefore, there is some $w \in F_q \cap F_r$ such that $q(w) \neq r(w)$. But note that $q(x_j) = r(x_j)$, and therefore we have $w \neq x_j$. That is, $w \in (F_q \setminus \{x_j\}) \cap (F_r \setminus \{x_j\})$. Therefore, $w$ witnesses that $q|_{F_q \setminus \{x_j\}}$ and $r|_{F_r \setminus \{x_j\}}$ are incompatible. So $R_j$ is a set of incompatible conditions, each of size $k$. Therefore, $R_j$ is countable by the inductive hypothesis.

Corollary: for all sets $A \subseteq \mathbb{P}$ of incompatible conditions, $A$ is countable.

Proof: $A = \bigcup\limits_{n \in \mathbb{N}} A_n$ where $A_n = \{p \in A \mid |F_p| = n\}$, and each $A_n$ is countable. So $A$ is also countable.
