Working informally, we can take any proof $P$ in constructive (or intuitionistic) logic and turn it into a classical proof $cP$ by 'copying' it, since all the rules of constructive logic reappear in classical logic. For a classical proof $Q$ of $q$, we can form the double negation translation $Q^N$, a constructive proof of $\lnot \lnot q$. Double negation translation followed by copying sends a classical proof to an equivalent classical proof. The other way around, copying followed by double negation, sends a constructive proof $P$ of $p$ to $(cP)^N$, which is syntactically equal to $P^N$, a proof of $\lnot \lnot p$. Since $p \rightarrow \lnot \lnot p$, it seems we have an 'adjunction' $c \dashv -^N$, which means we could classical logic a 'reflective subsomething' of constructive logic.
Can these ideas be formalized? That is, are there categories $\textbf{Clas} \stackrel{\stackrel{}{\leftarrow}}{\hookrightarrow} \textbf{Cons}$ defined in ways reasonably similar to the intuitions above?
One way to formalize the idea is to say the following: the category of classical propositional theories is a reflective subcategory of the category of intuitionistic propositional theories. In order to make sense of that claim, it's best to pass from "theories" to "algebras." Each classical theory corresponds to a Boolean algebra, and each intuitionistic theory corresponds to a Heyting algebra. The category of classical propositional theories is really just the category $\mathbf{BOOL}$ of Boolean algebras; and the category of intuitionistic propositional theories is really just the category $\mathbf{HEYT}$ of Heyting algebras.
[For a theory $T$, let $B_T$ be the Boolean algebra whose elements are equivalence classes of sentences modulo $T$-provable equivalence. Alternatively, we could build a Heyting algebra $H_T$ from $T$ using the same procedure, but using intuitionistic logic for provable equivalence. It's not difficult to see that, in fact, every Boolean algebra is a Lindenbaum-Tarski algebra for some theory. Similarly, every Heyting algebra results from some theory. So we might as well use Boolean and Heyting algebras in the place of theories.]
Obviously there is an inclusion $I:\mathbf{BOOL}\to\mathbf{HEYT}$. The double-negation translation $F:\mathbf{HEYT}\to\mathbf{BOOL}$ is the left adjoint to $I$. For more information, see http://ncatlab.org/nlab/show/Heyting+algebra