title: Uniquness of the absurdity proofs in Cartesian closed categories
tags: category theory
date: 2015-08-12 00:00
---

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](http://link.springer.com/article/10.1007%2FBF02485724) by M.E. Szabo