[Aldor-l] [Axiom-math] Type equivalence of domains in Axiom and Aldor

[Ralf Hemmecke]

>   Def: Two domains P and Q are equivalent if and only if both domains satisfy
>   exactly the same set of categories: (P has x) = (Q has x) for all Category
>   expressions x *and* neither P nor Q has any explicit exports that are not
>   provided by some named category.

Let's see...

Cat: Category == with {
   coerce: Integer -> %;
   coerce: % -> Integer;
   bar: (%, %) ->  %;
}
P: Cat == add {
   Rep == Integer; import from Rep
   coerce(x: Integer): % == per x;
   coerce(x: %): Integer == rep x;
   bar(x: %, y: %): % == per(rep x + rep y);
}
----------------------------------^

Q: Cat == add {
   Rep == Integer; import from Rep
   coerce(x: Integer): % == per x;
   coerce(x: %): Integer == rep x;
   bar(x: %, y: %): % == per(rep x - rep y);
}
----------------------------------^

You are saying that P and Q are equivalent.

Ralf