From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/6944 Path: news.gmane.org!not-for-mail From: Michael J Healy Newsgroups: gmane.science.mathematics.categories Subject: Re: diagrams in computer algebra Date: Mon, 3 Oct 2011 12:02:13 -0600 Message-ID: References: Reply-To: Michael J Healy NNTP-Posting-Host: lo.gmane.org Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=us-ascii Content-Transfer-Encoding: quoted-printable X-Trace: dough.gmane.org 1317723971 21252 80.91.229.12 (4 Oct 2011 10:26:11 GMT) X-Complaints-To: usenet@dough.gmane.org NNTP-Posting-Date: Tue, 4 Oct 2011 10:26:11 +0000 (UTC) To: categories@mta.ca Original-X-From: majordomo@mlist.mta.ca Tue Oct 04 12:25:50 2011 Return-path: Envelope-to: gsmc-categories@m.gmane.org Original-Received: from smtpx.mta.ca ([138.73.1.30]) by lo.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1RB2C5-0001Zb-QJ for gsmc-categories@m.gmane.org; Tue, 04 Oct 2011 12:25:49 +0200 Original-Received: from mlist.mta.ca ([138.73.1.63]:33821) by smtpx.mta.ca with esmtp (Exim 4.76) (envelope-from ) id 1RB2AJ-00084q-Bc; Tue, 04 Oct 2011 07:23:59 -0300 Original-Received: from majordomo by mlist.mta.ca with local (Exim 4.71) (envelope-from ) id 1RB2AH-0002U7-NZ for categories-list@mlist.mta.ca; Tue, 04 Oct 2011 07:23:57 -0300 In-Reply-To: Precedence: bulk Xref: news.gmane.org gmane.science.mathematics.categories:6944 Archived-At: Sergei, My colleagues and I have been looking for something like this for a = project. We need to be able to specify small categories as the = completions of finite graphs we are given, extend these by specifying = commutative diagrams, pullbacks, etc, of interest, then define functors = generated from graph homomorphisms, and take colimits of diagrams in = Cat, etc etc. We haven't found anything that does all this. So, we're = programming it in Haskell---one of our grad students knows the language. = We'll be happy to share our experience and will probably make the code = available. It's a work in progress. Best regards, Mike Healy On Oct 2, 2011, at 3:10 PM, Sergei SOLOVIEV wrote: > Question to the list: >=20 > I am very much interested, does there exist any practically usable > system for the "computer algebra style" work with diagrams. I.e. not > just write down the diagrams (like XyPic) but for example for > diagram chasing, > verification of commutativity in any interesting classes of categories > with structure etc. As I remember there were some systems permitting > computation of some limits in very limited classes of categories, > also some heavy attempts of formalisation in some general > purpose proof assistants > but I do not know about anything else. >=20 > Regards to all >=20 > Sergei Soloviev >=20 [For admin and other information see: http://www.mta.ca/~cat-dist/ ]