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