From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6179 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: Re: are fibrations evil? Date: Thu, 16 Sep 2010 11:47:55 +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 1284689132 17292 80.91.229.12 (17 Sep 2010 02:05:32 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Fri, 17 Sep 2010 02:05:32 +0000 (UTC) Cc: categories@mta.ca To: Michael Shulman Original-X-From: majordomo@mlist.mta.ca Fri Sep 17 04:05:31 2010 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpy.mta.ca ([138.73.1.139]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1OwQKQ-0003sM-Cv for gsmc-categories@m.gmane.org; Fri, 17 Sep 2010 04:05:30 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:42657) by smtpy.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1OwQJB-0002lf-C1; Thu, 16 Sep 2010 23:04:13 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1OwQJ7-0002i7-Ot for categories-list@mlist.mta.ca; Thu, 16 Sep 2010 23:04:09 -0300 Content-Disposition: inline Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6179 Archived-At: Dear Michael, Street's notion of fibration is a weakening not a strengthening of Grothendieck fibrations. For such a thing the key intuitions are lost as far as I can see (even if I and J are isomorphic the fibre over I may be inhabited whereas the fibre over J is inhabited). I doubt that category theory over a base (topos) can be deloped this way. At least it would be very cumbersome. Has the generalised notion of fibration been used for something? I agree with you that Kan fibrations in simplicial sets are an alternative and certainly the right thing if one want's to get "weak". After all that's what I suggested in 2006 in a talk in Uppsala. I personally am interested in the possibility of having type theories where equality coincides with being isomorphic or even weakly equivalent (as recently suggested by Voevodsky). But this is an extremal point of view which shouldn't be taken absolute since otherwise important parts of category theory get lost. I suspect that when doing fibered categories in a type theory validating Voevodsky's equivalence axiom one comes up with something like Street's generalisation of fibrations. But that doesn't mean that we arrive at something easy to work with. What Martin Hofmann and I thought when bringing up the idea was that use of intensional Id-types amounts to imposing a brutal bureaucracy which FORCES you to check all the coherence conditions often swept under the carpet. I think when interpreting type theory in the topos SSet of simplicial sets one can have both extensional Id-types and the intensional ones. In the first case a family of types is simply a map of SSet, in the second case it is a Kan fibration. Luckily both system of display maps are closed under \Sigma and \Pi. Thus the intensional model sits within the extensional one. It is the restriction to "kosher" types, i.e. Kan complexes. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]