Currently I am learning about dependent pair ($\Sigma$-)types, and I'm having some trouble understanding how an instance of a dependent type could be formed. I think I understand how the type of a dependent pair looks, but how do values of that type look like in practice?
From my understanding, given a type $\Sigma(x:\tau).\tau'$, the members are pairs where the first entry has type $\tau$ and the second one has type which may depend on the value $\tau'[x\mapsto\tau]$, which generalizes $\tau\times\tau'$. For example $$ x_1,x_2:\tau \\ \tau'(x_1):=\tau_1 \\ \tau'(x_2):=\tau_2 \\ $$ Then if we have some $y_1:\tau_1,y_2:\tau_2$ then $$ (y_1,y_2):\Sigma(x:\tau).\tau' $$ But this raises a problem: in a clean, unnotated environment, the type of $(y_1,y_2)$ would be infereed to be $\tau_1\times\tau_2$. This is a problem because I still want the pair to be used in a context where a dependent pair is needed.
This has me confused, because by introducing a pair we are fixing $\tau'$. Do I have a wrong idea about what dependent pairs are supposed to be? What other way would there be to introduce a dependent pair? Is an annotation required for this concept to work?