Equality as an adjunction
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/ ]
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/ ]
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/ ]
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/ ]
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/ ]
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/ ]
participants (5)
-
Andrej Bauer -
David Leduc -
Michael Shulman -
Robert Seely -
Vaughan Pratt