cartesian closed categories with one object

cartesian closed categories with one object

[Paul Taylor]

> how to build a cartesian closed category with one object ?

By the letter of the law, a CCC has finite products, including a terminal
object, which is therefore the only object, and its only morphism is the
identity.

By the spirit of the question, there is such a thing as a CCC with one
interesting object D, and one boring one, the terminal object.

What you want, therefore, is [a full subcategory of] a category with an
object D such that
                                       D
		D x D   =    D    =   D

where of course "=" denotes isomorphism, not equality, and the two maps
that form this isomorphism encode a lot of interesting structure.

This structure is known as "the untyped lambda calculus with surjective
pairing", and Dana Scott famously showed how to construct such objects
in the early 1970s.

Joachim Lambek and *Philip* Scott ("Intro to higher order categorical logic")
have a nice discussion that goes from the question of a two-object CCC to
the lambda calculus.

Any account of domain theory will tell how more ways than the world ever
needed to know of constructing these models.

Paul

cartesian closed categories with one object.

[Moustapha N. PEMY]

Please could somebody tell me how to build a cartesian closed category
with one object ?