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

From: HASEGAWA Masahito <[email-masked]>
Date: Tue, 15 Sep 1998 13:42:59 +0900

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: [email-masked]
URL:  http://www.kurims.kyoto-u.ac.jp/~hassei