From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6288 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: reverting religious terminology Date: Mon, 4 Oct 2010 21:38:02 +0200 Message-ID: References: Reply-To: Thomas Streicher NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Trace: dough.gmane.org 1286280924 9830 80.91.229.12 (5 Oct 2010 12:15:24 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Tue, 5 Oct 2010 12:15:24 +0000 (UTC) Cc: categories@mta.ca To: Michael Shulman Original-X-From: majordomo@mlist.mta.ca Tue Oct 05 14:15:22 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.138]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1P36QS-0000RO-Ky for gsmc-categories@m.gmane.org; Tue, 05 Oct 2010 14:15:20 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:42010) by smtpx.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1P36Pf-0001R2-Vk; Tue, 05 Oct 2010 09:14:31 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1P36Pb-0000FG-VI for categories-list@mlist.mta.ca; Tue, 05 Oct 2010 09:14:28 -0300 Content-Disposition: inline In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6288 Archived-At: 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/ ]