On Sun, Sep 3, 2017 at 1:19 PM, Baruch Garcia <baruchgarcia@gmail.com> wrote:
Hello,
I was wondering if someone of the categories list could answer this question:
In Godel's/Tarski's theorem and the Halting problem, the use-mention distinction (e.g. Boston is populous, but "Boston" is disyllabic) is essential. Is there an analog to the use-mention distinction in category theory or is the use-mention distinction just its own principle independent of category theory?
There's something like a distinction between use and mention in a symmetric monoidal closed category. Given a morphism f:X -> Y, there's the "name" of the function curry(f):I -> X -o Y, where I is the monoidal unit and -o is the internal hom. The evaluation morphism takes a value g of type X -o Y and a value x of type X and returns uncurry(g)(x). -- Mike Stay - metaweta@gmail.com http://www.cs.auckland.ac.nz/~mike http://reperiendi.wordpress.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]