Under the principle of propositions-as-types, existential propositions in logic are compared to $\Sigma$-types, and we have two projection rules $\pi_1$ and $\pi_2$ to make proof extraction. If we impose the principle of proof irrelevance, say by the operation of propositional truncation $||$–$||$, then the two projection rules no longer work for proof-irrelevant $\Sigma$-types. For convenience, I use the traditional notation $\exists$ for the proof-irrelevant $\Sigma$.
My question is related to this, for a proof-irrelevant proposition, say $(\exists X:\textsf{Prop})((X\rightarrow A)\wedge X)$ where $A:\textsf{Prop}$, how can we give an elegant proof for the following proposition without the availability of projection rules?
$$((\exists X:\textsf{Prop})((X\rightarrow A)\wedge X)))\rightarrow A$$
Best Answer
I will assume that by proof irrelevance you mean contratibility, that is the derivability of $x,y:A\vdash x =_A y$. Your statement cannot be proved unless you assume that $A$ is a contractible proposition. The reason is that $\exists X:Y.Q$ is contractible, and to build a function out of a contractible domain, the codomain must either be contractible or you must know one of its elements.
In general the elimination rule for propositional truncation says that to give a map $\|B\|\to C$, it suffices to give a map $f:B\to C$ and to check that $C$ is contractible.
So in your question, to prove $$(\exists X:\text{Prop}.X\wedge (X\to A))\to A :\equiv \left\|\Sigma X:\text{Prop}.X\wedge (X\to A)\right\|\to A,$$ it simply suffices to find a map $$(\Sigma X:\text{Prop}.X\wedge (X\to A))\to A$$ as one usually would by application.