From mboxrd@z Thu Jan 1 00:00:00 1970 X-Msuck: nntp://news.gmane.io/gmane.science.mathematics.categories/1091 Path: news.gmane.org!not-for-mail From: Paul Taylor Newsgroups: gmane.science.mathematics.categories Subject: Ronnie Brown's type-dream Date: Fri, 19 Mar 1999 19:23:37 GMT Message-ID: <199903191923.TAA08560@wax.dcs.qmw.ac.uk> NNTP-Posting-Host: main.gmane.org X-Trace: ger.gmane.org 1241017560 29454 80.91.229.2 (29 Apr 2009 15:06:00 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 29 Apr 2009 15:06:00 +0000 (UTC) To: categories@mta.ca Original-X-From: cat-dist Sat Mar 20 12:10:33 1999 Original-Received: (from Majordom@localhost) by mailserv.mta.ca (8.9.3/8.9.3) id LAA22550 for categories-list; Sat, 20 Mar 1999 11:10:49 -0400 (AST) X-Authentication-Warning: mailserv.mta.ca: Majordom set sender to cat-dist@mta.ca using -f Original-Sender: cat-dist@mta.ca Precedence: bulk Original-Lines: 51 Xref: news.gmane.org gmane.science.mathematics.categories:1091 Archived-At: Ronnie Brown asked, > This is written from the point of view of someone who would like to see a > computational system which is much nearer to real mathematics than the > current widely used systems (Maple, Mathematica, and various more > specialised systems, e.g. Singular). .... > So my question is: does all this general theory of types give a clear > indication as to what should be, not necessarily a final, but certainly a > convenient theory adequate for expressing a majority of present day maths? > > Let's make up a test case: one should be able to code reasonably > conveniently the type of a general groupoid acting on exterior algebras > over a commutative ring, and also of course the category of such objects. > A groupoid acting on exterior algebras with zero multiplication should be > coercible to a groupoid acting on graded modules. > > I would prefer the sytem to be so simple that it will allow tests for > consistency of new proposed types. Also it should be easy to understand, > since it would represent nicely current practice. > > Is this idea a mirage? No, I don't think it's a mirage, though [help me somebody I need a good pun here] the answer I have in mind may involve some altered states of perception. For the moment I want to steer clear of the "computational" question, as I haven't begun work on that, and would like to read his "current widely used systems" to refer to set theory, elementary toposes, Martin-Lof type theory and so on. That being said, I wonder whether the discussion and results in my "Abstract Stone Duality" paper (that I advertised on "categories" in the new year and which has since been revised) might appeal to Ronnie. It bases "set theory" on topology and not vice versa. It identifies categories of open discrete and compact Hausdorff spaces that are both pretoposes, and therefore suitable for doing algebra in, though the open discrete spaces are more appropriate for this as they admit free algebras. I do, as I said, have a computational model in mind, but am not yet in a position to say anything about it. Paul This paper, like most of what I talk about, is accessible from my Hypatia page http://hypatia.dcs.qmw.ac.uk/author/TaylorP