Truncation and $\textsf{isProp}$

Question

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$.

Answer 1

First, this:

In words, $A$ has the property $\mathsf{isProp}$ iff $A$ is either a singleton type or empty.

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}$.