lo.logic - Mechanically instantiating abstract constructions

I am looking for work on the effective inverse of abstraction, aka specialization.

There are two ways in which abstraction helps us:

1. Get a better understanding of the structural rules at play in specific situations.


2. Not wasting time re-inventing infrastructure that already exists.

Historically, we have group theory as an extremely successful abstraction of symmetry and permutations. More recently, category theory (CT) has catalogued a huge number of universal constructions that pervade mathematics (and universal algebra before that, and ...). Pedagogically, CT is very useful in sense #1 above.

What I really want is to use the constructions in CT in the sense of #2, but I want to do it as a 'conservative extension' of my base theory. Let me be a bit more precise: suppose I have a theory T using a language L (you can assume higher-order-logic as the background logic if that helps) for which I have identified some categorical structure already. In other words, some objects of T with some morphisms for a category with some 'nice' properties. These properties allow me to pick out some categorical constructions as now being 'available' (from pushouts to coends to Kan extensions, etc, as appropriate). Now, what I really want to do is to enrich the theory T with the results of these categorical constructions, but with all categorical language erased. In other words, I want to retract the construction from CT to T by using L.

For example, given the category Set, one should be able to unwind the definitions (mechanically!) to see that pushouts over the empty set is exactly disjoint union [imagine that disjoint union had not yet been defined!]. Much better examples are given all through Abstract and concrete categories: The joy of cats.

What I really would like to do is to mechanically obtain as many of the examples from The joy of cats as possible. [Yes, I know that what that means is that I need to discharge a lot of proof obligations mechanically as well]. This turns out to be significantly harder than it seems (category theorists don't seem to put a lot of effective algorithms in their papers). So I would like to know what previous work has been done on this, so that I can at least start from there.

EDIT: For example, take this MO question about left adjoints and its nice characterization of when you have a left adjoint for a Functor. With all of that machinery, how can you 'specialize' all of that to the $mathrm{CHaus} rightarrow mathrm{Top}$ case of the given example and 'extract' Stone-Cech compactification? Tom Leinster's answer to the same question is also full of examples of exactly what I am after. As another example, how do I use the Adjoint Functor Theorem so 'extract' an Abelianization procedure from the forgetful Functor from AbGroup to Group, ie how does one get 'construction' given in Andrew Critch's answer to 'drop out' of the abstract-nonsense?