Vaughan Pratt wrote:
JeanBenabou wrote:
(i) Your "guess" about cartesian closed categories is most certainly correct. I knew that Eilenberg/Kelly had explicitly used this name in their La Jolla paper, and it is probably the first instance, because "closed", in this sense, was first introduced in that paper, as far as I know..
What most impressed my students and me two decades ago, when we were applying the concepts of EK65 to modeling concurrency, was their attempt to define "closed" as a self-contained notion independently of any tensor product as its left adjoint (or so it seemed to us). This defeated us. Has a clearer story of that attempt, or any related story, emerged in the meantime?
Meanwhile the following examples occurred to me: 1. Implicational logic without conjunction. 2. The type structure of the pure lambda calculus without products. 3. The subcategory of FinSet consisting of the prime powers. (With regard to 3, Mike Barr mentioned to me that (Eilenberg and?) Kelly had come up with the category "-6" meaning the category of all sets save those with six elements, but this seems less natural than the prime powers, important in ideal theory as we saw in the recent discussion about the division lattice.) The free closed category would be a good example if it had ever been sighted in nature? Has it? (Just because we see initial ring every day in the wild doesn't mean that all free objects arise in nature.) Vaughan