Barr's symmetric monoidal closed comma category
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
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
participants (2)
-
HASEGAWA Masahito -
Paul Taylor