From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/4216 Path: news.gmane.org!not-for-mail From: Thorsten Altenkirch Newsgroups: gmane.science.mathematics.categories Subject: Re: A small cartesian closed concrete category Date: Sat, 16 Feb 2008 12:21:01 +0000 Message-ID: NNTP-Posting-Host: main.gmane.org Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit X-Trace: ger.gmane.org 1241019798 12250 80.91.229.2 (29 Apr 2009 15:43:18 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:43:18 +0000 (UTC) To: categories@mta.ca Original-X-From: rrosebru@mta.ca Sat Feb 16 10:19:51 2008 -0400 Return-path: Envelope-to: categories-list@mta.ca Delivery-date: Sat, 16 Feb 2008 10:19:51 -0400 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1JQNhT-0004PF-5l for categories-list@mta.ca; Sat, 16 Feb 2008 10:07:31 -0400 Original-Sender: cat-dist@mta.ca Precedence: bulk X-Keywords: X-UID: 38 Original-Lines: 52 Xref: news.gmane.org gmane.science.mathematics.categories:4216 Archived-At: On 16 Feb 2008, at 00:17, Andrej Bauer wrote: > PETER EASTHOPE wrote: >> Is there a cartesian closed concrete category which >> is small enough to write out explicitly? It would be >> helpful in learning about map objects, exponentiation, >> distributivity and etc. Can such a category be made >> with binary numbers for instance? > > A Heyting algebra, viewed as a category (every poset is a category), > is > a CCC. If you take a small Heyting algebra, e.g. the topology of a > finite topological space, you can write it out explicitly. > > If you would like a CCC made from n-bit binary numbers, here is how > you > can do it: > > The two-point lattice B = {0, 1} is a Boolean algebra with the usual > logical connectives as the operations. Because B is a poset with 0<=1, > it is also a category (with two objects 0, 1 and a morphism between > them). Since every Boolean algebra is a Heyting algebra, B is > cartesian > closed, with the following structure: > - 1 is the terminal object > - the product X x Y is the conjuction X & Y > - the exponential Y^X is the implicatoin X => Y > > The product of n copies of B is the same thing as n-tuples of bits, > i.e., the n-bit numbers. This is again a CCC (with coordinate-wise > structure). > > At this late hour I cannot see what can be said about finite CCC's > which > are not (eqivalent to) posets. Indeed, are there any at all? If you have coproducts you can define the infinite collection of objectss 0,1,2,... and if you identify any of those you get equational inconsistency. A similar construction should also work for CCCs. In the simply typed lambda calculus with one base type o you can iterpret n as o^n -> o and you get equational inconsistency if you identify any two finite types. This carries over to a finite collection of base types, and hence there cannot be a finite CCC which isn't a preorder. I am sure there must be a more elegant proof of this. Cheers, Thorsten