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