Re: [Axiom-developer] Curiosities with Axiom mathematical structures

[William Sit]

Bill Page wrote:
> > Ralf Hemmecke wrote:
> > > There is Chapter 9 of Doye's PhD thesis
> > > http://portal.axiom-developer.org/refs/articles/doye-aldor-phd.pdf
> > > which deals in part with the renaming.

> > William Sit wrote:
> > By the way, I don't follow his example at bottom of p. 127:
> > If \phi is a functor (he said homomorphism, but that is wrong,
> > because a list and a set are from different categories),
> 
> Doye's use of the work homomorphism is correct in the context
> of order-sorted algebra. Doye is not using the language of
> category theory in either the mathematical sense or in Axiom's
> sense.

> > What Doye has in mind is the following diagram:
> >
> >                  #
> >           Lists --> NNI
> >             |        |
> >        \phi |        |  id
> >             v   #    v
> >           Sets  --> NNI
> >
> > But there is no reason to expect this to be a commutative
> > diagram of functors. So I think his example illustrates nothing.
> >
> 
> No. The diagram should look like this:
> 
>         #: Lists --> NNI
>                   |
>              \phi |
>                   |
>                   v
>         #: Sets  --> NNI
> 

Thanks, Bill, for clarifying this and my apologies to Doye. So Doye is really
saying the same thing I said, that in his setup, \phi (in your diagram above) is
not a homomorphism and there is no such homomorphism possible. If I follow this
correctly (using normal meaning of functor and category):

  the objects in Doye's setup the objects are functors between categories,     
f:A -> B, g: C -> D, where A, B, C, D are categories
     for example, f = #_List and g = #_Set in your diagram

  a morphism between two such objects f and g is a pair of functors 
    \phi = (h: A->C, k: B->D) which make the diagram below commute:

                f
            A  -->   B
            |        |
          h |        |  k
            v   g    v
            C  -->   D
    

and Doye says for the example f and g, there is no morphism \phi:f -> g where h
is the functor that takes a list to the corresponding set, precisely because my
diagram is not commutative. (I may yet be wrong in this interpretation, since
this could be far from the order-sorted algebra, which I find difficult because
of all the new terms.)

Back to reading more of Doye to understand the implication of this. Is it his
conclusion that automatic coercion is not possible because of this lack of
homomorphism between the two 'ordered-sorted algebras' in Axiom?

William