Re: Equality as an adjunction

[Robert Seely <rags@math.mcgill.ca>]

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