# 3.7 Propositional truncation

The propositional truncation, also called the $(-1)$-truncation, bracket type, or squash type, is an additional type former which “squashes” or “truncates” a type down to a mere proposition, forgetting all information contained in inhabitants of that type other than their existence.

More precisely, for any type $A$, there is a type $\mathopen{}\left\|A\right\|\mathclose{}$. It has two constructors:

• For any $a:A$ we have $\mathopen{}\left|a\right|\mathclose{}:\mathopen{}\left\|A\right\|\mathclose{}$.

• For any $x,y:\mathopen{}\left\|A\right\|\mathclose{}$, we have $x=y$.

The first constructor means that if $A$ is inhabited, so is $\mathopen{}\left\|A\right\|\mathclose{}$. The second ensures that $\mathopen{}\left\|A\right\|\mathclose{}$ is a mere proposition; usually we leave the witness of this fact nameless.

The recursion principle of $\mathopen{}\left\|A\right\|\mathclose{}$ says that:

• If $B$ is a mere proposition and we have $f:A\to B$, then there is an induced $g:\mathopen{}\left\|A\right\|\mathclose{}\to B$ such that $g(\mathopen{}\left|a\right|\mathclose{})\equiv f(a)$ for all $a:A$.

In other words, any mere proposition which follows from (the inhabitedness of) $A$ already follows from $\mathopen{}\left\|A\right\|\mathclose{}$. Thus, $\mathopen{}\left\|A\right\|\mathclose{}$, as a mere proposition, contains no more information than the inhabitedness of $A$. (There is also an induction  principle for $\mathopen{}\left\|A\right\|\mathclose{}$, but it is not especially useful; see http://planetmath.org/node/87806Exercise 3.20.)

In http://planetmath.org/node/87799Exercise 3.17,http://planetmath.org/node/87834Exercise 3.18,§6.9 (http://planetmath.org/69truncations) we will describe some ways to construct $\mathopen{}\left\|A\right\|\mathclose{}$ in terms of more general things. For now, we simply assume it as an additional rule alongside those of http://planetmath.org/node/87533Chapter 1.

With the propositional truncation, we can extend the “logic of mere propositions” to cover disjunction  and the existential quantifier  . Specifically, $\mathopen{}\left\|A+B\right\|\mathclose{}$ is a mere propositional version of “$A$ or $B$”, which does not “remember” the information of which disjunct is true.

The recursion principle of truncation implies that we can still do a case analysis on $\mathopen{}\left\|A+B\right\|\mathclose{}$ when attempting to prove a mere proposition. That is, suppose we have an assumption  $u:\mathopen{}\left\|A+B\right\|\mathclose{}$ and we are trying to prove a mere proposition $Q$. In other words, we are trying to define an element of $\mathopen{}\left\|A+B\right\|\mathclose{}\to Q$. Since $Q$ is a mere proposition, by the recursion principle for propositional truncation, it suffices to construct a function $A+B\to Q$. But now we can use case analysis on $A+B$.

Similarly, for a type family $P:A\to\mathcal{U}$, we can consider $\mathopen{}\left\|\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)% }}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x% :A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_% {(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)\right\|\mathclose{}$, which is a mere propositional version of “there exists an $x:A$ such that $P(x)$”. As for disjunction, by combining the induction principles of truncation and $\Sigma$-types, if we have an assumption of type $\mathopen{}\left\|\mathchoice{\sum_{x:A}\,}{\mathchoice{{\textstyle\sum_{(x:A)% }}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_{(x% :A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{\mathchoice{{\textstyle\sum_% {(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}P(x)\right\|\mathclose{}$, we may introduce new assumptions $x:A$ and $y:P(x)$ when attempting to prove a mere proposition. In other words, if we know that there exists some $x:A$ such that $P(x)$, but we don’t have a particular such $x$ in hand, then we are free to make use of such an $x$ as long as we aren’t trying to construct anything which might depend on the particular value of $x$. Requiring the codomain to be a mere proposition expresses this independence of the result on the witness, since all possible inhabitants of such a type must be equal.

For the purposes of set-level mathematics in http://planetmath.org/node/87585Chapter 11,http://planetmath.org/node/87584Chapter 10, where we deal mostly with sets and mere propositions, it is convenient to use the traditional logical notations to refer only to “propositionally truncated logic”.

###### Definition 3.7.1.

We define traditional logical notation using truncation as follows, where $P$ and $Q$ denote mere propositions (or families thereof):

 $\displaystyle\top$ $\displaystyle\ :\!\!\equiv\ \mathbf{1}$ $\displaystyle\bot$ $\displaystyle\ :\!\!\equiv\ \mathbf{0}$ $\displaystyle P\land Q$ $\displaystyle\ :\!\!\equiv\ P\times Q$ $\displaystyle P\Rightarrow Q$ $\displaystyle\ :\!\!\equiv\ P\to Q$ $\displaystyle P\Leftrightarrow Q$ $\displaystyle\ :\!\!\equiv\ P=Q$ $\displaystyle\neg P$ $\displaystyle\ :\!\!\equiv\ P\to\mathbf{0}$ $\displaystyle P\lor Q$ $\displaystyle\ :\!\!\equiv\ \mathopen{}\left\|P+Q\right\|\mathclose{}$ $\displaystyle\forall(x:A).\,P(x)$ $\displaystyle\ :\!\!\equiv\ \mathchoice{\prod_{x:A}\,}{\mathchoice{{\textstyle% \prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{\mathchoice{{% \textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x:A)}}}{% \mathchoice{{\textstyle\prod_{(x:A)}}}{\prod_{(x:A)}}{\prod_{(x:A)}}{\prod_{(x% :A)}}}P(x)$ $\displaystyle\exists(x:A).\,P(x)$ $\displaystyle\ :\!\!\equiv\ \Bigl{\|}\mathchoice{\sum_{x:A}\,}{\mathchoice{{% \textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}}}{% \mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:A)}% }}{\mathchoice{{\textstyle\sum_{(x:A)}}}{\sum_{(x:A)}}{\sum_{(x:A)}}{\sum_{(x:% A)}}}P(x)\Bigr{\|}$

The notations $\land$ and $\lor$ are also used in homotopy theory for the smash product and the wedge of pointed spaces, which we will introduce in http://planetmath.org/node/87579Chapter 6. This technically creates a potential for conflict, but no confusion will generally arise.

Similarly, when discussing subsets as in §3.5 (http://planetmath.org/35subsetsandpropositionalresizing), we may use the traditional notation for intersections  , unions, and complements  :

 $\displaystyle\{x:A|P(x)\}\cap\{x:A|Q(x)\}$ $\displaystyle:\!\!\equiv\{x:A|P(x)\land Q(x)\},$ $\displaystyle\{x:A|P(x)\}\cup\{x:A|Q(x)\}$ $\displaystyle:\!\!\equiv\{x:A|P(x)\lor Q(x)\},$ $\displaystyle A\setminus\{x:A|P(x)\}$ $\displaystyle:\!\!\equiv\{x:A|\neg P(x)\}.$

Of course, in the absence of $\mathsf{LEM}$, the latter are not “complements” in the usual sense: we may not have $B\cup(A\setminus B)=A$.

Title 3.7 Propositional truncation
\metatable