Well, isn't Gray code doing that?

@SridharRamesh Agreed. I think this is exactly the point of Jem's answer.

@ZhenLin Isn't that always true internally? If $E$ is locally small internal category and $Y \to E$ is a $Y$-indexed collection of objects of $E$, then I can build an internal (small) category which is a full subcategory of $E$ and whose object of objects is $Y$. So internally for any small familly of small category with maps to $E$ I can factor all of them trhough some common small category (so this is "small directed" internally). Or maybe you want to impose this as an external condition?

Oh I see, that make sense too.

Should $\mathbb{E}'$ be $\mathbb{E}^X$, defined by the fact that its fiber over $I$ is the fiber over $I \times X$ for $\mathbb{E}$ (for $X$ some fixed object of the topos)

That is very interesting, I need to think about it a little more, but that does look promising.

I don't know any thing specific. But the Elphant does a lot on fibered/indexed categories in part B. A Stack is a fibered or indexed category that behave well with respects to a Grothendieck topology in the base. Typically, in the case of a base elementary topos you want that $C(A \coprod B ) = C(A) \times C(B)$ and if $f:X \to Y$ is an epimorphism then $C(Y)$ can be expressed as the category of object of $C(X)$ equipped with a "descent data" (similar to the one defined in section C.5).

It doesn't sounds very different from the induction principle of the NNO conceptually though... not sure this makes the problems any simpler.

(But I agree with your point that we do not need the NNO to make sense of the problems)

yes, but you do that internally, so the induction principle you get from finiteness works with regards to other objects of the topos, but "large categories" aren't objects of the topos. So, I agree that what you are saying allows to show that if an internal (small) category $C$ has a terminal object and binary product then it has finite products. But I don't see how to make sense of a "large" (or maybe locally small) category in a way that allows this sort of argument to still work.

I'm note sure I understand what you are saying. That doesn't seem enough to build a product or a coproduct of an "internal" family indexed by a Kuratowsiki finite decidable objects: the stack condition only allows to talk about product and coproduct indexed by external finite familly? it seems we need something more to get the internal finite familly.

I agree with your answer, but I guess my question is, How do you find such suitable categories that contains the basic large categories we want to consider (like the category of sets). For example, I'm not convinced we can find them as full subcategories of the categories of presheaves.

But yes, basically the question is about how to strengthen the definition of locally internal category. I'm not exactly sure how to do that.

I agree it feel related to replacement, but I'm not sure it is. I don't think I need replacement to prove that categories with binary product have finite product