[Axiom-developer] a little category theory and inductive types

[Bill Page]

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.