Re: A small cartesian closed concrete category

[Thorsten Altenkirch <txa@Cs.Nott.AC.UK>]

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