John Bourke
noticed recently that the category whose objects are categories with pullbacks and whose morphisms are pullback preserving functors is cartesian closed. Given a pair of categories with pullbacks A and B, the internal hom [A,B] has objects: pullback preserving functors from A to B, and morphisms: cartesian natural transformations. I have posted a short paper on the arxiv proving this fact: http://arxiv.org/abs/0904.2486 It seems like a fairly natural fact but is not to my knowledge in the literature. I am wondering whether anyone was previously aware of this result, and if so whether it might be mentioned somewhere in the literature?
Along with Francois Lamarche and various other people that I don't clearly recall, I did a lot of work on this idea in the early 1990s. I was based on earlier ideas by Pierre Ageron, Gerard Berry, Yves Diers, Jean-Yves Girard, Peter Johnstone, Andre Joyal, Christian Lair, ... Since the motivations came from either domain theory or generalisations of algebraic theories, the functors that were considered also preserved directed joins or filtered colimits, but these are not relevant to the basic cartesian closed structure. One of the best known categories of posets like this is that of "coherence spaces", which were described in Girard's book "Proofs and Types", which Yves Lafont and I translated. Earlier work by Berry had been the beginning of the search for models of the notion of sequentiality in programming languages. That by Diers had been about a generalisation of algebraic theories to cover the case of fields, with unique disjunction. In the categorical setting, I considered functors that preserve pullbacks. However, Andre Joyal, Francois Lamarche and others considered functors that preserve squares that differ from a pullback by an epi. Then there's the question of whether to preserve equalisers and/or cofiltered limits; for such generalisations I introduced the term "wide pullback". Girard's version had a representation of the function-space. I put this in categorical form by showing that there is a factorisation system in which the "epis" are maps with left adjoints and the "monos" are similar to discrete fibrations. This system is closely related to the Street--Walters "comprehensive" fibration. I described a model whose objects are called "quantitative domains" and which involves permutation groupoids. See www.PaulTaylor.EU/stable/ for my stuff on this subject. There has been renewed interest in some of these things, for which you should look out for words like "species", "shape", "container". Paul Taylor