Are Proofs of Dependent Pair Types Equivalent to Finding an Inverse Function?

Question

Since $\Pi_{(B:A\rightarrow\mathcal{U})}\Sigma_{(a:A)}B(a)$ is the type theoretic way for expressing $\forall B:A\rightarrow\mathcal{U}.\exists a \in A. B(a)$ and one often has to work backwards to figure out what $a$ is supposed to be in a proof, would a proof of $\Pi_{(B:A\rightarrow\mathcal{U})}\Sigma_{(a:A)}B(a)$ be equivalent to finding a certain function of type $(A\rightarrow\mathcal{U})\rightarrow A$?