Equality as an adjunction

Equality as an adjunction

[David Leduc]

In "Categorical Logic", Pitts explains that equality can be defined as
an adjunction. See Fig. 8, page 55
(http://www.cl.cam.ac.uk/~amp12/papers/catl/catl.ps.gz)

He writes the definition as a bidirectional typing rule for the
internal language of a suitable category.

       Phi |- P(x,x)   [x:A]
===================
Phi, x=x' |- P(x,x')   [x x':A]

What are the left and right adjoint functors here?


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

Re: Equality as an adjunction

[Robert Seely]

David - you might like to look at Lawvere's paper "Equality in
hyperdoctrines and the comprehension schema as an adjunct functor" or
"Adjointness in foundations" (the latter being a TAC reprint, and so
easy to find).  My thesis also explored this in detail
("Hyperdoctrines, natural deduction, and the Beck condition", on my
webpage, url given below).

-= rags =-

On Thu, 2 Sep 2010, David Leduc wrote:

> In "Categorical Logic", Pitts explains that equality can be defined as
> an adjunction. See Fig. 8, page 55
> (http://www.cl.cam.ac.uk/~amp12/papers/catl/catl.ps.gz)
>
> He writes the definition as a bidirectional typing rule for the
> internal language of a suitable category.
>
>       Phi |- P(x,x)   [x:A]
> ===================
> Phi, x=x' |- P(x,x')   [x x':A]
>
> What are the left and right adjoint functors here?
>
>

-- 
<rags@math.mcgill.ca>
<www.math.mcgill.ca/rags>


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

Re: Equality as an adjunction

[Michael Shulman]

Hi David

The two categories involved are Pred([A]) and Pred([A A]), the
categories (perhaps preorders) of predicates over the contexts A and A
A in the contextual category of the logic (or in some semantic
interpretation of it).  The diagonal morphism [A] --> [A A] induces a
pullback functor \Delta^*: Pred([A A]) --> Pred([A]) which interprets
a predicate P(x,x') as a predicate with only one variable of type A by
duplication: P(x,x).  Its left adjoint \Delta_! interprets a predicate
of one variable as a predicate of two variables which is only true
when the two variables are equal, i.e. it adds x=x' to the predicate.
I believe this adjunction was first noticed by Lawvere in "Equalities
in hyperdoctrines and comprehension schema as an adjoint functor."

Mike

On Wed, Sep 1, 2010 at 6:40 PM, David Leduc <david.leduc6@googlemail.com> wrote:
> In "Categorical Logic", Pitts explains that equality can be defined as
> an adjunction. See Fig. 8, page 55
> (http://www.cl.cam.ac.uk/~amp12/papers/catl/catl.ps.gz)
>
> He writes the definition as a bidirectional typing rule for the
> internal language of a suitable category.
>
>       Phi |- P(x,x)   [x:A]
> ===================
> Phi, x=x' |- P(x,x')   [x x':A]
>
> What are the left and right adjoint functors here?
>


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

Re: Equality as an adjunction

[Andrej Bauer]

On Thu, Sep 2, 2010 at 3:40 AM, David Leduc <david.leduc6@googlemail.com> wrote:
> He writes the definition as a bidirectional typing rule for the
> internal language of a suitable category.
>
>       Phi |- P(x,x)   [x:A]
> ===================
> Phi, x=x' |- P(x,x')   [x x':A]
>
> What are the left and right adjoint functors here?

Short answer: the right adjoint is contraction, the left adjoint is
(making conjunction with) equality.

Long answer:

To make things easier to understand, let me interpret types as sets,
predicates as subsets and entailment |- a the subset relation. For a
set X let Sub(X) be the powerset of X ordered by subset inclusion. Fix
a set A and define functors (monotone maps between posets)

G : Sub(A x A) --> Sub(A)

F : Sub(A) --> Sub(A x A)

by

G(P) = {x \in A | P(x,x)}

F(Q) = {(x,y) \in A x A | Q(x) and x = y}

Thus G is composition with the diagonal map (a.k.a. contraction in
logic) and F is intersection with the diagonal (equality relation).
These two functors are adjoint, since for any P in Sub(A x A) and Q in
Sub(A) we have

Q \susbeteq G(P) <==> F(Q) \susbeteq P

If we write this in logical form and plug in definitions of F and G we get:

Q(x) |- P(x,x)  [x : A]
==================================
Q(x), x=x' |- P(x,x') [x,x' : A]

which is more or less what you wrote.

With kind regards,
Andrej


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

Re: Equality as an adjunction

[Vaughan Pratt]

On 9/1/2010 6:40 PM, David Leduc wrote:
> In "Categorical Logic", Pitts explains that equality can be defined as
> an adjunction. See Fig. 8, page 55
> (http://www.cl.cam.ac.uk/~amp12/papers/catl/catl.ps.gz)
>
> He writes the definition as a bidirectional typing rule for the
> internal language of a suitable category.
>
>         Phi |- P(x,x)   [x:A]
> ===================
> Phi, x=x' |- P(x,x')   [x x':A]
>
> What are the left and right adjoint functors here?

There's a certain tension between logic and algebra here.  The
algebraist's response to a question of this nature should be, adjunction
is third-order equality, where isomorphism is second-order and
commutative diagrams are first-order.

The adjunction case is best understood 3-categorically, representable
quite easily with origami.  I can't find the origami I constructed to
demonstrate this, I should build it again and post a photo of it at some
point.

Using adjunctions to explain equality is fine, just as using a hammer
two sizes too large to crack a peanut works fine when wielded gently, as
Andy has done here.

Vaughan


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

Re: Equality as an adjunction

[David Leduc]

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/ ]

Re: Equality as an adjunction

[David Leduc]

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/ ]

Re: Equality as an adjunction

[David Leduc]

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/ ]