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?
(iii) I agree with you on the idea that the "natural" definition of locally cartesian closed category should not imply the existence of a terminal object. If I asked the question, it is because in Johnstone's "Elephant" he does assume a terminal object. Has such an assumption become, now, commonly accepted in the definition ?
Hopefully not. If affine geometry has no origin, why should locally cartesian closed categories have a global reference point? (What would Andy Pitts have decided there, and for that matter the orientation of profunctors in B2.7, which seems backwards from say Borceux?) Vaughan