The question is basically "do we really have a good way to talk about large categories internally in an elementary topos"?

An internal small category in a topos $E$ is just a category object in $E$.

Until now I assumed that when we want to talk about a "large" categories internally in an elementary topos $E$ we would use a stack for some appropriately chosen topology on $E$. This seems to be the commonly held point of view in every text that deal with this.

If $E$ is a Grothendieck topos, we can use the canonical topology and this works very well, which is why I never really questioned this. But for an elementary topos, using the coherent topology works decently well, but we run into a big problem with how it interact with notion like finiteness:

For a small internal category $C \in Cat(E)$ I can show "by induction" that (internally) if $C$ has a terminal object and binary products then it has finite products. Where by finite products I mean products indexed by any (Kuratowski) finite decidable object.

But if $C$ is a large category, it seems very unclear that one can do the same thing! (or if you know how to do it, that would answer my question!)

Keep in mind that an elementary topos can have non-standard finite objects, that aren't (locally) finite coproducts of the terminal object. So these internally finite limits aren't really externally finite and something that is just a Stack for the coherent topology has I think no reason to have then?

Of course, it is possible to show this sort of things for concretely defined large internal categories, like "the category of sets" or a "category of sheaves on an internal site", but don't know how to give a good definition of an "internal large category" that allows to prove this sort of results ( basically being able to use induction when construction objects of the topos).

Can we come up with a good notion of "internal large category" in an elementary topos $E$ (maybe as a stack on $E$ satisfying some additional condition) that:

• include the usual example, like the categories of set, groups, fields, sheaves, etc...

• can be manipulated internally like a (large) category would - for example the Elephant is supposed to mostly do thing that are internally valid, but it uses large categories in many places, I'd like to be able to be able to convince myself that this notion would allow to properly internalize all this.

• We can prove result like "if a category has binary products and a terminal objects then it has finite products".

For example, in set theoretic foundation that doesn't seem to be a problem: if one defines classes as formulas, then we can still construct objects and morphisms by induction without problems.