Subject: categories: Constructive Category Theory

From: Steve Stevenson <[email-masked]>
Date: Fri, 13 Feb 2004 09:30:25 -0500

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

steve
--------
D. E. Stevenson, Department of Computer Science
Director, Institute for Modeling and Simulation Applications
Clemson University, Clemson, SC 29634-0974
864.656.5880 http://www.cs.clemson.edu/~steve

---

From: Bas Spitters <[email-masked]>
Date: Mon, 16 Feb 2004 16:53:55 +0100

> 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: [email-masked]  Phone: +31-24-3652631.
Fax: +31-24-3652525 Room: A5024
http://www.cs.kun.nl/~spitters/

---

From: Jeremy Gibbons <[email-masked]>
Date: Mon, 23 Feb 2004 12:35:01 GMT

> If so, what is a good reference?

Not sure if this is what you're looking for, but there's a
very nice paper, "Category theory as coherently constructive
lattice theory", by Roland Backhouse et al:

  http://www.cs.nott.ac.uk/~rcb/papers/abstract.html#CatTheory

Jeremy

-- 
[email-masked]
  Oxford University Computing Laboratory,    TEL: +44 1865 283508
  Wolfson Building, Parks Road,              FAX: +44 1865 273839
  Oxford OX1 3QD, UK.
  URL: http://www.comlab.ox.ac.uk/oucl/people/jeremy.gibbons.html