Is there some genuinely categorical account of the notion of WELL POWERED CATEGORY that would rid this topic of what I have taken to calling "hocus pocus" foundations? That is, I do not want to be told that a well powered category has a "set" of isomorphism classes of subobjects of each object. (I have just done a web search for this phrase but, despite the occurrence of several names for which I have a lot of respect, I could not find anything along the lines I have in mind.) Suppose we are using some elementary topos E as our usual mathematical workbench, so objects of E are called "sets". We can set up the notions of poset, dcpo, lattice, complete lattice and whatever in E in the usual way. To talk about some category C being "well powered", I want: - I don't care about "collecting" all the objects of C, so it doesn't need to be an internal category in E. - I would like the homs of C to be objects of E, so it is an E-enriched category. - Each object of C has a "set" (E-object) of isomorphism classes of monos into it, and - C might as well have pullbacks of monos (inverse images), so this is a contravariant functor Sub : C^op ------> Poset_E - Now I want to so some ordinary categorical constructions in C using diagrams, with such things as pullbacks, colimits of diagrams indexed by E-objects, maybe function types. - Suppose that all of the objects that occur in my construction have monos into a handful of particular C-objects X_1, ..., X_k - Then I want to INTERNALISE the construction using endofunctions of Sub (X_1 x ... x X_k) or something like that. - I use some logic and constructions in the elementary topos E to do something or other with this internalisation. - Then I want to EXTERNALISE this to give some diagrammatic construction in the category. - A particular application of this would be to PARTIAL MAPS, so maybe some of the work of Pino Rosolini, Robin Cockett and others might form part of this theory. For example, let C just be the topos E. We know how to internalise ("classify") subobjects - using the subobject classifier Omega. Simple constructions like intersection and union of subobjects in E can be internalised as the meet and join on Omega. So we can show that it is a Heyting algebra. Doing this is an exercise that many of us will have done as graduate students. It's straightforward, once you get the idea, but a bit tedious after a while. So what I'm looking for is the universal property that says how to internalise and externalise, ie translate between categorical diagram constructions in the category C and endofunctions of the Sub(X) objects in E. I will write about the subject for which I need this in another posting. Any ideas? Paul Taylor. [For admin and other information see: http://www.mta.ca/~cat-dist/ ]