Dear Prof Cap, I just wanted to reinforce the replies of Mitchell and Barr. In any Heyting algebra (cartesian closed poset) there is a great deal of redundancy. In particular, 1 x U = U = 1 => U. And in Set, 0 x U = 0 = V => 0 for any non-empty V, since the empty-set is unique. These are cartesian-closed, and hence a fortiori, monoidal closed, but they are rather semantic models. If you are thinking of presentations of categories as cartesian closed/ symmetric monoidal closed subject to certain equations, then I do not know of any work on syntactic criteria for the equations which would prevent the kind of identification you ask about. This is because a category theorist would never write an equation between objects. Instead they would introduce two maps between the objects (often one at least is pre-existing) and specify that they are inverse isomorphisms. This is not only more in line with "the spirit of category theory", but actually gives you more information, since it tells you how the two structures on the objects are related. In your case, it would tell you, for example, just how a function could be looked at as an ordered pair. A simple equality of objects will not do this. best wishes Edmund Robinson