Let $P$ be a type, $||P||$ denotes a mere proposition obtained by truncating $P$. Let $D$ be a type and $A:D\rightarrow\textsf{U}$, then $\Pi x:D.A(x)$ is a well-formed type. Assuming that we are working with intuitionistic logic, we have $(*)$ but not its converse. $$||\Pi x:D.A(x)||\rightarrow\Pi x:D.||A(x)||\tag{$*$}$$ My question is: let $D$ denote a finite domain such that $D=\{d_1,...,d_n\}:\textsf{U}$, can we have the converse of $(*)$, namely: $$\Pi x:D.||A(x)||\rightarrow||\Pi x:D.A(x)||\tag{$**$}$$ It seems to me that $(**)$ should hold. Given $D=\{d_1,...,d_n\}:\textsf{U}$, we shall then write $\Pi x:D.A(x)$ as $A(d_1)\times...\times A(d_n)$. Since we have $||P\times Q||\leftrightarrow||P||\times||Q||$ (for $P,Q:\textsf{U}$), we shall generalize it to $A(d_1)\times...\times A(d_n)$ such that we have $(***)$: $$||A(d_1)||\times...\times||A(d_n)||\rightarrow||A(d_1)\times...\times A(d_n)||\tag{$***$}$$
I find this very similar to the case of double negation shift (DNS). It is known that in intuitionistic logic, the converse of DNS is a theorem, but DNS itself is not. But if we require that the domain be finite, then writing $\Pi x:D.A(x)$ as a generalized conjunction $A(d_1)\times...\times A(d_n)$, DNS is valid by virtue of the fact that $\neg\neg$ distributes over $\rightarrow$ (that is, $\neg\neg(P\rightarrow Q)\leftrightarrow(\neg\neg P\rightarrow \neg\neg Q)$ for $P,Q:\textsf{U}$). $$\Pi x:D.\neg\neg A(x)\rightarrow\neg\neg\Pi x:D.A(x)\tag{DNS}$$
I think it's something very basic, but since I have not read it in any introductory book I know, I am not sure if my reasoning is correct. Can anyone help me?
You are correct. Here is a cubical Agda proof. It essentially carries out your product-of-truncations = truncation-of-product equivalence by induction on the (size of the) finite set. The rest is just dealing with transporting along a (truncated) witness that a type is equivalent to the inductively defined finite sets.