Re: Category of categories with pullbacks is cartesian closed

[Paul Taylor <pt09@PaulTaylor.EU>]

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