# Free CCC or topos on a cartesian category

$\def\sC{\mathcal{C}}\def\sD{\mathcal{D}}\def\Set{\mathbf{\mathrm{Set}}}\DeclareMathOperator{\Sub}{Sub}\def\op{\circ}$I have a Cartesian category $\sC$. I would like to embed $\sC$ into a cartesian closed category (or better, a topos) $\sD$. However, $\Set^{\sC^\op}$ is bigger than I want -- in particular, I would like my embedding to preserve subobject lattices: $\Sub_\sC(x) \cong \Sub_\sD(x)$ for each object $x$ of $\sC$. I think I would also like it to preserve whatever limits already exist in $\sC$ and be a full embedding.

If $\sC$ already has a subobject classifier, can I hope for it to still be so in a topos $\sD$?

Is there a standard construction to construct a CCC or a Topos $\sD$ out of a Cartesian category $\sC$? What properties can I expect out of such constructions? Is there any hope that it could satisfy the properties I ask for?

If it matters, I'm particularly interested in the case where $\sC$ is the category of semi-algebraic varieties. That is, the category of definable objects in the first-order theory of real closed fields.

-
No, there can be no such a standard construction --- subobject lattices in any topos are complete Heyting algebras, so you should not expect the equivalences between $\mathit{Sub}_\mathbb{C}(x)$ and $\mathit{Sub}_\mathbb{D}(x)$. –  Michal R. Przybylek Jun 10 '12 at 10:03
BTW, perhaps the right framework to ask your question is to start from the subobject fibration over your category, and ask about adjoining to it some logical connectives. –  Michal R. Przybylek Jun 10 '12 at 10:10
If $\mathcal C$ is a regular category, its ex/reg completion preserves subobject lattices. One way to construct this completion, is to take the least exact subcategory of the category $\mathrm{Sh}(\mathcal C,R)$ of sheaves for the regular topology on $\mathcal C$ that contains all representable (pre)sheaves. I suppose one could look at the least subCCC of $\mathrm{Sh}(\mathcal C,R)$ instead, to solve your problem for regular categories. –  Wouter Stekelenburg Jun 10 '12 at 10:31
A version of Michal's first comment, without mentioning complete Heyting algebras explicitly: The subobject lattices in a topos are distributive; not so in some cartesian categories, for example, the category of vector spaces over your favorite field. –  Andreas Blass Jun 10 '12 at 11:23
For a category being a topos is equivalent to having a higher-order subobject fibration. Therefore, from this point of view, your condition implies that the internal logic of your category is a fragment of higher-order logic. I may guess that this is just too much. –  Michal R. Przybylek Jun 10 '12 at 13:06