by Hancock on July 11, 2008.
Tagged as: Lunches.
Paul Levy seems to have taken an interest in the category of containers, and in particular in whether or not it is a CCC. (Like [Set,Set], in which it faitfully and fully embeds.)
In his thesis, Pierre Hyvernat proved that (interaction structures, which are essentially) indexed containers provide a model of multiplicative linear logic, which is to say tensor (><), lolly (-o) and bang (!). A while ago, we "back-ported" at least tensor and lolly to the category of (plain 'ole) containers. I'm not 100% sure, but I think we backported the bang. (The details are in the containers blog, which seems to be defunct.) It would follow that if we define the exponential of containers so that (A -> B) = (!A)-oB, we’d get what ought to be the exponential. Some slightly inebriated investigations last night persuaded me that it could well work out. The question arises of relating this construction to Paul L’s one — it looks prima facie
a bit different. Paul’s centres round partial functions. Mine centres round bags.
The discussion was mostly about the details of the bang construction, eg. the right way to deal with multisets constructively. (Pierre used finitely indexed families modulo permutations of the index set.) Thorsten had a vague memory that decidability of equality was needed somewhere. Indeed, this rings some kind of bell. The moral was that one should try to stay out of the pub long enough to nail this stuff down.