[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
## [Axiom-developer] a little category theory and inductive types

**From**: |
Bill Page |

**Subject**: |
[Axiom-developer] a little category theory and inductive types |

**Date**: |
Sat, 12 May 2007 01:58:56 -0400 |

Ralf,
I have updated my example of one way to write an inductive type (as
per our recent discussion with Gaby) so that I hope the structure
of the definition is more clear. See:
http://wiki.axiom-developer.org/SandBoxAldorInductiveTypes
In particular I found it convenient to first implement an extension
of Aldor's Union type to make it more "categorical", i.e. as a
true co-product in the sense of category theory. See
http://wiki.axiom-developer.org/SandBoxLimitsAndColimits
This exercise makes me think that there may be a potential for
developing a new library in Aldor and domains in Spad that would
provide these and similar categorical constructs.
I would be most interested in your comments on this approach.
Regards,
Bill Page.

**[Axiom-developer] a little category theory and inductive types**,
*Bill Page* **<=**