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