From: Thomas Streicher <streicher@mathematik.tu-darmstadt.de>
To: categories@mta.ca
Subject: are fibrations evil?
Date: Wed, 15 Sep 2010 13:43:49 +0200 [thread overview]
Message-ID: <E1Ow1kx-0002Vi-3Z@mlist.mta.ca> (raw)
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/ ]
next reply other threads:[~2010-09-15 11:43 UTC|newest]
Thread overview: 30+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-09-15 11:43 Thomas Streicher [this message]
2010-09-16 0:28 ` Michael Shulman
2010-09-16 1:14 ` Peter LeFanu Lumsdaine
2010-09-16 5:14 ` Is equality evil? Vaughan Pratt
2010-09-17 8:28 ` Toby Bartels
2010-09-18 14:11 ` Thomas Streicher
2010-09-19 20:30 ` Erik Palmgren
2010-09-24 12:50 ` Bas Spitters
[not found] ` <20100918141110.GC9467@mathematik.tu-darmstadt.de>
2010-09-22 4:00 ` Toby Bartels
2010-09-25 16:18 ` Michael Shulman
[not found] ` <20100922040041.GB14958@ugcs.caltech.edu>
2010-09-22 10:27 ` Thomas Streicher
2010-09-16 8:50 ` why it matters that fibrations are "evil" Thomas Streicher
[not found] ` <AANLkTinosTZ2NQW9biPxiwpX9zPi5m=kwvA16nHjK=Xu@mail.gmail.com>
2010-09-16 9:47 ` are fibrations evil? Thomas Streicher
2010-09-16 10:00 ` Prof. Peter Johnstone
[not found] ` <alpine.LRH.2.00.1009161023190.12162@siskin.dpmms.cam.ac.uk>
2010-09-16 10:46 ` Thomas Streicher
2010-09-17 7:44 ` Toby Bartels
[not found] ` <20100916094755.GA19976@mathematik.tu-darmstadt.de>
2010-09-17 5:01 ` Michael Shulman
2010-09-18 13:48 ` Thomas Streicher
[not found] ` <20100918134829.GB9467@mathematik.tu-darmstadt.de>
2010-09-20 16:25 ` Michael Shulman
2010-09-17 2:17 David Roberts
2010-09-17 4:36 John Baez
2010-09-18 13:50 ` Joyal, André
2010-09-19 14:57 ` David Yetter
[not found] ` <F8DA87C6-CBED-44AE-B964-B766A95D8417@math.ksu.edu>
2010-09-19 18:21 ` Joyal, André
2010-09-20 17:04 ` Eduardo J. Dubuc
2010-09-20 16:59 ` Eduardo J. Dubuc
2010-09-22 2:52 ` Toby Bartels
[not found] ` <20100922025245.GA14958@ugcs.caltech.edu>
2010-09-22 18:56 ` Eduardo J. Dubuc
[not found] ` <4C9A5156.3010307@dm.uba.ar>
2010-09-22 21:06 ` Toby Bartels
2010-09-24 23:43 Fred E.J. Linton
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=E1Ow1kx-0002Vi-3Z@mlist.mta.ca \
--to=streicher@mathematik.tu-darmstadt.de \
--cc=categories@mta.ca \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox;
as well as URLs for NNTP newsgroup(s).