I don't know, since I don't understand these issues sufficiently well, but if you can define the free abelian group cotriple, you can then define the coalgebra category for that cotriple and that is the category of sets. Peter Freyd succinctly shows you can't with The category of co-groups in Ab is equivalent to Ab. Interesting that Peter used duality to prove it, since my reason for strongly believing it was also duality-based. The general principle I used for my reasoning was that the only categories "definable" in the internal logic of a self-dual category are full subcategories of it. FinAb is self-dual, but FinSet does not fully embed in FinAb. If only I knew what "definable" meant this would be a proof. I came to appreciate this principle while investigating Chu(Set,K). All notions of "definable" I understand (e.g. first order definable) are subsumed by this principle. However that's not sufficient reason to call it a theorem, since someone may have a method of definition I don't know about that violates it. For example I have not yet figured out whether the method of sketches violates it, though I can't imagine how it could. In fact, that is a ! operation, in Girard's sense, on the fragment of linear logic that Ab satisfies. (This last was an observation of Jim Otto's.) Is Jim's statement even well-defined? ! is a functor projecting LL onto a cartesian closed full subcategory of itself. For the above to make sense you would need a full embedding of the coalgebra category, namely Set, back into Ab. But unless I'm dreadfully confused (which I often am) there isn't such. What could a set reasonably be other than the free abelian group on it? But when you're inside Ab, Ab(G,H) = H for H a fag, so that's not it. Similar deal with Rel or CSLat. I was dreadfully confused about this in 1991 when I first got involved with duality via CSLat and their sibling Event spaces. I wish someone had pointed out to me that my ! *didn't* produce a cartesian closed category as I was claiming. Instead I had a long period of waiting for my vision problems to clear up. Adding ! to LL stretches LL out a lot, much wider than Ab with respect to the Stone gamut (the Set<->Set\op axis). Enough in fact to make it look rather like Chu(Set,K) for indefinite K, less such amenities as induction and such obscurities as 1 par 1 |- 1 (noticed by Lafont and Streicher---with its contrapositive _|_ |- _|_ @ _|_, the two objects 1 par 1 and _|_ become sort of the "two halves" of a single coalgebra in Chu(Set,K)). You just have to take the bad with the good when you have a nice model like Chu(Set,K). I've incorporated my proof that Set is a bicomplete equational topos (meaning one with all natural isos identities) into my LL'96 paper, "Linear Logic complements Classical Logic," sent off last night. In the light of Peter Johnstone's remarks it seemed prudent to add an explanatory paragraph as a sort of talisman against the nonmonotonic logic of antiChoice fundamentalism extolled on Sundays. This is now available as ftp://boole.stanford.edu/pub/llcocl.ps.gz, with tex and dvi counterparts in the usual subdirectories, /pub/TEX and /pub/DVI. I'll post the abstract here shortly, or look it up yourself in the file ABSTRACTS in the same directory. This is paper 45 in that directory, getting time to compress its scattered ideas down a bit. Vaughan Pratt