Re: functors defined by well-founded induction

[Michael Shulman <shulman@sandiego.edu>]

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/ ]