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?



Set truncations in homotopy type theory
In order for this to be a higher inductive type, we also need an induction principle. By analogy with the induction principle for the usual set truncation in section 6.9 of [the HoTT book](https://hott.github.io/book/nightly/hott-online-1040-gd35275f.pdf), we might use the following:


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.


