Re: [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