Adding the DNE to CCCs collapses them into Boolean algebras: Suppose $\mathcal{C}$ is a Cartesian closed category. We can show that if $\mathcal{C}$ has a family of isomorphisms between $A$ and $(A \to 0) \to 0$, then $\mathcal{C}$ is a poset (and a Boolean algebra).
Proposition. For any object $A$ of $\mathcal{C}$, $A \times 0 \simeq 0$.
Proof. ${\mathit{\mathop{Hom}}}(A \times 0, B) \simeq {\mathit{\mathop{Hom}}}(0 \times A, B) \simeq {\mathit{\mathop{Hom}}}(0, B^A) \simeq 1$. Therefore, $A \times 0$ is an initial object in $\mathcal{C}$. Clearly $(\pi_2, \bot_{A \times 0})$ establishes the isomorphism.
Qed
Proposition. Given a morphism $f : A \to 0$, we can conclude that $A \simeq 0$.
Proof. The isomorphism is witnessed by $(f, \bot_A) : A \to A \times 0 \simeq 0$ (where $\bot_A : 0 \to A$ is the unique initial morphism).
Qed
We have seen that given the morphism $f : A \to 0$ we can construct an iso $A \simeq 0$. In particular, that means that there can be at most one arrow between $A$ and $0$; interpreting arrows as "proofs" or "proof object", that means that in the intuitionistic calculus there is at most one proof/realizer of the negation (up to isomorphism).
Now, returning to the original question, how do CCCs with double-negation elimination look like? Specifically, we want to show that if in $\mathcal{C}$ there is an isomorphism between $A$ and $0^{(0^A)}$ for all objects $A$, then the categorical structure collapses into a Boolean algebra.
We say that a category has double negation elimination if for every $A$, it is the case that $A \simeq 0^{(0^A)}$.
Proposition. Given a category with double negation elimination and two morphisms $f, g : A \to B$, it is the case that $f = g$.
Proof. Let $i$ be the isomorphism between $B$ and $0^{(0^B)}$. Then, $i \circ f, i \circ g \in {\mathit{\mathop{Hom}}}(A, 0^{(0^B)}) \simeq {\mathit{\mathop{Hom}}}(A \times (0^B), 0)$. But the latter set can contain at most one element; thus, $i \circ f = i \circ g$. Because $i$ is an isomorphism, $f = g$.
Qed
It might be worth noting that in "standard" cartesian closed categories, a morphism $i : B \to 0^{(0^B)}$ serve as a coequalizer of $f$ and $g$. Perhaps stretching the analogy a bit, we can view $i$ as "equalizes" two constructive proofs of $B$ into a single classical proof.
See also
- A categorical characterization of Boolean algebras by M.E. Szabo
