From http://ncatlab.org/nlab/show/Grothendieck+fibration I take that weak fibrations are necessary only when considering fibrations in bicategories
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. 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/ ]