Say that a setoid is trivial if the equivalence classes are all singletons. The full subcategory of trivial setoids is isomorphic to the category of sets (and this time the isomorphism works constructively).

Note that image factorisation is different in trivial setoids and setoids. Suppose we have some morphism of trivial setoids f: (X, ~) -> (Y, ~) (since these are trivial setoids this is just any map X -> Y). For the image factorisation in setoids, we take the underlying set of im(f) to be X, but change the equivalence relation, to ~' defined by x ~' x' whenever f(x) = f(x'). On the other hand the image factorisation in trivial setoids is the quotient X/~' together with the trivial equivalence relation. Assuming choice these will be isomorphic. However, the key point is that in general the converse also holds, so by working internally in a model of set theory where AC fails, we can get examples where the image factorisations are not isomorphic (ie where the inclusion of subcategory functor does not preserve image factorisation).

On the other hand, the rest of the type theoretic structure is preserved by the inclusion functor. Dependent products, finite limits and disjoint sums are all the same in trivial setoids and setoids.

We now assume that we have an inaccessible set, stated using a suitable constructive notion of inaccessible. We define a universe U_1 -> U_0 by taking U_0 to be the set of all small trivial setoids, and an element of U_1 is a small trivial setoid together with one of its elements. Take the equivalence relation on U_1 and U_2 to just be trivial. The small maps f: X -> Y are then those which are both small in the usual sense (fibres are isomorphic to elements of the inaccessible set), and also admit a function f': X -> Y which makes a pullback square with f and the quotient maps. Note that if Y is trivial and f: X -> Y is small then X is also trivial. We can also consider another larger universe V_1 -> V_0 which consists of all small setoids.

If we interpret type theory in the above category we can almost, but not quite answer question (4). We work internally in the Lifschitz realizability model like in Chen, Rathjen, Lifschitz realizability for intuitionistic Zermelo–Fraenkel set theory. In type theory we work over the context consisting of binary sequences a: N -> 2 which are 1 at most once, and we consider the propositions P(a) = forall n. a(2n) = 0 and Q(a) = forall n. a(2n + 1) = 0. Call this context A. Then LLPO is the statement that for all a in A, the proposition P(a) \/ Q(a) is true (when disjunction exists at all). If the disjunction ||P \/ Q|| exists, then we would have maps of the form P + Q -> || P + Q || -> A in the model. If || P + Q || belongs to the universe U, then the map || P + Q || -> A would be small, which would make the setoid || P + Q || trivial, and in particular it has to be just a subset of A. On the other hand, if this is still the disjunction of P and Q when we move up to the larger universe V, then it has to be isomorphic to the "real" image factorisation in setoids, which consists of pairs (i, a) where either i = 0 and P(a) holds or i = 1 and Q(a) holds, together with the equivalence relation that identifies (0, a) and (1, a) when both occur in the set. If this was isomorphic to a monomorphism, then, assuming LLPO, we would have a choice function, that selects for each a in A, a choice of i such that i = 0 and P(a) or i = 1 and Q(a). However this is impossible in Lifschitz realizability.

I think it's possible to get a complete answer to question (4) by instead working with the arrow category of setoids, and then interpreting the universe as the inclusion of U into V.