[Axiom-developer] RE: categorial rep and per?

[Bill Page]

On May 12, 2007 5:35 AM Ralf Hemmecke wrote:
> 
> On
> 
> http://wiki.axiom-developer.org/SandBoxLimitsAndColimits
> 
> you write
> 
> > I am especially interested in how the duality between rep
> > and per is involved in these constructions.
> 
> My answer is: I don't know.

What I mean specifically is:

    project1(x:%):X == rep(x).a
    project2(x:%):Y == rep(x).b
    product(A:Type,f:A->X,g:A->Y):(A->%) ==
       (x:A):% +-> per [f(x),g(x)]

versus

    inject1(x:X):% == per [a==x]
    inject2(y:Y):% == per [b==y]
    sum(A:Type,f:X->A,g:Y->A):(%->A) ==
       (x:%):A +->
         rep(x) case a => f(rep(x).a)
         rep(x) case b => g(rep(x).b)
         never

Do you see how rep is used in the definition of 'project' but
per is used in the definition of 'inject'? And opposite in the
definitions of 'product' and 'sum'? I just thought that was a
little unexpected (to me) by-product of the duality.

> And I also don't know why you think that per and rep is
> something categorial.

Categorical in the sense of category theory - not necessarily
in the sense of category used in Axiom/Aldor. I guess I could
put it this way: I *want* to find a categorical definition of
rep and per because I do not fully understand why they appear
in Spad and Aldor but not in any other "object-oriented"
language with which I am familiar. I think (perhaps) that Spad
has made something explicit that is in fact implicit in these
other programming languages. Making this explicit is a good
thing, but I am not completely confident that the current
implementation - as a distinguished name 'Rep' and macros
'rep' and 'per'. I would like (perhaps) an appropriate
categorical semantics for rep and per and maybe some other
syntax in the Spad/Aldor language that properly distinguishes
this construct -- after all, this notion is central to the
implementation of abstract algebra in Axiom.

I tried to do something like this a while ago in

http://wiki.axiom-developer.org/RepAndPer

Perhaps it needs a little updating since I wrote it.

> 
> Suppose I have a domain R with some exports CatR. And I 
> define for some other exports CatD a domain
> 
> D: CatD == add {
>    Rep == R;
>    ...
> }
> 
> rep and per relate R with D (basically saying that they
> are the same things as data structures with no features).
> But their exports have no relation at all.

Their exports are in fact related by the logic that is
implemented in ...

Exports are arrows.

> Mathematically seen, they are objects of different 
> categories. So rep and per would be functors (if
> anything). But how can such a construction be made
> functorial. I don't see that.
> 

It is necessary to define more clearly I think what
*mathematical* category we are talking about. I was arguing
in RepAndPer that yes rep and per are adjoint functors in
a categorical sense. I still think that might be a fruitful
point of view.

Regards,
Bill Page.