Do you mean that I am *all* wrong when I spell out the adjunction? Anyway, I will definitely read Lawvere's papers on the topic and maybe your thesis although I am a bit scared by this fibrational setting. On Sat, Sep 4, 2010 at 3:09 PM, Robert Seely <rags@math.mcgill.ca> wrote:

I *really* suggest you look at Lawvere's papers (and I also suggest you might find my elaboration of these ideas helpful).  What is going on here is essentially adjunctions (for sum and product, or equivalently existential and universal quantification) to substitution.  This sort of setup occurs in a fibrational setting, and the functors involved are between fibres;  the underlying common story is more compelling than just one example can suggest, I think.

 - all the best, Robert

On Sat, 4 Sep 2010, David Leduc wrote:

...

Sorry, I guess my mistake is that I've got the adjunction in the wrong direction: it is a left Kan extension:

 [CxC,2](Lan_Delta P, Q) =~ [C,2](P, Q o Delta)

And equality is given by Lan_Delta T : CxC -> 2. Does it always exist?

And what was the right Kan extension in my previous mail when it exists?

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]