Turnstile (\vdash) in adjoint functor and type theory.

246 Views Asked by At

Is common symbol $\vdash$ an abuse of notation or there is a deep sacred connection between $$\Gamma \vdash \lambda(a:A).a:\Pi(a:A).A$$ which is preorder and $$G \vdash F \quad \mbox{($F$ is left adjoint to $G$)}$$ ?

(the source of misunderstanding is adjoined functor wiki)

=========Edited=========

I found some useful here in Categorical Logic and Type Theory B.Jacobs (1999).

But I didn't understand about which categories author wrote.

1

There are 1 best solutions below

0
On

The adjoint functor is not the normal turnstile, but the reverse turnstile ⊣

There is quite a strong relation between the adjoint functor and semantics, see "The Galois connection between syntax and semantics"

http://www.logicmatters.net/resources/pdfs/Galois.pdf

but that would make one expect the double turnstile to be used... It would be interesting to know if there is anything more to the use of this symbol.