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