re: query: presheaf construction

re: query: presheaf construction

[Todd H. Trimble]

> How about Span?                                                     
>                                                                    
> Steve Lack.                                                         
> 

Since Ladj(Span) is essentially Set, we would need, for every set b, 
a set pb such that for every a, the large category of spans a -|-> b 
is equivalent to the small discrete category of functions a --> pb. 
This doesn't work. 

[Just to avoid a possible misunderstanding: if B is a bicategory, then 
by Ladj(B) I mean the locally full subbicategory of B with the same 
objects as B and whose 1-cells are left adjoints in B. Katis and Walters 
have a paper which uses the same notation Ladj(B) for something else.] 

-- Todd.  

>> 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.        
>>
               [rest of message snipped]

re: query: presheaf construction

[Steve Lack]

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
 > 

query: presheaf construction

[Todd H. Trimble]

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