Lambda the Ultimate

Um... there are entire fields of mathematics inspired by following categorical intuitions. One particular method at arriving at such is to look at a category of existing things, e.g. the category of topological spaces, and note that it fails to be cartesian closed, as indeed the category of topological spaces does fail to be, and consider what needs to be changed to make it cartesian closed. The result is the source of many "synthetic" areas of mathematics such as synthetic topology, synthetic domain theory, synthetic differential geometry. As far as I know, coalgebra as a coherent field is completely due to category theory. Certainly, there were fore-runners, such as automata theory, but mathematics has mostly hidden its coalgebraic structures. Category theory has had a significant impact and has been a significant guiding force in type theory, proof theory, logic, and the semantics of programming languages. Category theory has, unsurprisingly, had a significant impact on algebraic topology, the field in which it arose. Category theory mostly destroyed universal algebra. I'm not sure on the history, but if not begun in category theory, sheaf theory, sheaf cohomology, topos theory, and the theory of schemes were dramatically impacted by category theory early in their lives and are what they are today due to category theory. This isn't even mentioning incestuous things like the theory of operads.

I don't know much synthetic topology (or synthetic differential geometry, or synthetic domain theory). However, from your description it sounds as if these examples are even better than what I hoped: not only do the categorical notions uncover hidden concepts, but they warn us that we might be heading in the wrong direction.

So, in the synthetic case, what I am looking for is a non-categorical justification for the synthetic fields. What advantage comes out of replacing the traditional theories with the synthetic ones? Does it benefit the instances that also fit the non-synthetic theory?

The coalgebraic structures seem to fit exactly my original question. However, I am unsure about the other examples that you gave. Category theory has unarguably helped to generalise and unify semantics, logic, type theory, algebraic topology, universal algebra, sheaves and topoi. But I am not sure whether they were useful in uncovering new concepts in the way described above: Instantiate a categorically important concept and discover a new, central, concept to the theory at hand.

So, in the synthetic case, what I am looking for is a non-categorical justification for the synthetic fields. What advantage comes out of replacing the traditional theories with the synthetic ones?
I can't speak to synthetic theories in general, but synthetic differential geometry has distinct non-categorical benefits. The most immediate is that it provides a theory of calculus where the major theorems can be proved through simple algebra (and nilpotent infinitesimals) rather than limits.

More generally the benefits of seeking cartesian closure for your category of smooth spaces create a more naturally cohesive theory. For example, in classical differential geometry one can have intuitive notions of a vector field an a manifold as a section of the tangent bundle, or as an infinitesimal flow across the manifold, or even as an infinitesimal element of the automorphism group of the manifold. The important thing is that, at least in the classical theory, these are (aside from the first) intuitions or analogies, and certainly any equivalence between the three different notions would be painfully hard to prove. In the synthetic theory, in part due to the cartesian closedness, these notions become formal, rather than mere intuitions, and moreover their equivalence is proved simply via lamda abstraction.

Thanks too! It seems to me that these categorical concepts have applications in modeling/verifying concurrency formally. I've found this compendium "Semantics of Concurrent Systems - Foundations and Applications" from 1996. Quoting:

"Temporal logic and the theory of Galois connections are two gems of theoretical computer science which are rarely, if ever, mentioned together"

Any more modern references, anyone?

Linking theories of concurrency (2005) by Jifeng and CAR Hoare is a nice example:

We construct a Galois connection between the theories that underlie CCS and CSP.

From the linked page:

Abstract:

the governments of the People’s Republic of China and Portugal through a contribution to the UNU Endownment Fund. As well as providing two-thirds of the endownment fund, the Macau authorities also supply UNU-IIST with its office premises and furniture and subsidise fellow accommodation. The mission of UNU-IIST is to assist developing countries in the application and development of software technology...

It's an error: the article is from the United Nations University (the first author from the Software Engineering Institute of East China Normal University and Citeseer miscopied the abstract:

We construct a Galois connection between the theories that underlie CCS [7] and CSP [4]. It projects the complete transition system for CCS onto exactly the subset that satisfies the healthiness conditions of CSP. The construction applies to several varieties of both calculi: CCS with strong, weak or barbed simulation, and CSP with trace refinement or failures refinement, or failures/divergence. We suggest the challenge of linking other theories of concurrency by Galois connection

Edit: I submitted a correction to Citeseer. Thanks.