Can anyone give me a good reason for taking ! literally as a comonad when defining the notion of "model of linear logic"? The problem I have with it is that it seems to force either the co-Kleisli or co-Eilenberg-Moore category on you. I have two objections to this. First, correct me if I'm wrong but I was under the impression that co-Eilenberg-Moore categories were hard to determine. Second, again correct me if I've misunderstood this, but if you have a particular adjunction in mind and F is not comonadic, then when you plug FU into the definition it won't give your F and U back. Instead it will go into convulsions trying to find some comonadic adjunction that you didn't want in the first place. The alternative I have in mind is that the notion of model should be defined so as to permit you to specify an adjunction F -| U such that ! = FU. This allows you to use whatever nice adjunction you had in mind in place of the canonical one determined by FU. One might require that U be monadic, but I don't see any compelling reason to require this. I've been doing just this for the past couple of years, but it occurs to me that the notion of "model of linear logic" might need to be standardized at some point, in which case it would be a pity if it got this detail wrong. Vaughan Pratt ==============================================================================