I've spent the past 1½-2 months picking back up on a part of my research that I first initiated in the last summer and early fall of last year. The idea is vaguely "sets, but where elements only influence substructure rather than determine it". This is perhaps not the best description because these objects don't actually need to have any elements at all (in a certain sense), but it's good enough for a first impression I think.
The idea behind these objects can be motivated by the following set of observations. Suppose that P : Set → Set is the covariant powerset functor, meaning the functor that sends a set to its powerset and sends a function between sets to the induced image map between their powersets. P is an equivalence of categories, which essentially means that for most purposes working with powersets and the image maps between them is essentially the same as working with sets and the functions between them. But this functor can also be interpreted as sending sets and their functions to a certain category where the objects are complete lattices and the morphisms are a slight weakening of the usual morphisms of complete lattices. Alternatively, we can consider the contravariant powerset functor, which again sends sets to their powersets but instead sends functions to the inverse image maps they induce. This again is essentially the same as working in Set (except we have to turn arrows around), and this functor can also be seen as sending us to a category of lattices—only this time, it's the *usual* category of complete lattices.
In both these case, we see that we're able to replace a lot of the significant machinery associated with sets by instead using order theory and algebra: the substructure of a set (i.e. it's subsets) are reinterpreted as an order relation, and the way we can "mix" subsets is described using algebra. Given that categories can be seen as a way of generalizing both these things (as well as giving a concise way of describing the relationship between image and preimage maps), this suggests the "right" setting for these objects is as categories satisfying certain properties formally analogous to properties of powersets. It was for this reason I originally called these objects *formal powersets*, though I don't really like the baggage that comes with that. I'm now calling them *schemas*, if with some hesitation given that this name is very similar to a very well-known class of objects. The motivation behind the name is that we specify a schema not by declaring the points it contains, but instead by prescribing the internal structure is has. That is, we describe a hypothetical set by specifying the overall structure of its abstract powerset (even if no such corresponding set can exist).
I won't give any definition at the moment, in one part because there's a number of definitions involved and, even though I've managed to simplify them a bit by relating them to existing ones, there's still a degree of length to the definitions. The other part, and the bigger one, is that I only have a broad idea of what the right definition is. I know what it should *reduce to* in a certain, simple case, but that only gives hints to the more general definition. As such, I still have much work to do.
