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