Re: reverting religious terminology

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

Sorry for forgetting about your posting from a couple of weeks ago. I can
see that working with essential fibres escapes my criticism.
Still I feel uneasy about it because it messes up things to such an extent
that I can't imagine to rewrite even a basic introductory section of a text
about fibrations in terms of weak fibrations. Of course, one could do it using
the language  of intensional type theory and then interpreting it in the
groupoid model. I couldn't say in advance whether formalizing basic theory of
fibrations in intensional type theory is possible. Experience tells us that
there pop up unpleaseant suprises in even simpler situations.
So my question is what do you (or other readers of the list) think why a
non-evil account of fibrations could be useful after all besides for
ideological reasons. Generalising to 2-categories like toposes and geometric
morphisms - which is useful - is not an example because there one still may
stay strict and reduce everything to Grothendieck fibrations as you have
explained convincingly.
From http://ncatlab.org/nlab/show/Grothendieck+fibration I take that weak
fibrations are necessary only when considering fibrations in bicategories
that are not 2-categories. Why not take the paradigmatic case of the bicategory
Dist of distributors. Has this exampe been worked out in detail.

Thomas


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