Dear Bob: I now realize that I was overlooking something important in my previous memos on the subject of theories based on categories other then sets. I am convinced that the questions raised are important, but they are not as easy as I thought. I also remain convinced that operations should not be assumed to be morphisms in the underlying category. Just as operations in a theory are not normally morphisms of the theory. What I forgot is that arrows have codomains as well as domains. Thus a morphism n to m in a category is not---except in a metaphorical sense--- simply an n-fold of m-ary operations. So suppose 2 and 3 represent the 2 and 3 element chains, resp. An arrow 2 --> 3 does not simply represent a pair of 3-ary operations, but rather a pair of 3-ary operations of which the first is less than or equal to the second. This means that such inequalities can be built directly into the theory. It also means that the simple-minded HSP theorem I stated before is wrong. (It appears to be correct for the special kind of theories in which every arrow n-->m factors through the set of components of n, a very special case in which there are no non-trivial inequalities between distinct operations.) Now one the most interesting examples is going to be the theory whose models is the set of omega-complete posets; that is posets in which every increasing chain has a sup. A lot can be learned by looking at that example in some detail. Begin with an operation theta:omega+1-->omega. A model of such an operation will assign to each increasing sequence x={x_0<x_1<...} a sequence {theta_0(x)<theta_1(x)<...<theta_omega(x)}. The first thing that has to be done is to put in the equation theta_i(x)=x_i, which is unproblematic and proceeds in the same way as in sets-based theories. A model for the resultant theory assigns to each increasing sequence an upper bound for that sequence. It needn't be the least upper bound, even if the sequence is eventually constant or even constant (although the latter could be added as an equation). What is clearly needed is to add the condition that if x_i<y for all i, the theta_omega(x)<y. Now if we think of this in terms of subcategories, it is clear that the full subcategory of all models that satisfies is HSP, meaning quite precisely that it is closed under strong subobjects, arbitrary products and surjective epimorphisms. Not ALL epimorphisms, even regular ones; here is an example. Let B consist of countably pairs of elements u_i<v_i, not otherwise comparable. Let theta_omega be the sup operation, in this case pretty trivial. Let C be the quotient gotten by identifying v_i=u_{i+1}. C now has a plethora of countable increasing sequences, all of which have to be provided with values of theta_omega. Since this has to be done freely, the value of theta_omega on each sequence (save only for the few that come from sequences in B) must be different from those of all the others, even though all the proper increasing sequence would have the same sup. So this regular image doesn't lie in the subcategory (which means the inclusion doesn't preserve coequalizers, why should it?, and the category doesn't have effective equivalence relations). So provisionally at least, it seems that that ought to be taken as the definition of HSP. It is not hard to show that a full HSP subcategory of a category of models that contains all the free algebras is the whole thing. This is clearly a necessary condition. If such a subcategory doesn't contain the free algebras, then any algebra it doesn't contain gives rise to an equation. For example, in the case at hand, the free algebra generated by a countable chain is uncountable, since it contains one element corresponding to each possible subchain (including ones that are repetitious, even constant) and once the condition of being a sup is imposed, then the value of theta_omega at each eventually constant sequence is set equal to the element in question and the sups of all the not-eventually-constant sequences are identified. So far so good. It looks like one could hope to say that corresponding to an HSP category, you get a quotient theory by imposing either equations or inequalities. The problem is that this doesn't quite lead to a quotient theory. Here's why. A theory is a category with a contravariant functor from the base that is an isomorphism on objects. This means that a quotient theory wouldn't identify any objects. But a quotient category that doesn't identify objects is more-or-less like a quotient among semigroups; in particular it is surjective. But I will show now that HSP categories don't lead to surjectives at the object level. Let F--|U be the free and underlying functor between B and the category E of models. Let E_0 be an HSP subcategory and let I:E_0-->E be the inclusion and L its left adjoint. Then LF--|UI is the adjoint pair between E_0 and B. Let K and K_0 be the Kleisli categories for the triples. These are dual to the theory categories. The functor K-->K_0 is induced by the morphism of triples. K(m,n)=B(m,UFn) and K_0(m,n)= B(m,UILFn) and the induced map is surjective iff the map UFn-->UILFn is split epi, which isn't in the example above. I believe that the map from E-->ILE is surjective in this example, but it is not always the case. To see this consider the theory that has just one 2-ary operation. In other words it has an operation, call it sigma that takes pairs x<y to sigma(x,y). Let us assume the equation sigma(x,x)=x. Then the free algebra generated by x<y has just 3 elements x,y and sigma(x,y). Now add the inequality y<sigma(x,y). now the free algebra generated by x<y is infinite. It contains not only the three elements above, but also sigma(y,sigma(x,y)) and so on. On the other hand, it does determine an HSP subcategory. It is clear that an equational theory cannot be just a quotient theory in a simple-minded sense; yet it does seem to be the insertion of (in)equalities in the right places. So the question that seems to be open is to see in what sense the insertion of these inequalities corresponds to equations. For the converse, going from quotient theories to subcategories, analogous questions arise. If we suppose we have a quotient theory, then the algebras give a subcategory closed not only under strong subobjects, but under all of them. So here too we see that the traditional idea of equational subcategory is not the right one. So what is the right one? Another question that is unrelated (as far as I can see) is what is a sketch in this context? When I said take an operation from omega+1 --> omega, it was clear that I had in mind some idea of sketching theories, not the theory itself. Although Peter Johnstone described the use of sketches as retrograde in a review of TTT (analogous to going back from groups to generators and relations), the fact is that a sketch is frequently finite and a the theory isn't. In fact, many interesting sketches are quite manageably finite and this is important in computing. I think of the difference between sketches and theories as analogous to that between lazy evaluation and (whatever is opposite to lazy, perhaps beaverish). Regards, Michael P.S. All those who object to non-categorical material on the net, please stop reading here. This does not bear on category theory at all (except in a very remote sense of having to do with software verification), but I think it deserves as wide circulation as possible. I got it from my son who found it on a Microsoft BB. I cannot vouch for its accuracy, but it is consistent with whatever information has leaked about the HT fiasco.