I have two questions, which I hope, someone has the answer or a pointer where I could obtain some hints: Question 1: Let C be a CCC, which not necessarily is a free CCC. Is there a reasonable way of typing C ? More precisely: If X is an object in a (not necessarily free) Cartesian closed category, is it possible to tell, whether X is of the form Y => Z or of the form Y x Z, with suitably chosen Y and Z ? The problem I have is the following: Assume D is a free CCC constructed over a set of constants. Now identify some of the objects in D to yield the not-free CCC C. Now we could think of a situation, where an object in C is of the form U x V and at the same time of the form W => R. On the other hand, the restrictions on the identifications of D-objects, which come from the requirement, that C again is a CCC, could prevent that an object in C could have two possible forms. Question 2: What about the same problem in a symmetric monoidal closed category ? Here things are a bit more complicated, since the bifunctor x no longer is a product and there are no decomposing projection morphisms. In fact, an object which has the form A x (B x C) could be indistingusihable or even identical to an object of the form (A x B) x C. What is known here ? Can an object at the same time be of the form U x V and of the form W => x ?? And what about identifications of products due to assoviativity commutativity and neutrality ? Please reply to cap@ifi.unizh.ch. THANX A LOT FOR YOUR HELP. -- * Prof. Clemens H. CAP cap@ifi.unizh.ch (email) * Dept. of Computer Science +41-1-257 / 4326, 4331 (office voice) * University of Zurich +41-1-363 00 35 (office fax) * Winterthurerstr. 190 +41-1-362 97 11 (home; voice and fax) * CH-8057 Zurich, Switzerland * Motto: "Please do not read the last line of this signature".
Can an object at the same time be of the form U x V and of the form W => x ?? Yes, since it is possible for these to have the same cardinality (e.g., cpo's). John Mitchell
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
participants (3)
-
Clemens Cap -
Edmund Robinson -
John C. Mitchell