How about Span? Steve Lack.
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