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?

  • 1
    $\begingroup$ I#ve read your question many times, but still I didn't get it. Can you provide more examples? $\endgroup$ Apr 8, 2010 at 22:23
  • $\begingroup$ 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. $\endgroup$ Apr 8, 2010 at 23:04
  • $\begingroup$ 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 ... $\endgroup$ Apr 9, 2010 at 2:28
  • $\begingroup$ 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. $\endgroup$ Apr 9, 2010 at 3:01

1 Answer 1


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$).

In any case, the specialization procedure is mechanical, given by some sort of substitution, but then the question arises as to how to best simplify and present the result. Say you've specialized the proposition that every split epimorphism in a category is, in fact, an epimorphism. Specializing to monoids states this result in the language of monoids, but maybe you want afterwards to search for definitions and restate the proposition to be that every monoid element with a right inverse is right cancellable. This was just a simple example, but in general there may of course be many possible simplifications of the specialized terms. You could normalize, but the normalization is rarely the most simple form, especially if everything takes place in a non-empty background context.

  • $\begingroup$ Right, that was exactly what I was thinking about. And the crux of the problem really is as you state it in your last paragraph: once you have a specialized theorem, how do you 'present' it in a (relatively) simplified manner in the language of the theory. Your second paragraph introduces something new to me (display map) which I'll have to look up. $\endgroup$ Apr 10, 2010 at 13:35

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.