3.7 Propositional truncation

The propositional truncation, also called the $\mathrm{(}\mathrm{-}\mathrm{1}\mathrm{)}$-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 $\parallel A\parallel$. It has two constructors:

• For any $a:A$ we have $\left|a\right|:\parallel A\parallel$.

• For any $x,y:\parallel A\parallel$, we have $x=y$.

The first constructor means that if $A$ is inhabited, so is $\parallel A\parallel$. The second ensures that $\parallel A\parallel$ is a mere proposition; usually we leave the witness of this fact nameless.

The recursion principle of $\parallel A\parallel$ says that:

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

In other words, any mere proposition which follows from (the inhabitedness of) $A$ already follows from $\parallel A\parallel$. Thus, $\parallel A\parallel$, as a mere proposition, contains no more information than the inhabitedness of $A$. (There is also an induction principle for $\parallel A\parallel$, 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 $\parallel A\parallel$ 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, $\parallel A+B\parallel$ 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 $\parallel A+B\parallel$ when attempting to prove a mere proposition. That is, suppose we have an assumption $u:\parallel A+B\parallel$ and we are trying to prove a mere proposition $Q$. In other words, we are trying to define an element of $\parallel A+B\parallel \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 𝒰$, we can consider $\parallel {\sum }_{(x:A)}P(x)\parallel$, 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 $\mathrm{\Sigma }$-types, if we have an assumption of type $\parallel {\sum }_{(x:A)}P(x)\parallel$, 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):

$\top$ $\mathrm{ }:\equiv \mathbf{\hspace{0.25em}1}$

$\perp$ $\mathrm{ }:\equiv \mathbf{\hspace{0.25em}0}$

$P\wedge Q$ $\mathrm{ }:\equiv P\times Q$

$P\Rightarrow Q$ $\mathrm{ }:\equiv P\to Q$

$P\iff Q$ $\mathrm{ }:\equiv P=Q$

$\mathrm{\neg }P$ $\mathrm{ }:\equiv P\to \mathrm{𝟎}$

$P\vee Q$ $\mathrm{ }:\equiv \parallel P+Q\parallel$

$\forall (x:A).P(x)$ $\mathrm{ }:\equiv {\displaystyle \prod _{x:A}}P(x)$

$\exists (x:A).P(x)$ $\mathrm{ }:\equiv \parallel {\displaystyle \sum _{x:A}}P(x)\parallel$

The notations $\wedge$ and $\vee$ 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:

$\mathrm{\{}x:A|P(x)\}\cap \{x:A|Q(x)\}$ $:\equiv \{x:A|P(x)\wedge Q(x)\},$

$\mathrm{\{}x:A|P(x)\}\cup \{x:A|Q(x)\}$ $:\equiv \{x:A|P(x)\vee Q(x)\},$

$A\setminus \{x:A|P(x)\}$ $:\equiv \{x:A|\mathrm{\neg }P(x)\}.$

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

Title	3.7 Propositional truncation