Dear Bob: After thinking about Vaughn's letter some more, I realized that that is not how I would have been tempted to make a Pos theory. In two respects. First, I would not have used contravariant operations. Second, I would not have stuck to discrete exponents. Let me take up the second point first. Surely you would like to be able to have an algebra that had operations whose domain { (x,y) | x < y }, which means you want an operation of arity 2 = .-->. . For example, you want to be able to have countably CPO's as axiomatized by an operation of arity \omega, which means that the operation is defined on countable increasing sequences. Suitable axioms will guarantee that it is a countably CPO. As for the first point, this bothered me. The way Vaughn has it, you lose the ability to apply the Yoneda lemma, one leg of the categorist's holy trinity (the other two being adjoint functors and representable functors; they are all essentially equivalent concepts, but one or the other looks more fundamental, depending on the context). In this setup, these functors will be representable and the Yoneda lemma is available. At first I thought I would have to make a poset-enriched version of Yoneda (which would certainly be no problem), but eventually I realized that that is not quite the way to go. In fact, this is the setup. Let V:Pos --> Set be the underlying functor on the category of posets. A poset enriched theory (or, more properly, sketch) consists of n-ary operations for each poset n, along with equations and poset-based Horn clauses. A model is a poset X equipped with a function V(n --o X) --> VX for each n-ary operation in the sketch. The point of the V is that I make no hypothesis that these functions either preserve or reverse or have any interaction with the order. So no mental gymnastics with the symmetric difference or other mixed operations. The point is that, as Vaughn's examples show, the operations do not naturally preserve the order. Or reverse it. I am reasonably confident that I could dream up a theory in which there was no way of decomposing the operations so that they can be made up from mixed variance operations in the way that Vaughn did it. Now let B be the category of models. We have U:B --> Pos and it has a left adjoint F. There is a downside to all this. Vaughn asked for an HSP theorem and I gave one for his theory. It crucially depended on the fact that powers and the op functor preserved those epimorphisms in Pos (surjections). Well, non-discrete exponentiation doesn't preserve exponentiation. In fact, it is more-or-less obvious that only split epis are preserved by arbitrary exponentiation. So now what? Over sets, the crucial step in showing that theories and triples are (ignoring certain size questions that I will keep under the rug for the moment; they have no effect on the kinds of theories that will interest computer scientists and I am perfectly to restrict to countably based sketches and \aleph_1 accessible triples) equivalent is that the natural transformations from U^n to U are in one-one correspondence with UFn. It is not hard to prove that the set of natural transformations from U^n to U is equivalent to VUn and from there to show that if that set of natural transformations is given the obvious order: \alpha < \beta if for all f:n\to UB, \alpha B(f) < \beta B(f), then that set of natural transformations is order isomorphic to UFn. From this, I think the equivalence between theories and triples will follow. However, there is a downside to all this. Surjections are not split and therefore are not preserved by triples. This being crucial to the argument about HSP subcategories, that would seem to go down the drain as well. There are some possbilities, which I will discuss shortly, but I don't believe any simple recovery is possible. First an example. Suppose we consider a theory with just one operation of arity 3, meaning .-->.-->. This means a value I will call <x,y,z> defined whenever x < y < z. Put in the following: z < <x,y,z> and <x,x,z> = <y,z,z> = z. Then there is an algebra whose underlying poset is 2 + 2, that is the disjoint union of two arrows. The values of this operation are forced. In fact, this is the free algebra on 2 + 2. If we now identify the head of one arrow with the tail of the other, then there are now three distinct x < y < z. Thus we get elements <x,y,z> which is now strictly greater than z, as well as <y,x,<x,y,z>> and <z,<x,y,z>,<y,z,<x,y,z>>>,..., not to mention <x,z,<x,y,z>> and many others. Thus the coequalizer of that identification is infinite. This shows that images are not always very simple. Now here is what you can do. I feel more comfortable with triples. Suppose that B is a category of algebras and C is a full subcategory and let us suppose it is reflective. If we suppose at least that C is closed under U contractible quotients, then the composite is tripleable. This means that whenever X -->> Y is an arrow, split as posets and X is in C, then so is Y. Call the triple S. Then we have T --> S a map of triples. There is (of course) a category of triples and in that category, there is a factorization T -->> R >--> S where the first is a strict epi and the second monic. The real question is to what extent can T -->> R be viewed as the introduction of equations. I don't know at this point, but I don't expect there to be any easy connection. Of course, if T -->> R is actually surjective, then it can be viewed as the introduction of equations. The trouble is that there might be new operations forced by the identifications. In fact, the example above, although it takes place at the level of models, not theories, gives an example how this happens. Still, the new operations are a result of an identification that was made (or perhaps of a new ordering introduced), so this may still give a kind of HSP theorem. But to illustrate the kind of thing that will have to be taken into account, consider that T --->> R is an epimorphism in the category of triples. Unless it is an epimorphism in the functor category, one cannot even infer that a T algebra that is a subobject of an S algebra is an S algebra. This is the S of the HSP theorem. I don't see any obvious way around this. Regards, Mike