well powered categories, categorically?

[Paul Taylor <cats@PaulTaylor.EU>]

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/ ]