closure under colimits

Stream: maths

[Reid Barton]

Suppose C is a category.{u v} that has_colimits and I have a family A_i of objects of C indexed by a Type v. I also have (let's say for simplicity) a fixed J which is a small_category.{v}. I want to construct the closure of the objects A_i under colimits of shape J, as a new family also indexed on a Type v. Is it possible?

[Reid Barton]

I was going to use an inductive type of course, but in order to write down the data needed in the inductive constructor, I also need to know what the actual objects in C are (that is, the values of the indexed family), because a diagram involves morphisms in C between those objects. So I end up with an inductive-recursive definition.

[Reid Barton]

I thought about adding the value of the object as an index of the type, but then it won't live in the right universe.

[Reid Barton]

The only thing I can think of is to do some manual transfinite recursion up to an ordinal of large enough cofinality (I know... that's my solution to everything).