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