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, 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.