On Friday 13 February 2004 15:30, Steve Stevenson wrote:

Is there a "tradition" in constructive development of category theory? If so, what is a good reference?

I am not aware of a "tradition", but I know two references. In the book A course in constructive algebra (Mines, Richman, Ruitenburg) there is a very short outline of category theory. There is a machine checked formalization inside constructive type theory by Huet and Saibi. http://citeseer.nj.nec.com/huet98constructive.html The impression I got from both approaches is that basic constructive category theory is fairly similar to its its classical counter part, which might explain the apparent lack of tradition. I hope this is of any use. Bas ------------------------------------------------------- Department of Computer Science, University of Nijmegen. P.O.box 9010, NL-6500 GL Nijmegen, The Netherlands. e-mail: spitters@cs.kun.nl Phone: +31-24-3652631. Fax: +31-24-3652525 Room: A5024 http://www.cs.kun.nl/~spitters/