Mike Shulman asked:
Suppose I have a well-founded poset W, regarded as a category, and I would like to define a functor W -> C into some other category by well-founded recursion. Is there written out anywhere in the literature a general schema for doing this? It's a little more subtle than defining an ordinary function by well-founded recursion, since we have to define the value of the functor on morphisms too, and its value at a given object may depend on its value at morphisms between previous objects.
The simple answer is that the recursion has to define the functor, ie the morphisms corresponding to instances of the order relation, and not just the values at individual ordinals, in order to make sense of defining the values at limit ordinals as colimits. I suspect, however, that Mike is looking for a more sophisticated answer than this. (The particular reason why I suspect this is that he solved the problem of how to define Conway numbers without using excluding middle at every level, in the final chapter of the Homotopy Type Theory book. Although he apparently discovered this independently, his solution turned out to be the two-sided analogue of my notion of "plumpness" for intuitionistic ordinals.) The well founded recursion is a routine matter if the categories W and C in Mike's notation are small ones, ie structures within some ambient universe. However, if C is Set or any other familiar large category, even if W is small, we have to invoke some part of the Axiom-Scheme of Replacement. For example, if W=omega and the values are the interated powersets P^n(N) then we cannot form the colimit of the diagram (or turn the diagram itself into a fibration) in an arbitrary elementary topos. This is because, in set theory, the result is the cardinal aleph_omega and its members form an elementary topos. In the mid 1990s I investigated not only intuitionistic ordinals in a quasi-set theoretic style but also a categorical one. The results are summarised in sections 6.3, 6.7 and 9.6 of my book, "Practical Foundations of Mathematics". Gerhard Osius showed how one can regard a "set" (epsilon-structure) as a coalgebra in a topos for the covariant powerset functor. This structure is extensional if the coalgebra structure map is mono. The definition of a "well founded coalgebra" is given in my book. One can also apply the same ideas in other categories, varying the notion of "mono". Several kinds of intuitionistic ordinals are obtained by doing this in the category of posets, with the lattice-of-lower-subsets functor in place of the powerset. This leads to a purely categorical way of defining transfinite iterates F^alpha of a functor F and of expressing the Axiom-Scheme of Replacement. First, we can encode an ordinal-indexed family of objects, along with morphisms for the order, by a fibration (internal to the ambient topos). Then by standard fibrational methods we can apply the functor F to the family. Again by standard methods we can compute the colimit of F^beta over the "elements" beta of alpha that are specified by the structure map of the coalgebra. Such an internal fibration is the family of iterates of the functor iff a certain square is a pullback. The relevant diagram is in the final pages of the text of my book. Beware that this is a characterisation not a construction. We may take the existence of such pullback diagrams as a purely categorical formulation of (part of) the Axiom-Scheme of Replacement. Note also that pullbacks of this kind then form a reflective subcategory of a category composed of squares. We therefore have examples of subcategories that are closed under all available limits but only have reflectors if Replacement holds. Unfortunately, not only is the summary in my book the only published account of these ideas, but I do not really have any more coherent private notes. I had hoped that this work might contribute to a categorical debate about Replacement, but that went off in other directions without me. Paul Taylor [For admin and other information see: http://www.mta.ca/~cat-dist/ ]