Re: Bourbaki and Categories

[Jacques Carette <carette@mcmaster.ca>]

I hereby volunteer my time and the technical resources I have at my
disposal to 'host' a "New Bourbaki based on CT" project.

Why me?
1. I am an interested _user_ of category theory, but not an 'inventor'
in the field.  Neutrality is frequently an asset in a "keeper of the
infrastructure".
2. I need the results of such a project!  My core work (for 11 years in
industry and now 6 in academia) is in "mechanized mathematics", or
computer-based tools that help automate the mathematics process,
explicitly including both computation (i.e. what Maple does) and proof
(i.e. what Coq does).  (The curious can see
http://imps.mcmaster.ca/mathscheme/publications.html for some of our
work and my personal publications page for more).  One cannot
simultaneously build a library of mathematics and know category theory
without seeing its tendrils everywhere.
3. I have a real stake in seeing "mathematics on computers": not only is
it my day-to-day research, I am also the Chair of the Electronic
Services Committee for the Canadian Mathematical Society (CMS).  I am
actively searching for *good* applications of "electronic services"
where we can get involved.

I cannot promise the resources of the CMS for this, but I can certainly
promise to bring this up as an agenda item for our December meeting in
Ottawa.  However, I would be extremely proud if I could claim, years
from now, that "Bourwiki" was a ``truly international project which
benefited from a strong involvement of the Canadian Mathematical Society''.

Jacques Carette

PS: Below here are some minor comments/thoughts on the various topics in
this email thread -- the only important parts are above.
1. I am fairly fond of the (awfully titled) book "Post-modern Algebra"

http://www.amazon.com/Post-Modern-Algebra-Applied-Mathematics-Wiley-Interscience/dp/0471127388
  by J. Smith and A. Romanwska, as a middle-ground between full-fledged
use of categories and classical algebra in an introductory text.  The
organization of the text is definitely non-classical and tries to
organize concepts according to mathematical criteria rather than
historical timelines.
2. I definitely believe that a proper encoding of modern mathematics
into a 'library' should be done top-done by specializing abstract
concepts.  The "Little Theories" method from theorem proving is
essentially the recognition that a large body of mathematics is a huge
diagram in an appropriate category of theories. These issues are all too
frequently treated as meta-mathematical.  The constructive theory of
"representations of theories" (via sketches or otherwise) can play a
very important role in software construction.
3. Heuristics and examples are crucial for human understanding of
mathematics.  Thus, while a "mechanized mathematics system" may be built
from highly abstract pieces, it needs to present itself to its users in
as concrete a manner as possible.  This dichotomy between
system-building and usability is further explored in a paper "High-Level
Theories" (available officially at
http://www.springerlink.com/content/b1122523vtm88w73/, unofficially at
http://imps.mcmaster.ca/doc/hlt.pdf )
4. I cannot over-emphasize my agreement with Joyal's statement that "But
mathematics is naturally organised and simple!"
5. To a certain degree, some libraries (like those of the large theorem
provers) attempt "partially unified presentations of mathematics"; some
even have pseudo-databases.  These are unfortunately quite classical in
their structure, with the exception of the work of the Kestrel Institute
(in computer science) which is very categorical.  The algebra library of
the programming language 'Aldor' (www.aldor.org) was definitely
influenced by categories.  Category theory is actively influencing the
development of the language 'Haskell'.
6. What I propose to help with are the technical and online aspects of
Andre Joyal's proposal:
> A special database for mathematics should be created
> (but I dont know how).
> Papers in the NB section of the arXves could be selected,
> modified and organised with a system of references,
> to give a partially unified presentation of mathematics.
> The same database could support different
> presentations realised by different competing teams.
> Each team could work like a mathematical journal,
> with an editor in chief and an editorial board.
>
using means like the ones which Andrej Bauer suggested.