Solid applications of category theory in TCS? I've been learning a few bits of category theory. It certainly is a different way of looking at things. (Very rough summary for those who haven't seen it: category theory gives ways of expressing all kinds of mathematical behavior solely in terms of functional relationships between objects. For example, things like the Cartesian product of two sets are defined completely in terms of how other functions behave with it, not in terms of what elements are members of the set.) 

I have some vague understanding that category theory is useful on the programming languages/logic (the "Theory B") side, and am wondering how much algorithms and complexity ("Theory A") could benefit. It might help me get off the ground though, if I know some solid applications of category theory in Theory B. (I am already implicitly assuming there are no applications in Theory A found so far, but if you have some of those, that's even better for me!) 

By "solid application", I mean:

(1) The application depends so strongly on category theory that it's very difficult to achieve without using the machinery.

(2) The application invokes at least one non-trivial theorem of category theory (e.g. Yoneda's lemma).

It could well be that (1) implies (2), but I want to make sure these are "real" applications. 

While I do have some "Theory B" background, it's been a while, so any de-jargonizing would be much appreciated.

(Depending on what kind of answers I get, I might turn this question into community wiki later. But I really want good applications with good explanations, so it seems a shame not to reward the answerer(s) with something.)
I can think of one instance where category theory was directly "applied" to solve an open problem in programming languages: Thorsten Altenkirch, Peter Dybjer, Martin Hofmann, and Phil Scott, "Normalization by evaluation for typed lambda calculus with coproducts".  From their abstract: "We solve the decision problem for simply typed lambda calculus with strong binary sums, equivalently the word problem for free cartesian closed categories with binary coproducts. Our method is based on the semantical technique known as 'normalization by evaluation' and involves inverting the interpretation of the syntax into a suitable sheaf model and from this extracting appropriate unique normal forms."

In general, though, I think that category theory is not usually applied to prove deep theorems in programming languages (of which there aren't so many), but instead offers a conceptual framework that is often useful (for example in the above, the idea of (pre)sheaf semantics).

An important historical example is Eugenio Moggi's suggestion that the notion of monad (which is basic and ubiquitous in category theory) could be used as part of a semantic explanation of side effects in programming languages (e.g., state, nondeterminism).  This also inspired some reflection on the syntax of programming languages, for example leading directly to the "Monad typeclass" in Haskell (used to encapsulate effects).

More recently (the past decade), this explanation of effects in terms of monads has been revisited from the point of view of the old connection (established by category theorists, in the 60s) between monads and algebraic theories: see Martin Hyland and John Power's, "The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads".  The idea is that the monadic view of effects is compatible with the (in some ways more appealing) algebraic view of effects, wherein effects (e.g., store) can be explained in terms of operations (e.g., "lookup" and "update") and associated equations (e.g., idempotency of update).  There is a recent paper building on this connection by Paul-André Melliès, "Segal condition meets computational effects", which also relies heavily on ideas coming from "higher category theory" (for example the notion of "Yoneda structure" as a way of organizing presheaf semantics).

Another, related class of examples comes from linear logic.  Soon after its introduction by Jean-Yves Girard in the 80s (with an aim of a better understanding of constructive logic), solid connections to category theory were established.  For some explanation of this connection, see John Baez and Mike Stay's, "Physics, Topology, Logic and Computation: A Rosetta Stone".

Finally, this answer would be incomplete without reference to sigfpe's illuminating blog "A Neighborhood of infinity".  In particular you could check out "A Partial Ordering of some Category Theory applied to Haskell".