Re: Barr's symmetric monoidal closed comma category

Re: Barr's symmetric monoidal closed comma category

[HASEGAWA Masahito]

Related to Mike and Paul's messages to categories, I had the
following observation in my recent draft paper 
(http://www.kurims.kyoto-u.ac.jp/~hassei/papers/basic.ps.gz
 "Logical predicates for intuitionistic linear logic", Lemma A.1): 

	Suppose that C and D are symmetric monoidal closed
	categories and that G:C->D is a symmetric monoidal
	functor. Moreover suppose that D has pullbacks.
	Then the comma category (D,G) can be given a symmetric
	monoidal closed structure, so that the obvious projection
	(D,G)->C is strict symmetric monoidal closed.  

I used this (together with the free symmetric monoidal cocompletion) 
for deriving "logical predicates (logical relations)" for
intuitionistic linear type theories, thus in a similar way as Lafont's 
use of glueing for typed lambda calculi and ccc. In this paper I also
have another lemma for glueing symmetric monoidal adjunctions, for
interpreting the modality !.

I have been wondering if this is a sort of folklore, but never found a 
reference. 

Best Regards,

Masahito.


Masahito Hasegawa
Research Institute for Mathematical Sciences
Kyoto University
Kyoto 606-8502 Japan
MAIL: hassei@kurims.kyoto-u.ac.jp
URL:  http://www.kurims.kyoto-u.ac.jp/~hassei

Barr's symmetric monoidal closed comma category

[Paul Taylor]

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