Re: are fibrations evil?

[Toby Bartels <toby+categories@ugcs.caltech.edu>]

Thomas Streicher wrote at last:

>BTW under a regime which identifies equality with being isomorphic (or weakly
>equivalent) it looks tempting to use functors from B^\op to Cat. These should
>capture the pseudo-functors since equality and isomorphism are identified. But
>writing down functoriality in type theory using \Sigma for existence amounts
>to choosing a lot of not at all canonical "canonical isomorphisms". Actually,
>one would get something even more general than pseudo-functors because one
>wouldn't write down the coherence conditions (actually one couldn't even
>since there is no honest for good equality!).

Yes, you can write the coherence conditions down
(although I agree that it would be easy to forget them).

What you need is that a functor (pseudofunctor) P: B^\op -> Cat
is not just the following data:
*  for each object x of B,
     a category P_x,
*  for each object x, object y, and morphism f: x -> y,
     a functor P_f: P_x -> P_y,
*  functoriality structure (and maybe coherence conditions);
but in fact the following data:
*  for each object x of B,
     a category P_x,
*  for each object x, object y, and morphism f: x -> y,
     a functor P_f: P_y -> P_x,
*  for each object x, object y, and equal morphisms f = g: x -> y,
     a natural isomorphism P_{f=g}: P_f => P_g,
*  functoriality structure and coherence conditions.

For example, given f: w -> x, g: x -> y, and h: y -> z in B,
we want to compare (P_f . P_g) . P_h with P_f . (P_g . P_h).
In a "kosher" treatment of category theory, these aren't equal
(that would be meaningless), but there is an associator between them.
As a coherence condition, we want to demand that this associator
is equal (and this does have meaning) to a natural isomorphism
built out of the functoriality structure isomorphisms and their inverses.
As we do this, we need to compare P_{(f;g);h} and P_{f;(g;h)}.
Again, it's not meaningful (much less true) that these are equal,
but P_{(f;g);h = f;(g;h)} is a natural isomorphism between them.
So we can write down this coherence condition after all.


--Toby


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