Actually, my question is much more basic. On Wed, Jul 9, 2014 at 2:39 AM, Paul Taylor <cats@paultaylor.eu> wrote:
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.
That's exactly what I said:
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.
All I'm looking for is a general theorem of the form "given a well-founded relation < on a set X, and a category C, and such-and-such data, there is an induced functor X -> C." I don't care about set-theoretic issues right now, I'm just looking for a place where someone has written out exactly how to construct such a functor using the well-foundedness of <. It seems like it should be a well-known thing, so that I can just cite it rather than having to write out my own proof. Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ]