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?


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.