Truncated types or bracket types are used to recover traditional logic within type theory. I have a question about truncating $\Pi$-types. The question is very basic. Let $A:\textsf{U}$ and $B:A\rightarrow\textsf{U}$, then what is the relationship between the following two types?
$$||\Pi x:A.B(x)|| \quad(*),\quad\quad\quad\quad\Pi x:A.||B(x)||\quad(**)$$
Does $(*)\rightarrow(**)$ or the other way around? Thanks a lot!
In the Homotopy Type Theory book, I find the following (pp.119-120):
Lemma 3.8.2 The axiom of choice is equivalent to the statement that for any set $X$ and any $Y:X\rightarrow\textsf{U}$ such that each
$Y(x)$ is a set, we have $$(\Pi x:X.||Y(x)||)\rightarrow||\Pi x:X.Y(x)||.\quad\quad\quad(3.8.3)$$
Then immediately, in a remark, it says the following:
Remark 3.8.4. It is easy to show that the right side of (3.8.3) always implies the left. …
I got sort of confused. Does this say that the two types are equivalent?
Best Answer
First, note that $\Pi x:A.||B(x)||$ is a mere proposition.
Indeed, suppose $f , g : \Pi x:A.||B(x)||$. We must show $f = g$. By extensionality, it is sufficient to show that for all $x : A$ we have $f(x) = g(x)$. So let $x : A$. Since $f(x) , g(x) : ||B(x)||$, we have $f(x) = g(x)$ due to the fact that $||B(x)||$ is a mere proposition.
Second, note that $\lambda f. \lambda x. |f(x)| : (\Pi x:A.B(x)) \to \Pi x:A.||B(x)||$. Thus, from the recursion principle of truncation, there is a term of the type $||\Pi x:A.B(x)|| \to \Pi x:A.||B(x)||$.
So we have shown $(*) \to (**)$. The other way around, i.e. $(**) \to (*)$, is the axiom of choice. Read carefully lemma 3.8.2 that you quoted. The book does not claim that the axiom of choice is valid, only that there are two equivalent statements of it.