Re: Equality as an adjunction

[Andrej Bauer <andrej.bauer@andrej.com>]

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