# Truncation and $\textsf{isProp}$

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

• You may as well ask the question about $\textsf{isProp} (P) \to (\| P \| \leftrightarrow P)$, where $P$ is an arbitrary type. It is true for the reason you state: if $P$ is a propositional type then $P$ is equivalent to $\| P \|$. Dec 11, 2020 at 12:44

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