# Set truncations in homotopy type theory

We can define set truncation as a higher inductive type with the following constructors:

• $|-|_0 : A \to ||A||_0$
• trunc : $(a\ a' : ||A||_0)\ (p\ p' : a = a') \to p = p'$

If we replace the type of trunc with $(a\ a' : A)\ (p\ p' : a = a') \to \text{pmap}\ (|-|_0)\ p = \text{pmap}\ (|-|_0)\ p'$, then this definition will be too weak.

The question is, what if we define trunc as follows:

trunc : $(a\ a' : A)\ (p\ p' : |a|_0 = |a'|_0) \to p = p'$?

Is this enough to give us the set truncation or is it also too weak?

Suppose we are given $B : \| A \|_0 \rightarrow U$ together with
• a function $g : \Pi_{(a : A)} B(|a|_0)$, and
• for any $a, b: A$ with $z : B(|a|_0)$, $w : B(|b|_0)$, and each $p, q : |a|_0 = |b|_0$ with $r : z =^B_p w$ and $s: z =^B_q w$, a 2-path $v : r =^{z =^B_- w}_{u(x, y, p, q)} s$, where $u(x, y, p, q) : p = q$ is obtained from $\operatorname{trunc}$.
Then there exists $f : \Pi_{(x : \|A\|_0)} B(x)$.
Now using the above induction principle, we can show that this set truncation is equivalent to the usual one. It is enough to show that $\| A \|_0$ is an hSet.
To apply the induction principle, set $B(x) := \operatorname{IsContr}(x = x)$. We can apply $\operatorname{trunc}$ to construct a witness of $B(|a|_0)$ for each $a : A$. Since $B(x)$ is an hProposition, we can ignore the "higher" part of the inductive hypothesis. Now by induction we obtain that for all $x : \|A \|_0$, $\operatorname{IsContr}(x = x)$, and hence $\|A\|_0$ is an hSet, as required.