I have been reading up on the Curry-Howard isomorphism. In the last chapter of Conceptual Mathematics, Lawvere and Schanuel say that the logical connectives are completely analogous to the categorical operations x, map object and +. Is this an oblique reference to the Curry-Howard isomorphism?
At the 1963 Model Theory conference in Berkeley, I pointed out that an interlocking system of adjoints occurring in set theory and type theory has also as a very special example the one arising in the logic of parts. In Eilenberg and Kelly's 1965 pioneering paper on closed categories, part of my result was cited and it came to be known as the statement that Heyting algebras are cartesian closed categories. In my papers "Adjointness in Foundations"(submitted December 15th 1967), "Equality in Hyperdoctrines...", and "Diagonal Arguments...", I tried to clarify these and related matters. I became aware at some point that Haskell Curry in one of his books had informally pointed out earlier the possible importance of this as an analogy. In the late 1960s, Bill Howard, a student of Mac Lane, began circulating his results which were finally published in 1980; Howard's paper could be described as containing an oblique reference to the closed category theorems. The term "isomorphism" which has emerged in the literature is rather misleading since the map in question is bijective at best at the level of subjective presentations, rather than at the level of objective algebras. That is to say, a symbolic presentation of a particular Heyting algebra can always be construed in many ways as an image of a presentation of a cartesian closed category, but there is the additional draconian rule of inference which says that any two maps with a given domain and codomain are equal. I tried to give a more accurate description of this situation by referring to "an adjunction" rather than to an isomorphism in my paper "Adjointness in and Among Bi-categories" Logic and Algebra, Lecture Notes in Pure and Applied Mathematics, vol. 180, pp 181-189, edited by A. Ursini and P. Agliano', Marcel Dekker, 1996. Bill Lawvere ************************************************************ F. William Lawvere Mathematics Department, State University of New York 244 Mathematics Building, Buffalo, N.Y. 14260-2900 USA Tel. 716-645-6284 HOMEPAGE: http://www.acsu.buffalo.edu/~wlawvere ************************************************************