Reducing products in HoTT to church/scott encodings
The standard reference I often give is Induction is not derivable in second order dependent type theory by Herman Geuvers, which says that there is no type

$$N : \mathrm{Type}$$

with functions
$$Z:N\qquad S:N\rightarrow N $$

such that

$$\mathrm{ind}:\Pi P:N\rightarrow \mathrm{Type}.P\ Z\rightarrow (\Pi m:N.P\ m\rightarrow P\ (S\ m))\rightarrow \Pi n:N. P\ n $$

is provable. This suggests that indeed, such an encoding cannot work for pairs as you describe.

The system this is proven for is a subset of the Calculus of Constructions, which contains powerful product types and a universe. I suspect this result can be extended to the system you are interested in, depending on what you have.

Sadly, I don't know the complete answer to your question. I suspect that adding certain parametricity principles "internally" is exactly what is required to make these encodings work with the full induction principle. Neel Krishnaswami, whose knowledge is a strict superset of my own, wrote a paper along these lines with Derek Dreyer:

Internalizing Relational Parametricity in the Extensional Calculus of Constructions

Also of interest is the following paper by Bernardy, Jansson and Patterson (Bernardy has thought deeply about these topics):

Parametricity and Dependent Types

Obviously parametricity has a strong relationship with HoTT in general, but I don't know what the details are. I think Steve Awodey has considered these questions, since the encoding trick is useful in contexts where we don't really know what the eliminators should look like.