Subtyping Recursive Types modulo AssociativeCommutative Products

1 Introduction The study of type isomorphisms is concerned with identifying data types by abstract-ing away from irrelevant details in the syntax of types, or--in other words--irrelevant choices in the representation of data. The basic idea is quite simple: one wishes to iden-tify two data types if data of one type can be transformed into data of the other type without loss of information. Formally speaking, o/1 and o/2 are said to be isomorphic ifand only if there exist functions f: o/1! o/2 and g: o/2! o/1 that are mutual inverses,in the sense that they make the following diagram commute