On Coherence in Computer Algebra

Modern computer algebra systems (e.g. AXIOM) support a rich type system including parameterized data types and the possibility of implicit coercions between types. In such a type system it will be frequently the case that there are different ways of building coercions between types. An important requirement is that all coercions between two types coincide, a property which is called coherence. We will prove a coherence theorem for a formal type system having several possibilities of coercions covering many important examples. Moreover, we will give some informal reasoning why the formally defined restrictions can be satisfied by an actual system.