Mike Barr asked whether anyone had been aware that the comma category (F,A) or equivalently (S,U) is symmetric monoidal closed, where A ^ | F| -| |U | V S is a monoidal (tripleable) adjunction over S=Set. As he said, an object (S,s,A) is an arrow s:FS--> A (or, by adjointness, an S-tuple of elements of A) and a map (S,s,A) to (T,t,B) is a pair f: S --> T and g: A --> B making the obvious square commute. He said that the closed structure (S,s,A) --o (T,t,B) is a certain arrow of the form (Hom((S,s,A),(T,t,B),?,B^S). I have certainly seen comma categories like (S,U); they are referred to as gluing, sconing or the Freyd cover. (BTW Peter says that "scone" is a corruption of Sierpinski cone, so its correct pronunciation is presumably "shco:ne".) This construction provides an almost magical proof of strong normalisation, consistency and similar results for various fragments of symbolic or categorical logic. The algebraic theory that I have in mind here for Mike's monadic adjunction is that which describes the fragment of logic in question (the Australians would prefer us to talk about a 2-monad here). An early example of such a proof in the unification of these two traditions was given by Yves Lafont in an appendix to his thesis. He proved that the embedding of a category in the free CCC that it generates is full and faithful. In the course of this he described the exponential in (S,U), which is what Mike's formula gives, though I didn't notice (and apparently nor did Yves) that the A-object which we have is the internal version of Mike's Hom-set. Yves Lafont's result appears as part of a generic account of the gluing construction in Section 7.7 of my forthcoming book. Paul