From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6173 Path: news.gmane.org!not-for-mail From: Thomas Streicher Newsgroups: gmane.science.mathematics.categories Subject: are fibrations evil? Date: Wed, 15 Sep 2010 13:43:49 +0200 Message-ID: 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 1284594762 16229 80.91.229.12 (15 Sep 2010 23:52:42 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Wed, 15 Sep 2010 23:52:42 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Thu Sep 16 01:52:41 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 1Ow1mL-0005Oc-22 for gsmc-categories@m.gmane.org; Thu, 16 Sep 2010 01:52:41 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:47178) by smtpy.mta.ca with esmtp (Exim 4.71) (envelope-from ) id 1Ow1l2-0007s2-Lg; Wed, 15 Sep 2010 20:51:21 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1Ow1kx-0002Vi-3Z for categories-list@mlist.mta.ca; Wed, 15 Sep 2010 20:51:15 -0300 Content-Disposition: inline Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6173 Archived-At: On the occasion of the discussion about "evil" I want to point out an example where speaking about equality of objects seems to be indispensible. If P : XX -> BB is a functor and one wants to say that it is a fibration then one is inclined to formulate this as follows if u : J -> I is a map in BB and PX = I then there exists a morphism \phi : Y -> X with P\phi = u and \phi cartesian, i.e. ... I don't see how to avoid reference to equality of objects in this formulation. This already happens if XX and BB are groupoids where P : XX -> BB is a fibration iff for all u : J -> I in BB and PX = I there is a map \phi : Y -> X with P\phi = u. Ironically the category of groupoids and fibrations of groupoids as families of types was the first example of a model of type theory where equality may be interpreted as being isomorphic. So my conclusion is that equality of objects is sometimes absolutely necessary. Avoiding reference to equality is also not a question of using dependent types as some people implicitly seem to say. Even in intensional type theory there is a notion of equality. But it is sometimes inconvenient to use. As pointed out by Ahrens one can and should use extensional type theory whenever convenient. Intensional type theory allows one to interpret equality as being isomorphic, a kind of reward for the inconvenience of using intensional identity types. Thomas [For admin and other information see: http://www.mta.ca/~cat-dist/ ]