In fact, the condition can be weakened into these versions as in the forum post:
https://nforum.ncatlab.org/discussion/560/codomain-stacks/
Is there any proof of this fact (or some proofs that can be easily modified into a proof of this)?
I would be happy if someone can directly refer to a textbook. But if there is not any, many thanks for writing out a proof or a sketch!
Thanks!
Let us fix an elementary topos $\mathscr S$. We start with a type $\vdash J:Type$ in the empty context and a bunch of types $j:J\vdash I_\alpha(j) : Type$ above $J$. This is in essence the same thing as an object $().J$ in the base category $\mathscr S$ plus a bunch of maps $p_\alpha: ().J.I_\alpha \to ().J$ into that object. The $p_\alpha$ are the display maps of the dependent types $I_\alpha$. The best exposition of the precise categorical semantic I am aware of is Martin Hofmann's text On the interpretation of type theory in locally cartesian closed categories. I will take all that for granted and just move on (because it is to much for a stackexchange post).
I denote the self-indexing $\partial_1:\mathscr S^\mathbf 2\to \mathscr S$ by $\mathbb S$. Let us define a category $Desc((I_\alpha)_\alpha,\mathbb S)$ of descent data. An object in the category of descent data consists of a family of dependent types$$j:J,i:I_\alpha(j)\vdash X_\alpha(j,i):Type$$ together with isomorphisms $$j:J,i_1:I_\alpha(j),i_2:I_\beta(j)\vdash \theta_{\alpha \beta}(j,i_1,i_2):X_\alpha(j,i_1)\to X_\beta(j,i_2)$$ which satisfy the cocycle condition. The cocycle condition states that for each triple $\alpha,\beta,\gamma$ of indices we have that the following subsingelton type is inhabited (our equality is extensional). $$j:J,i_1:I_\alpha(j),i_2:I_\beta(j),i_3:I_\gamma(j)\vdash \theta_{\beta\gamma}(j,i_2,i_3)\circ\theta_{\alpha \beta}(j,i_1,i_2)=\theta_{\alpha\gamma}(j,i_1,i_3)$$
A morphism of descent data $(X_\alpha, \theta_{\alpha\beta})\to (X'_\alpha,\theta'_{\alpha\beta})$ consists of terms $j:J,i:I_\alpha(j)\vdash f_\alpha(j,i):X_\alpha(j,i)\to X'_\alpha(j,i)$ which are compatible with the structure isomorphisms. There is a restriction functor $$Fib_\mathscr S(().J,\mathbb S)\to Desc((I_\alpha)_\alpha,\mathbb S)$$ where $Fib_\mathscr S(().J,\mathbb S)$ is the category of types $j:J\vdash X(j):Type$ depending on $().J$. The restriction functor just weakens along the display maps, the structure isomorphisms are identities. We say that the codomain fibration satisfies descent with respect to the family $(I_\alpha)_\alpha$ of sets depending on $().J$ when the functor is fully faithful. It satisfies effective descent when the functor is an equivalence.
I will now show that $\mathbb S$ is a prestack in the coherent topology. The covers consists of finite families of maps which are jointly epi. We may thus assume that the $\alpha$ range over an external finite set and that the display maps cover $().J$. In the internal language this means that we may assume that $$\forall j:J.\bigvee_\alpha (\exists i:I_\alpha(j))$$ is valid, i.e. that from the internal perspective at least one of the $I_\alpha(j)$ is always inhabited. So assume we have two maps $j:J\vdash f(j),g(j): X(j)\to Y(j)$ which yield the same morphisms of descent data after we restricted them. This means that the following subsingelton type is inhabited for each $\alpha$. $$j:J,i:I_\alpha(j)\vdash f(j) = g(j)$$ In other words it holds that $\forall j:J.\forall i:I_\alpha(j).f(j) = g(j)$ is true for each $\alpha$. Now combining this with $\forall j:J.\bigvee_\alpha (\exists i:I_\alpha (j))$ and a bit of intuitionistic logic shows us that $\forall j:J.f(j) = g(j)$ is also valid. In other words we have show that the restriction functor to descent data is faithful. To show that it is full, assume we start with two dependent types $j:J\vdash X(j),Y(j):Type$. Assume that we have terms $j:J,i:I_\alpha(j)\vdash f_\alpha(i,j) : X(j) \to Y(j)$ which together yield a morphism of descent data. That the $f_\alpha$ are a morphism of descent data means that the following holds for each tuple $\alpha\beta$ of external indices. $$\forall j:J.\forall i_1:I_\alpha(j).\forall i_2:I_\beta(j). f_\alpha(j,i_1) = f_\beta(j,i_2)$$ Using again that internally for each $j$ at least one $I_\alpha(j)$ is inhabited, we can derive that the following is valid internally. $$\forall j:J.\forall x:X(j).\exists ! y:Y(j). \bigvee_\alpha (\exists i:I_\alpha(j) \wedge y = f_\alpha(j,i)(x))$$ When we write $\varphi(j,x,y)$ for the formula appearing after the $\exists !$-quantifier, then we may use the $\iota$-operator of definite description to get the term which we like. (This is a bit of a cheat, since showing that the $\iota$-operator of definite description has a sound semantic is essentially the same thing as showing that $\mathbb S$ is a prestack, but since it is often part of type theory, I will freely use it). We can judge that $$j:J,x:X(j) \vdash \iota y.\varphi(j,x,y) : Y(j) $$ and the function which we are looking for is of course $$j:J\vdash \lambda x.(\iota y.\varphi(j,x,y)):X(j)\to Y(j)$$ We have shown that the functor into descent data is full. Finally, let us check that $(I_\alpha)_\alpha$ is an effective family of dependent types (i.e. that the functor into descent data is essentially surjective on objects). For that we will need effective quotient types and disjoint coproducts. We start with an object $(X_\alpha,\theta_{\alpha\beta})$ in the category of descent data. We like to find a dependent type $j:J\vdash X(j):Type$ which restricts up to an isomorphism to our descent data. The dependent type $X$ will be a quotient of the following type.$$j:J\vdash \bigsqcup_\alpha \sum_{i:I_\alpha(j)}X_\alpha(j,i)$$ Let us for a second write $j:J\vdash Y(j)$ for that type. To get a quotient type we need to produce an internal equivalence relation $$j:J\vdash R(j): Y(j)\times Y(j) \to Prop$$ I am using the subobject classifier $Prop$ only to simplify the notation, it is not really necessary for the proof! The idea is of course to identify all the fibers $X_\alpha(j,i)$ where $j$ is fixed and $\alpha$ and $i$ vary. So the relation we need is the following one. \begin{align}j:J,y_1:\bigsqcup_\alpha \sum_{i:I_\alpha(j)}X_\alpha(j,i), y_2:\bigsqcup_\alpha \sum_{i:I_\alpha(j)}X_\alpha(j,i) \vdash \\ \bigvee_{\alpha \beta} \exists i_1:I_\alpha(j).\exists i_2: I_\beta(j).\exists x_1:X_\alpha(j,i_1).\exists x_2:X_\beta(j,i_2). \\(y_1 = inc_\alpha (i_1,x_1)\wedge y_2 = inc_\beta (i_2,x_2) \wedge \theta_{\alpha\beta}(j,i_1,i_2)(x_1)= x_2) : Prop\end{align} I hope there is no typo in the formula. Let me write $R(j,y_1,y_2)$ for it. The internal equivalence relation which we need is $\lambda (y_1,y_2).R(j,y_1,y_2): Y(j)\times Y(j)\to Prop$. It is reflexive the $\theta_{\alpha \alpha}$ are identities. It is transitive because of the cocycle condition and symmetric because the $\theta_{\alpha\beta}$ are invertible. We may thus define $j:J\vdash X(j)$ as the dependent quotient $$j:J\vdash \left(\bigsqcup_\alpha \sum_{i:I_\alpha(j)} X_\alpha(i,j)\right)/R(j) : Type$$ The universal property of quotients then gives us comparison morphisms $$j:J,i:I_\alpha(j)\vdash q_\alpha(j,i): X(j)\to X_\alpha(i,j)$$ The remaining steps are checking that the comparison morphisms assemble into a morphism of descent data, and that they are bijective from the internal perspective (this implies that they are isomorphisms). For this we will need that the coproducts are disjoint and quotients are effective. I skip over the rest, because the answer is already long.