A couple of preliminary thoughts on Vaughn's communication. First, the whole business about symmetric difference was not well considered. Symmetric difference is a binary operation and calling it a quaternary operation doesn't make it one (cf. A. Lincoln). Of course, there is a quaternary, or more properly a (2,2)-ary operation that takes (x,y,z,w) to z.x- + w.y- and that can be specialized to give symmetric difference, but it isn't symmetric difference. If you want symmetric difference, it can also be defined from the operations of +, ., and -. In either case it is a derived operation, not a primitive one. This is not an important point, just to set the record straight. I have no knowledge on question I. As for II, I have some thoughts, at least on II i. First off the answer cannot be that an HSP subcategory is described by equations. This is already clear from the HSP subcategory of the theory of one binary (that's (0,2)-ary to be precise) operation +. Don't suppose it is associative or commutative. The Horn clause x < y => x+y = y defines an HSP subcategory. I don't think that, lacking associativity and commutativity, you can get that subcategory equationally. Even with them, I'm not sure you can, although you could get x+y<y from y+y=y. No, I haven't proved this, it just seems likely to me that these claims are true. Does that mean that HSP corresponds to Horn clauses. Well yes, but only Horn clauses that are stateable in the theory of posets. An equation is a Horn clause in the theory of sets. Of course the theory of sets has only one predicate, that of equality. (Membership doesn't count here because we don't use over subsets.) So an equation like x.x*=1 is the same as the Horn clause y=x* => xy=1. In a similar way, the theory of posets has only the predicates of = and <. (By the way, it is clear that Vaughn used < for less than or equal and I follow him in that usage.) I claim (or conjecture, if you prefer, but it is pretty clear) that HSP subcategories correspond to the Horn clauses that can be stated using only the predicates = and <. The reason is that if Pos is the theory of posets and if B is the category of models of one of these poset theories, then the underlying functor U:B--->Pos has an adjoint F (and in fact is tripleable). If C is an HSP (full) subcategory of B, then it is immediate that if C includes all the free algebras (that is F(Pos)), then B=C. Thus if B isn't C, there is some poset X such that F(X) isn't in C. Now C is reflective (trivial) so there is a free C algebra generated by X and it is a quotient of F(X). I am pretending that all these theories are finitary, although the infinitary generalization would probably offer no real difficulty. Suppose that X consists of elements x_1,...,x_n and some order relations such as x_i < x_j. Now there will be two terms t(x_1,...,x_n) and s(x_1,...,x_n) which are distinct in F(X), but not in its reflection in C. Or perhaps they are unrelated in F(X) but s < t in the C-reflection. This will give you Horn clauses of the sort x_i < x_j, ..., => s = t or x_i < x_j, ..., => s < t in the predicates available in Pos. The left hand sides are simply a listing of all the order relations in X. Or at least a generating family of such. In order to prove this, you must investigate the nature of quotients. However, unlike in Cat, they are surjective and are of the two types alluded to in the argument above. I don't fully understand II ii, but I think the above bears on that question too. There are obvious generalizations of this to bases other than Pos; I guess that is evident. It is a matter of taste, but I would prefer to leave the predicate of equality in rather than derive it from <. Cheers, Mike