Functor fibrations and Cartesian closure of general presheaves

Functor fibrations and Cartesian closure of general presheaves

[Henning Basold]

Dear Categorists,

I have three loosely related requests for references for constructions
that I am using in some of my current work.

First, does someone know of a publication, in which it is proved that
for a category I the 2-functor [I, -] : Cat -> Cat given by
post-composition extends to a map on the (large) fibration Fib -> Cat?
Alternatively, I would also be happy to have references for the fact
that [I, p] : [I, E] -> [I, B] is a fibration for a fibration p : E -> B
and a proof that [I, -] preserves strict 2-pullbacks, as these can be
put together to obtain the above result.

Second, I need to construct exponents in general presheaves I^op -> C.
In particular, I am interested in the case where I is the poset ?? of
finite ordinals. I am able to show that [??^op, C] is Cartesian closed,
if C has finite limits and is Cartesian closed. In this case, the
exponent s => t for s, t : ??^op -> C is given as follows. First, for
every natural number n, one defines a functor Sn : N x N^op -> C,
where N is the poset of ordinals less or equal to n, by putting

     Sn(m, k) = t(k)^{s(m)}  and
     Sn(m' <= m, k <= k') = t(k <= k')^{s(m' <= m)},

in which (-)^(-) : C x C^op -> C is the exponent in C. We can then
define the exponent s => t as the end

      (s => d)(n) = \int_{m in N} Sn(m, m),

which exists in C because N is a finite category and C has finite
limits. It takes a bit of effort to check this, but the construction
gives us indeed exponents in [??^op, C].

Did someone see this construction before or is aware of another way to
construct exponents in presheaf categories like [??^op, C]?

Finally, the previous construction can be also applied to the fibres
of the fibration [??^op, p] : [??^op, E] -> [??^op, B], if p : E -> B is
a fibred CCC with fibred finite limits. Thus, one also obtains that
the fibration [??^op, p] is a fibred CCC. Again, the question is,
whether someone has seen something like this before.

Thank you all very much in advance.

Best,
Henning

[For admin and other information see: http://www.mta.ca/~cat-dist/ ]

Re: Functor fibrations and Cartesian closure of general presheaves

[Thomas Streicher]

For the first question I may refer to p.17 of my Notes on Fibrations
namely the last paragraph "Fibrations of Diagrams"

I know this from the unpublished lectures notes by Roisin of a course
Benabou gave in 1980 in Louvain-la-Neuve

Thomas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]