From: "Peter LeFanu Lumsdaine" <plumsdai@andrew.cmu.edu>
To: categories@mta.ca
Subject: Re: terminology
Date: Tue, 1 Jun 2010 09:33:30 -0400 [thread overview]
Message-ID: <E1OJnUR-0005oV-Qi@mailserv.mta.ca> (raw)
In-Reply-To: <E1OJQI5-0002SA-Jy@mailserv.mta.ca>
On Tue, June 1, 2010 03:39, Thorsten Altenkirch wrote:
> A setoid is the intensional representation of a quotient (ie
> coequalizer) and any construction involving it should respect this
> structure. To use the underlying set of a setoid to construct another set
> seems fundamentally flawed.
Indeed; but what we construct is not just a set, it's a category! :-)
In Toby's construction \C |---> arr \C, the setoid structure of the
hom-sets of \C is _not_ respected if you just look at the underlying
objects of arr \C, but it _is_ respected once you look at the whole
resulting category arr \C.
This is surely no worse than the fact that in just about any construction
on setoids X |---> F(X), if you look at the underlying set of F(X), this
will not fully respect the setoid structure of X?
> My understanding of an arrow category is that it's objects are the
> morphisms of the underlying category and since this is a setoid objects
> should be represented as a setoid too.
The trouble here is that the original setoid structure is not on the whole
arrow-set C_1, but on the individual hom-sets C_1(a,b). The arrow
category sums this up over all a,b:C_0, and so is no longer a setoid from
this data alone. (A dependent sum of setoids over a set doesn't have a
natural setoid structure, as far as I can see?)
In our case, of course, the object-sets _are_ also naturally setoids, with
their equalities given by isomorphisms of the categories. But we don't
want to think of this setoid structure as primary: it's just a coarse
reflection of part of the overall category structure.
> You may say that we are only interested in objects upto isomorphism.
> But what does this mean precisely?
Going on from the above, it's an extension to the statement "we are only
interested in elements of a setoid up to the given equality relation". So
a more precise statement could go along the lines of: Any construction
dependent on objects should respect isomorphisms.
Best,
-p.
--
Peter LeFanu Lumsdaine
Carnegie Mellon University
[For admin and other information see: http://www.mta.ca/~cat-dist/ ]
next prev parent reply other threads:[~2010-06-01 13:33 UTC|newest]
Thread overview: 83+ messages / expand[flat|nested] mbox.gz Atom feed top
2010-05-19 10:38 Re terminology: Ronnie Brown
2010-05-20 7:58 ` soloviev
2010-05-20 19:53 ` terminology Eduardo J. Dubuc
2010-05-20 22:15 ` Re terminology: Joyal, Andre
2010-05-20 11:58 ` Urs Schreiber
[not found] ` <AANLkTikre9x4Qikw0mqOl1qZs9DDSkcBu3CXWA05OTQT@mail.gmail.com>
2010-05-21 17:00 ` Ronnie Brown
2010-05-22 19:40 ` Joyal, André
[not found] ` <B3C24EA955FF0C4EA14658997CD3E25E370F5827@CAHIER.gst.uqam.ca>
2010-05-22 21:43 ` terminology Ronnie Brown
[not found] ` <4BF84FF3.7060806@btinternet.com>
2010-05-22 22:44 ` terminology Joyal, André
2010-05-23 15:39 ` terminology Colin McLarty
2010-05-24 13:42 ` equivalence terminology Paul Taylor
2010-05-24 15:53 ` we do meet isomorphisms of categories Marco Grandis
2010-05-26 15:21 ` Toby Bartels
2010-05-27 9:29 ` Prof. Peter Johnstone
[not found] ` <alpine.LRH.2.00.1005271007240.11352@siskin.dpmms.cam.ac.uk>
2010-05-27 10:08 ` Marco Grandis
2010-05-30 12:05 ` Joyal, André
2010-05-24 18:04 ` terminology Vaughan Pratt
2010-05-26 3:08 ` terminology Toby Bartels
2010-05-24 23:06 ` Equality again Joyal, André
2010-05-26 2:27 ` Patrik Eklund
2010-05-27 11:30 ` Prof. Peter Johnstone
2010-06-01 6:36 ` Marco Grandis
2010-06-01 14:38 ` Joyal, André
2010-05-25 14:08 ` terminology John Baez
2010-05-25 19:39 ` terminology Colin McLarty
2010-05-29 21:47 ` terminology Toby Bartels
2010-05-30 19:15 ` terminology Thorsten Altenkirch
[not found] ` <A46C7965-B4E7-42E6-AE97-6C1D930AC878@cs.nott.ac.uk>
2010-05-30 20:51 ` terminology Toby Bartels
2010-06-01 7:39 ` terminology Thorsten Altenkirch
2010-06-01 13:33 ` Peter LeFanu Lumsdaine [this message]
[not found] ` <7BF50141-7775-4D3C-A4AF-D543891666B9@cs.nott.ac.uk>
2010-06-01 18:22 ` terminology Toby Bartels
2010-05-26 8:03 ` terminology Reinhard Boerger
[not found] ` <4BF6BC2C.2000606@btinternet.com>
2010-05-21 18:48 ` Re terminology: Urs Schreiber
[not found] ` <AANLkTilG69hcX7ZV8zrLpQ_nf1pCmyktsnuE0RyJtQYF@mail.gmail.com>
2010-05-26 8:28 ` terminology John Baez
-- strict thread matches above, loose matches on Subject: below --
2017-02-11 20:42 Terminology Fred E.J. Linton
2017-02-14 8:48 ` Terminology Steve Vickers
[not found] ` <02568D97-0A72-4CA8-8900-BDE11E890890@cs.bham.ac.uk>
2017-02-14 9:39 ` Terminology Jean Benabou
2017-02-09 22:03 Terminology Andrée Ehresmann
2017-02-08 8:03 Terminology Jean Benabou
2017-02-08 16:34 ` Terminology Jirí Adámek
2017-02-10 1:42 ` Terminology George Janelidze
2017-02-08 21:40 ` Terminology Carsten Führmann
2017-02-09 11:31 ` Terminology Thomas Streicher
[not found] ` <20170208180636.18346065.28939.42961@rbccm.com>
2017-02-09 16:38 ` Terminology Jean Benabou
2017-02-11 15:07 ` Terminology Steve Vickers
2013-05-02 3:57 Terminology Fred E.J. Linton
2013-05-03 11:53 ` Terminology Robert Dawson
2013-05-02 3:57 Terminology Fred E.J. Linton
2013-04-30 1:20 Terminology Fred E.J. Linton
2013-04-24 17:13 Terminology Jean Bénabou
2013-04-24 23:04 ` Terminology David Roberts
2013-04-27 13:08 ` Terminology Thomas Streicher
[not found] ` <20130427130857.GC16801@mathematik.tu-darmstadt.de>
2013-04-28 3:49 ` Terminology Jean Bénabou
2013-04-28 22:47 ` Terminology Olivier Gerard
[not found] ` <557435A6-4568-4012-8C63-E031931F41FB@wanadoo.fr>
2013-04-28 14:17 ` Terminology Thomas Streicher
2013-04-29 20:05 ` Terminology Toby Bartels
2013-04-30 0:58 ` Terminology Peter May
2010-09-29 2:03 terminology Todd Trimble
2010-09-28 4:38 terminology Eduardo J. Dubuc
2010-05-27 18:31 terminology Colin McLarty
2010-05-16 12:44 terminology Peter Selinger
2010-05-13 17:17 bilax_monoidal_functors Michael Shulman
2010-05-14 14:43 ` terminology (was: bilax_monoidal_functors) Peter Selinger
2010-05-15 19:52 ` terminology Toby Bartels
2010-05-08 3:27 RE : bilax monoidal functors John Baez
2010-05-10 18:16 ` bilax_monoidal_functors?= John Baez
2010-05-11 8:28 ` bilax_monoidal_functors?= Michael Batanin
2010-05-12 3:02 ` bilax_monoidal_functors?= Toby Bartels
2010-05-13 23:09 ` bilax_monoidal_functors?= Michael Batanin
2010-05-15 16:05 ` terminology Joyal, André
2007-01-27 17:06 terminology wlawvere
2007-01-26 23:30 terminology Eduardo Dubuc
2005-12-30 1:16 terminology vs27
2005-12-29 19:09 terminology Nikita Danilov
2005-12-10 3:51 Terminology jean benabou
2005-12-21 20:04 ` Terminology Eduardo Dubuc
2005-12-26 19:47 ` terminology Vaughan Pratt
2005-12-29 23:17 ` terminology Eduardo Dubuc
2006-01-04 14:59 ` terminology Eduardo Dubuc
2003-10-17 15:19 terminology Marco Grandis
2003-10-16 21:39 terminology James Stasheff
2001-04-09 11:06 Terminology Krzysztof Worytkiewicz
2000-12-14 6:17 Terminology Max Kelly
[not found] <3a35cdd73a39f901@amyris.wanadoo.fr>
2000-12-13 11:10 ` Terminology Dr. P.T. Johnstone
2000-12-13 1:17 Terminology Steve Lack
2000-12-12 8:19 Terminology Jean Benabou
2000-01-28 12:02 terminology James Stasheff
2000-01-28 9:57 terminology Marco Grandis
2000-01-27 19:28 terminology James Stasheff
2000-01-27 21:04 ` terminology Paul Glenn
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=E1OJnUR-0005oV-Qi@mailserv.mta.ca \
--to=plumsdai@andrew.cmu.edu \
--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).