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