query: presheaf construction

["Todd H. Trimble" <trimble@math.luc.edu>]

At the Como meeting last week, I asked various people a question 
which I view as having foundational significance: is there a 
setting in which one can iterate the presheaf construction (as 
free cocompletion) without ever having to use the word "small" 
or worry about size? 

Here is a more precise formulation of what I am after. 
I want an example of a compact closed bicategory B [think: 
bicategory of profunctors] with the following very strong 
property: the inclusion 

             i: Ladj(B) --> B, 

of the bicategory of left adjoints in B, has a right biadjoint p 
such that, calling y: 1 --> pi the unit and e: ip -|-> 1 the counit, 
the isomorphisms which fill in the triangles 
               iy               yp
             i --> ipi        p --> pip
               \    |           \    |    
                 \  | ei          \  | pe
                   \|               \|     
                    i                p 

furnish the unit and counit, respectively, of adjunctions iy --| ei 
in B and pe --| yp in Ladj(B).  (These structures should also be 
compatible with the symmetric monoidal bicategory structures on 
B and Ladj(B).)  By exploiting compact closure, it's easy to see 
that p(b) is equivalent to an exponential (p1)^(b^op) in Ladj(B), 
where b^op denotes the dual of b in the sense of compact closure. 
So the unit y: 1 --> pi takes the yoneda-like form b --> v^(b^op); 
the axioms imply it is the fully faithful unit of a KZ-monad. 

The reactions I got were varied and interesting. As filtered through 
me, here are some (abbreviated) responses: 
 
(1) "No, I don't think there are any examples except the obvious 
     locally posetal ones." 
(2) "The notion looks essentially algebraic, so I see no obstacle 
     in principle to producing examples; it should even be easy for 
     the right (2-categorically minded) people." 
(3) [From experts in domain theory] "Good question! Hmmmmmmmm....."  
(4) "It seems to me there is no reason in the world why examples 
     should not exist, but the techniques developed for dealing 
     with things like modest sets are probably not sufficient for 
     dealing with your question, and may be misleading here." 

The various responses suggest *to me* that the question may be 
quite interesting and quite hard. 

My own sense, based on playing around with the axioms on a purely 
formal level, is that there is probably no inconsistency in the sense 
that any two 2-cells with common source and target are provably equal. 
My only vague idea on producing an example would be to proceed as Church 
and Rosser did in the old days: work purely syntactically, and consider 
the possibility of strong normalization for terms. Perhaps one could 
then show that the term model is not locally posetal. 

Todd