# 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?

• I#ve read your question many times, but still I didn't get it. Can you provide more examples? – Martin Brandenburg Apr 8 '10 at 22:23
• I can give you an analogy for now, more examples later: I want to do specialize categorical constructions in the same way I did for the generic algorithm 'GaussianElimination' in cas.mcmaster.ca/~carette/publications/scp_metamonads.pdf (official version at dx.doi.org/10.1016/j.scico.2008.09.008). There are tens of thousands of variations (along 21 "dimensions" of design choices) for GE -- but only 1 algorithm, and this is fully constructive. – Jacques Carette Apr 8 '10 at 23:04
• hm your edit clarifies it a little bit. are you looking for examples how to specify an object which exists by abstract nonsense, without actually doing the construction again? if yes, I can give many examples ... – Martin Brandenburg Apr 9 '10 at 2:28
• I am looking for a methodology (so I can automate it) of constructing objects which exist by abstract nonsense, by 'unwinding' the abstract construction. From there, I should be able to generate many examples myself. – Jacques Carette Apr 9 '10 at 3:01

I don't know if this answers your question, but here's how I would think about it. Work in a dependent type theory, and suppose we've defined a type of categories, $\mathrm{Cat}$. Suppose we've proved some theorem about categories, $\mathit{Thm}$, with proof term $p\colon\forall C\colon\mathrm{Cat},\mathit{Thm}(C)$. An example of the phenomenon in question would then be to specialize this theorem to a specific category, or to a specialized class of categories. Say we want to specialize to monoids. Then we might have a type of monoids, $\mathrm{Mon}$, and a function $\alpha\colon\mathrm{Mon}\to\mathrm{Cat}$ constructing for every monoid the corresponding one-object category. Then we can specialize $\mathit{Thm}$ to get a new theorem, $\forall M\colon\mathrm{Mon},\mathit{Thm}(\alpha M)$, with proof term $\lambda M\colon\mathrm{Mon}, p(\alpha M)$.
Another way to look at this, it that having a theorem in some context $\Gamma$ corresponds to a display map in the context category, $(\Gamma, p\colon T)\to\Gamma$. Specializing to another context, $\Delta$, is given by a morphism of contexts $\alpha\colon\Delta\to\Gamma$. Pulling back along $\alpha$ gives you a display map over $\Delta$ with your specialized theorem (obtained by substituting according to $\alpha$).