In type theory, in particular, homotopy type theory. We have a notion of $\textsf{isProp}$ defined as follows (where we let $A:\textsf{Type}$):
$$\textsf{isProp}(A):=\Pi x,y:A.x=_Ay.$$
In words, $A$ has the property $\textsf{isProp}$ iff $A$ is either a singleton type or empty. Then, we have the truncation operation $||$–$||$. Let $A:\textsf{Type}$, then $||A||:\textsf{Prop}$.
My question is, if $\Sigma x:A.B(x)$ is known to have at most one inhabitant, that is, that $\Sigma x:A.B(x)$ in fact satisifes $\textsf{isProp}$, can we have the following?
$$\textsf{isProp}(\Sigma x:A.B(x))\rightarrow(||\Sigma x:A.B(x)||\leftrightarrow\Sigma x:A.B(x))$$
In this case, since $||\Sigma x:A.B(x)||$ is equivalent to $\Sigma x:A.B(x)$, we can apply the projection rules $\pi_1$ and $\pi_2$ of $\Sigma$.
Best Answer
First, this:
is incorrect unless one is assuming excluded middle. Constructively, propositions cannot be assumed to be either a singleton or empty.
The answer to your first question is, 'yes'. Truncation has an inclusion function:
$$|-| : A → \Vert A \Vert$$
And the induction principle for truncation allows for:
$$\mathsf{out}_{\Vert A \Vert} : \Vert A \Vert → A$$
provided $\mathsf{isProp}\ A$. Since both types are propositions and imply one another, it is even the case that $\Vert A \Vert =_\mathcal{U} A$ via univalence.
I'm unclear what precisely your second question means. You cannot exactly apply $π_1$ to a value of $\Vert Σ x:A. B(x)\Vert$ because it is ill typed. However, if the sigma type is a proposition, you can either use $\mathsf{out}$ to get a value that you can apply $π_1$ to, or you can transport $π_1$ along the equality between the types to get something of the right type to apply to the truncated type, which will have the same behavior as using $\mathsf{out}$.