Subject: categories: Barr's symmetric monoidal closed comma category

From: Paul Taylor <[email-masked]>
Date: Mon, 14 Sep 1998 01:55:11 +0100 (BST)

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