From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/7044 Path: news.gmane.org!not-for-mail From: Andrej Bauer Newsgroups: gmane.science.mathematics.categories Subject: Re: The boringness of the dual of exponential Date: Thu, 10 Nov 2011 02:11:50 +0100 Message-ID: References: Reply-To: Andrej Bauer NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=UTF-8 X-Trace: dough.gmane.org 1320954771 26967 80.91.229.12 (10 Nov 2011 19:52:51 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Thu, 10 Nov 2011 19:52:51 +0000 (UTC) Cc: categories To: Jocelyn Ireson-Paine Original-X-From: majordomo@mlist.mta.ca Thu Nov 10 20:52:46 2011 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.4]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1ROag1-0003mt-PO for gsmc-categories@m.gmane.org; Thu, 10 Nov 2011 20:52:45 +0100 Original-Received: from mlist.mta.ca ([138.73.1.63]:55004) by smtpx.mta.ca with esmtp (Exim 4.76) (envelope-from ) id 1ROac5-0006zq-D3; Thu, 10 Nov 2011 15:48:41 -0400 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1ROac3-0006hW-JC for categories-list@mlist.mta.ca; Thu, 10 Nov 2011 15:48:39 -0400 Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:7044 Archived-At: >> 1. "forall" goes with "weakening" because it is adjoint to it on the >> right. >> 2. "exists" goes with "weakening" because it is adjoint to it on the left. >> > What's the definition of "weakening"? I've not seen this word used formally. Weakening is the map Sub(A) -> Sub(A x B) which takes a subobject M >-> A to the subobject M x B >-> A x B, i.e., it is pullback along the projection pi1 : A x B -> A. The existential quantifier over B is the left adjoint to weakening, where Sub(A) and Sub(A x B) are viewed as posetal categories. The universal quantifier is the right adjoint. Working out the details in Set is instructive. As far as I know the terminology comes from logic. The rule of weakening says that a logical derivation may be "wakened" with an additional (but unneeded) hypothesis: Gamma |- A ---------------------- Gamma, H |- A With kind regards, Andrej [For admin and other information see: http://www.mta.ca/~cat-dist/ ]