From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/9327 Path: news.gmane.org!.POSTED!not-for-mail From: Mike Stay Newsgroups: gmane.science.mathematics.categories Subject: Re: The use-mention distinction and category theory Date: Tue, 5 Sep 2017 11:36:45 -0600 Message-ID: References: Reply-To: Mike Stay NNTP-Posting-Host: blaine.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset="UTF-8" X-Trace: blaine.gmane.org 1504709769 5107 195.159.176.226 (6 Sep 2017 14:56:09 GMT) X-Complaints-To: usenet@blaine.gmane.org NNTP-Posting-Date: Wed, 6 Sep 2017 14:56:09 +0000 (UTC) Cc: categories To: Baruch Garcia Original-X-From: majordomo@mlist.mta.ca Wed Sep 06 16:56:00 2017 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtp2.mta.ca ([198.164.44.40]) by blaine.gmane.org with esmtp (Exim 4.84_2) (envelope-from ) id 1dpbjr-00085n-CA for gsmc-categories@m.gmane.org; Wed, 06 Sep 2017 16:55:35 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:58394) by smtp2.mta.ca with esmtp (Exim 4.80) (envelope-from ) id 1dpbkD-0004pU-5Z; Wed, 06 Sep 2017 11:55:57 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1dpbiW-0002Vc-7B for categories-list@mlist.mta.ca; Wed, 06 Sep 2017 11:54:12 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:9327 Archived-At: On Sun, Sep 3, 2017 at 1:19 PM, Baruch Garcia 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/ ]