- #1

Hurkyl

Staff Emeritus

Science Advisor

Gold Member

- 14,916

- 19

## Main Question or Discussion Point

Suppose I have some arbitrary category C.

I would like to construct a cartesian category C' with C embedded in it. If at all possible, the embedding would be full, and C' would be universal amongst all such constructions.

What would be a good way to go about doing that? Can I even do that in general?

Once I've found C', I would like to construct a cartesian closed category C'', again with there being a full embedding of C into C'', and universal amongst all such constructions.

Once I have that, I what I really want is some topos E in which C is embedded, preferably fully. It would be nice, too, if E was universal amongst all such topoi, or at least being minimal amongst extensions.

Actually, the first category I want to do this with is already cartesian, and has a subobject classifier. (It would be cool if it was still the subobject classifier when extended to a topos) But I'm still curious about the more general case too!

I would like to construct a cartesian category C' with C embedded in it. If at all possible, the embedding would be full, and C' would be universal amongst all such constructions.

What would be a good way to go about doing that? Can I even do that in general?

Once I've found C', I would like to construct a cartesian closed category C'', again with there being a full embedding of C into C'', and universal amongst all such constructions.

Once I have that, I what I really want is some topos E in which C is embedded, preferably fully. It would be nice, too, if E was universal amongst all such topoi, or at least being minimal amongst extensions.

Actually, the first category I want to do this with is already cartesian, and has a subobject classifier. (It would be cool if it was still the subobject classifier when extended to a topos) But I'm still curious about the more general case too!