Re: are fibrations evil?

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

Sure, they are "evil" but it seems to be beneficial to be "evil" sometimes.
If the equivalence closed version would have been the original one I doubt
that it would have been recognized how useful they are for category theory
over fairly general bases. Or, rather, people would have quickly shifted to
the "evil" version.

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!).

Thomas


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