In my last mailing, I talked about my attempt to develop vector spaces from CCC's with finite sets and real arithmetic. Now it's time for some questions. (1) Assume a category with domains I, standing for a finite set; and R, standing for the reals. If it's a CCC, we can get the biproduct structure, by currying the Kronecker delta, i.e. the equality function on I. Even to express very simple statements about vectors, one now needs a legitimate way to write _summation over_ I. E.g. if we have a full set of injectors eta : I -> X where X = [I->R] we want to write an arbitrary vector as Sigma x(i) (eta i) i e I This is shorthand for something like compose : R x R x ... x R -> X where the R's correspond 1-1 with I. It's the domain I itself (rather than any element of it) which determines that finite product. We know what we mean, by summation over I; but it seems to me that (1) we are relying on induction over I, and therefore on first, last and successor arrows to I, the whole Peano development; and (2) that this is not explicit in the CCC definition. Yes, it is stated that a CCC has all finite products. But to make this formal, we need a formal means of expressing the inductive step; the equivalent, perhaps of a FOR loop in algorithms. Is there a standard way to address this? (2) To make the issue more pointed, let's step back from our category, and name it X(I,R). Now, define a category of finite sets, say Y, in which I1, I2, ... are domains, and each one can stand in for I, so that we have X(I1,R), etc. We would like to say, there is a category V(Y,R), of all such categories; and define a functor V(-,R): Y => X(Y,R) : I |=> X(I,R) We should be able to say that VECT(R) is a proper subcategory of V(,-R), because each f : Y -> Y maps onto V(f,R) : X(Y,R) -> X(Y,R) : X(I,R) |-> X(f(I),R) But there is more to V(-,R) than that. For one thing, there will be a unique arrow in V(-,R), expressing summation (or in general what they call "fold", or APL, "reduce"), fold : [RxR ->R] x Y -> [[Y -> R] -> R] such that fold <(+),I> : [[I -> R] -> R] : (i |-> a(i)) |-> Sigma(i) a(i) The fold arrow expresses _reduction by a real binary function, over an inductable set_, producing a unique arrow in each X(I,R) that does the job. Now if this makes me uneasy, it's possibly just "abstraction vertigo". As far as I can make out, fold is justified iff in Y, each domain I is equipped with arrows: first : 1 -> I last: 1 -> I next : (I-last(I)) -> I That means that in Y itself, one can define: First: Y -> (1->Y) : I |-> (first : 1 -> I) etc. Something is slipping here, and I think its that the notation is being overloaded when "I" refers both to a domain in Y, and to the actual finite set it denotes. It seems to me there much be a well-tried way of doing this, but my reading into categories in language specification haven't disclosed anyone spelling it out. (3) Now for a major issue. I managed to define my biproduct in X(I,R) by defining X(I,R) as a CCC, with real arithmetic, equality on I, _and only that_. Which seems to me a notable finding, and one to be followed up. In introducing functors on X(I,R), and further, functors on X(Y,R), I want to deduce the consequences of X(I,R) being Cartesian closed. Therefore I want to develop just those functors which map one CCC to another. Such functors will only be coherent, so to speak, if they map values to values, products to products, and exponentials to exponentials. That is, if they preserve Cartesian closure. What has been said about the properties of such functors? I'm following one lead, John W. Gray, _A Categorical Treatment of Polymorphic Operations_ in _S-V Lecture Notes in Computer Science 298, Mathematical Foundations of programming Language Semantics_. Let's just say about this, that the development of functors between exponential domains is more complex than I had expected. Enough for the present.