Has anybody experience in mechanizing category theory or knows
of such work? I'm about to implement basic parts of category
theory in a tactical theorem prover based on higher order
logic. I would appreciate to learn from anybody's earlier
experiences.
Here's a recent announcement on the categories mailing list. See also
ftp://www.maths.su.oz.au/sydcat/software
for various packages by Richard Buckland, Bob Walters, and others.
-- Vaughan Pratt=======================================================
Date: Sat, 16 Mar 1996 10:43:23 -0400 (AST) From: Bob Rosebrugh <rrosebru@mta.ca> To: categories <categories@mta.ca> Subject: Computational Category Theory Tools
CATEGORIES DATABASE/TOOLS
A C program for storage of and computation with finitely presented categories is now available as described below.
The program is menu-based and stores finitely presented categories, functors between them and finite-set valued functors from them. The storage format is the same as that used by the Carmody-Walters `kan' program (available from the University of Sydney ftp site.)
Several tools for computation with finite categories are included. For example, tests for equality of arrows, whether an object is initial and so on. A new implementation of the Todd-Coxeter procedure for computing left Kan extensions is complemented by an implementation of a procedure for computing right Kan extensions. Details are included in the user manual which may be found at ftp://sun1.mta.ca/pub/papers/rosebrugh/catuser.dvi
The program was written by Michael Fleming and Ryan Gunther while they were employed at Mount Allison University under NSERC Canada's USRA program. It is free software and without warranty. Indeed, it should be treated as an `alpha' version. Bug reports (to rrosebrugh@mta.ca) are welcome, but may not be acted upon immediately.
The source code and compiled (Sun and DOS) versions are avalable for ftp from the directory ftp://sun1.mta.ca/pub/sources/rosebrugh/{unix,DOS} The compiled versions are named category.exe. A set of examples is found in the `examples' subdirectories.
Bob Rosebrugh <rrosebrugh@mta.ca>