I appreciate that there are people on the list with more years of experience with abelian categories than I have days. AC's don't seem to have penetrated much into computer science, and I have no idea whether they need to. But the finite axiomatizability of the quasivariety generated by Set and Ab definitely has my attention. And the fact that toposes and abelian categories, so far apart intuitively (sets vs. abelian groups?), are brought to within so short an axiom of each other by the definition of AT cats, has the potential to make abelian categories much more relevant to fans of toposes. Peter (and privately Fred Linton and Mike Barr) have answered my question about what I was naively calling "abelian closed". "Abelian" and "cartesian" are not interchangeable adjectives inasmuch as the latter describes the tensor product in the context of "cartesian closed" while the former names a quasivariety. While I was aware of the distinction, I was hoping that abelian categories as the models of the universal Horn theory of Ab, combined with Ab having closed structure, would somehow make the juxtaposition "abelian closed" meaningful, but the examples show this to be wishful thinking. And Peter's define TX as the image of rX removes any motivation to define TX as 1@X. (Meanwhile I've reconciled myself to TX as the pushout of the projections of 0xX.)
After saying that it's a regular category with a coterminator contained ^^^^^^^ [Is "effective" not needed? -v] in its terminator, I'd start with the P-E-l-r-/\ structure as in my last post, and prove it to be the correflection of X into the full subcategory of type-T objects. 0xX -> X is easily seen to be the correflection of X into the full subcategory of type-A objects. Then the axiom that these two correflections yield a coproduct decomposition for each object allows one to prove quickly that the category is the cartesian product of the two correfletive subcategories. The type-T objects clearly form a topos. All that's needed now is a couple of axioms to make the type-A objects abelian.
Not just finitely axiomatizable but beautifully so. Vaughan