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
_______________________________________________
Axiom-math mailing list
[email protected]
http://lists.nongnu.org/mailman/listinfo/axiom-math
