Justin Pearson asks what is the "correct" definition of Cartesian closed category. I would say that the definition most commonly used is that a category C is a cartesian closed category (ccc) if it has specified terminal object, binary products, and exponentials for each pair of objects. This means that there is a (natural and) precise correspondence between cccs, and equational theories with unit type, binary products and function types. What is potentially confusing is that a Cartesian category is often taken to mean a category with finite limits (binary products and equalisers) because Descartes's work involved equationally defined subsets. For this reason it might be best to call cccs (def. as having finite products and exponentials) by a different name, say exponential categories---but here "best" is clearly of dubious meaning ! Roy Crole.