Propositional Truncation (HIT)

Definition

The propositional truncation $\parallel A\parallel$ is a Higher Inductive Type that truncates a type $A$ to a proposition (a (-1)-Type).

Given a type $A$, the propositional truncation $\parallel A\parallel$ has the following constructors:

• $|\_|:A\to \parallel A\parallel$
• $\mathrm{squash}:\forall x,y:\parallel A\parallel .(x=y)$

The first constructor embeds elements of $A$ into the truncation. The second constructor ensures that any two elements of $\parallel A\parallel$ are equal, making it a proposition.

Properties

The propositional truncation satisfies the universal property of (-1)-Truncation: it is a proposition, and any function from $A$ to a proposition $P$ factors uniquely through $\parallel A\parallel$.

The propositional truncation is used to express existence without providing a specific witness. While $A$ may have many distinct elements, $\parallel A\parallel$ has at most one element up to identity.

Usage

Propositional truncation is fundamental in Homotopy Type Theory for:

• Expressing mere existence (existential quantification)
• Converting types into propositions
• Implementing logical connectives that forget computational content

Related Concepts

Higher Inductive Type Truncation (HoTT) (-1)-Type Proposition 0-Type Set Quotient