I've heard of many truncations in homotopy type theory, like propositional truncation, homotopy n-truncation, etc., and I think I understand these specific concepts.

People also talk about 'double-negation truncation', which talks about the 'double-negation' version of a certain type.

I'm wondering if there is a general definition or folklore notion called 'truncation'? Is it a special kind of modality or something?

  • 3
    $\begingroup$ A search for "double negation truncation" turns up nothing. Can you point to where this phrase is used? $\endgroup$
    – Trebor
    Jun 13, 2022 at 3:23
  • $\begingroup$ I'm just guessing but I suppose you could call the double negation translation a "truncation" because you are losing the constructive information $\endgroup$
    – Couchy
    Jun 13, 2022 at 4:21
  • $\begingroup$ @Trebor in our private conversations. :P $\endgroup$
    – ice1000
    Jun 13, 2022 at 7:35

1 Answer 1


Yes, truncations are a form of modalities, as explained in Section 7.7 of the HoTT book.

  • $\begingroup$ Thanks very much! $\endgroup$
    – ice1000
    Jun 13, 2022 at 19:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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