From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/5891 Path: news.gmane.org!not-for-mail From: Thorsten Altenkirch Newsgroups: gmane.science.mathematics.categories Subject: Re: terminology Date: Sun, 30 May 2010 20:15:38 +0100 Message-ID: References: Reply-To: Thorsten Altenkirch NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 (Apple Message framework v936) Content-Type: text/plain; charset=ISO-8859-1; format=flowed; delsp=yes Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1275350066 14921 80.91.229.12 (31 May 2010 23:54:26 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Mon, 31 May 2010 23:54:26 +0000 (UTC) To: Toby Bartels Original-X-From: categories@mta.ca Tue Jun 01 01:54:25 2010 connect(): No such file or directory Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from mailserv.mta.ca ([138.73.1.1]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1OJEoK-0004NN-L0 for gsmc-categories@m.gmane.org; Tue, 01 Jun 2010 01:54:24 +0200 Original-Received: from Majordom by mailserv.mta.ca with local (Exim 4.61) (envelope-from ) id 1OJEJ4-00070V-KG for categories-list@mta.ca; Mon, 31 May 2010 20:22:06 -0300 In-Reply-To: Original-Sender: categories@mta.ca Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:5891 Archived-At: > But category theory has been done in Martin-L=F6of type theory: > http://www.cs.st-andrews.ac.uk/~rd/publications/CTMLTT.pdf > It has also been done in the type-theoretic proof assistant Coq: > http://coq.inria.fr/distrib/v8.2/contribs-20090527/ConCaT.html > > In both of these, there *is* a notion of equality (or better, =20 > identity) > at all types, hence a notion of identity of objects of any given =20 > category, > allowing one to define isomorphism of categories, etc. > However, this logicians' identity does not match mathematicians' =20 > equality; > the easiest way to see this is that there are no quotient types. > (This means that already to do set theory, let alone category theory, > you must define a set to be a type equipped with an equivalence =20 > relation. > Such a thing is also called "setoid", depending on which author you =20= > read.) I don't know any reasonable formalisation in Intensional Type Theory. =20= People usually assume that hom sets are a setoid but objects aren't. =20 This means that constructions like arrow categories are not available. =20= To avoid this one would have to formalize explicitely what is a family =20= of setoids indexed over a setoid. After this it is hard to see the =20 category theory... Cheers, Thorsten= [For admin and other information see: http://www.mta.ca/~cat-dist/ ]