On Thu, Sep 2, 2010 at 3:40 AM, David Leduc <david.leduc6@googlemail.com> wrote:
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?
Short answer: the right adjoint is contraction, the left adjoint is (making conjunction with) equality. Long answer: To make things easier to understand, let me interpret types as sets, predicates as subsets and entailment |- a the subset relation. For a set X let Sub(X) be the powerset of X ordered by subset inclusion. Fix a set A and define functors (monotone maps between posets) G : Sub(A x A) --> Sub(A) F : Sub(A) --> Sub(A x A) by G(P) = {x \in A | P(x,x)} F(Q) = {(x,y) \in A x A | Q(x) and x = y} Thus G is composition with the diagonal map (a.k.a. contraction in logic) and F is intersection with the diagonal (equality relation). These two functors are adjoint, since for any P in Sub(A x A) and Q in Sub(A) we have Q \susbeteq G(P) <==> F(Q) \susbeteq P If we write this in logical form and plug in definitions of F and G we get: Q(x) |- P(x,x) [x : A] ================================== Q(x), x=x' |- P(x,x') [x,x' : A] which is more or less what you wrote. With kind regards, Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]