Re: Equality as an adjunction

[Michael Shulman <shulman@math.uchicago.edu>]

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