why it matters that fibrations are "evil"

[Thomas Streicher <streicher@mathematik.tu-darmstadt.de>]

Let BB be a (base) topos. Then split fibrations over BB correspond to
categories internal to Psh(BB). (Well, in Psh(BB) = Set^{BB^op} one has to
choose Set big enough!). Thus in Psh(B) one can speak about split fibrations
over BB as categories internal to Psh(BB).
To which extent can this be extended to arbitrary fibrations P : XX -> BB
typically not split. In a recent paper by Mike Shulman this has been
exercised for the fundamental fibration P_BB : BB^2 -> BB. (Well, he was even
exploiting that P_BB is a stack w.r.t. the regular topology on BB). But it
works for every fibration P. One can speak about P in a first order
dependently typed language L(P) without equality of objects. Generalized
elements of sort "object" at stage I are objects of the fibre P(I) and
similarly for morphisms. Now this language can be given a Kripke-Joyal
interpretation in BB. If P is a JJ-stack then one thinks of BB as endowed with
the topology JJ and incorporates this into the Kripke-Joyal interpretation.
The key trick is that implicitly one quantifies over all possible reindexings.
First I was quite enthusiastic about this because I thought that it augments
the usual fibrational foundations of category theory over an arbitrary base
topos with a linguistic framework entending that of the internal language
of the base (or rather (pre)sheaves over it).

But when trying to test the viability of this approach I came across the
following problem. It is not enough to quantify over objects but one also
has to quantify over families of objects indexed objects of BB.
This leads one to consider also the family fibration Fam(P) over BB together
with the cartesian functor FFam(P) from Fam(P) to P_BB. One can now easily
cook up a language speaking about P, Fam(P) and the cartesian functor FFam(P).
The first thing one wants to show is that the proposition
"Fam(P) is a fibration" holds under the Kripke-Joyal interpretation. But
when writing this down one sees that one cannot escape equality of objects
which has been dropped to make the whole thing possible.

Thus it might be easier to replace P by an equivalent split fibration Sp(P)
and reason about this in Psh(BB). Nothing seems to be lost when one considers
everything up to isomorphism. The question rather is whether this excessive
prevention of "evil" is appropriate. I have some doubts since it prevents
us from speaking about fibrations in a natural way.

Thomas


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