Re: Equality as an adjunction

[David Leduc <david.leduc6@googlemail.com>]

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?

I wrote:
> Thank you all for your replies. If I understood you well, the
> adjunction is as follows:
>
>  [C,2](P o Delta, Q) =~ [CxC,2](P, Ran_Delta Q)
>
> where Ran_Delta Q is the right Kan extension if Q along Delta.
> (I write [C,D] for the functor category, and 2 for the category with
> only two objects True and False and identities). If T is the constant
> functor that sends every object to True, then Ran_Delta T : CxC -> 2
> is the equality predicate, right?
>
> Now I write this adjunction in logical form:
>
>    P(x,x) |- Q(x)
> ==============
> P(x,y) |- Q(x) /\ x=y
>
> But in Pitts it was reversed:
>
>   Q(x) |- P(x,x)
> ==============
> Q(x) /\ x=y |- P(x,y)
>
> Where is my mistake?
>


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