5
$\begingroup$

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?

Improve this question
$\endgroup$
3
  • 3
    $\begingroup$ A search for "double negation truncation" turns up nothing. Can you point to where this phrase is used? $\endgroup$
    – Trebor ♦
    Commented 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
    Commented Jun 13, 2022 at 4:21
  • $\begingroup$ @Trebor in our private conversations. :P $\endgroup$
    – ice1000 ♦
    Commented Jun 13, 2022 at 7:35

1 Answer 1

Reset to default
4
$\begingroup$

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

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thanks very much! $\endgroup$
    – ice1000 ♦
    Commented 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.