Shape of axioms in algebraic structures When defining algebraic structures (like monoids, groups, etc...), are there some constraints on the shape of the axioms, for the structure to have good properties that we implicitly use in many proofs (like behaving well with respect to morphisms and quotients)?
For instance, is the following axiom acceptable, in a structure equipped with a unary function $f$ and a binary operator $\circ$:
$$\forall x, \text{ if }x\circ x=x\text{ then } f(x)=x.$$
More specifically, does it make sense to study varieties generated by (subclasses of) such classes of objects, even if the class of structures so defined is not a variety, since this axiom is not an equation?
 A: x = "preservation".
Usually one is motivated to study a structure because it
serves as a model for something of interest.  Likewise a
certain statement or class of statements may have nice
consequences for its class of models.  It is uncommon
to say 'I want to build this structure, but only if I can
characterize it with regular identities or in iambic
pentameter."  Preservation theorems are the family
of theorems that relate the shape of a characterizing
language/theory to the shape of the constructions 
preserved.
If you need a special kind of suit to dress up a class
of models  of which your structure is a member,
you may not get a precise fit: some members of the
class are excluded, or perhaps some additional members
are included.  Whether this is desirable depends on the
party for which one is dressing up.
The short answer is : it depends.  If you are looking
at alternative axiomatizations for your class, then why?
Do you need a term rewriting system to work on it?
Is recursive axiomatizability sufficient?  Do you need
a mixed presentation of a second order axiom and
one or two modifying first order axioms?  Are you
trying to fit your class in some poset of defined classes?
Shape does matter.  I can't tell you why before you tell
me enough motivation.
A: This is what is known as an equational Horn clause.  It is an implication between two equations.  It is a special case of what is called a near equational theory, which is one with operations and partial operations, the latter having domains given by equations using the ordinary (total) operations, plus equations involving the partial and total operations.  There is an apparent generalization in which you allow partial operations whose domains are given by equations involving partial operations, but it turns out not to be more general.
A good example is the category of (small) categories in which the domain of the composition operation is given equationally in terms of the total operations of domain and codomain.  This is discussed in detail in ``Category Theory for Computing Science'', available free at http://www.math.mcgill.ca/triples/Barr-Wells-ctcs.pdf.
