In ETCS, how do we take the limit of an infinite diagram? As everyone knows, the category $\mathrm{Set}$ is complete, or in other words all small limits exist.
Now suppose we're using ETCS as a foundation. I think we can take finite limits without issue. But, how do we define the limit of a diagram with (small but) infinite scheme? Indeed, how do we even define an infinite diagram?
I'm especially interested in the uncountable case.
 A: If you're taking ETCS as a foundation, then externally, all you have to construct diagrams is what you can do in the language of first-order logic, and so the only (meta-)diagrams you can draw are finite, so there is no problem.
What you need is an internal notion of diagram, and then we can ask about taking limits and colimits of those.
The brief outline as I understand it is:


*

*Define internal categories. This is directly analogous to the usual definition of small category as a set of objects, a set of morphisms, et cetera. But since "set" now means "object of my topos" and so forth, this turns into the usual definition of internal category.

*For an internal category $J$, define internal functors $J \to \mathbf{Set}$. This is a trickier problem than defining a functor between two internal categories. The right approach is to use the equivalence between set-valued functors and category actions on a set. An internal functor is then defined to be an object of $\mathbf{Set}$ together with an action of $J$ on that object.

*Define the notions of limit and colimit for internal diagrams. This can be done externally by constructing the (meta)category $\mathbf{Set}^J$ of internal functors, and defining limits and colimits as the right and left adjoints to the diagonal $\mathbf{Set} \to \mathbf{Set}^J$.
