<p>Squash types correspond to <em>judgmental</em> truncation, not <em>propositional</em> truncation.  In a type theory without a type for judgmental equality, there's non much of a way to make use of an inhabitant of a squash type; there's no way to write an eliminator into any type except another squash type.  Relatedly, having squash types, as presented in the book you linked, makes typechecking undecidable; having propositional truncation types does not result in this drawback.</p>

<p>Why do squash types result in undecidable typechecking?  Quoting the book you linked:</p>

<blockquote>
  <p>The first approach to representing the proposition is to consider the ‘squash’
  type, defined in [C+86a] to be</p>
  
  <p>$\|A\| ≡_{df} \{ t : \top\ \mid\ A \}$</p>
  
  <p>which will be inhabited by the object $Triv$ if and only if there is some proof
  object $a : A$.</p>
</blockquote>

<p>Now let $A$ be your favorite undecidable problem, and ask your typechecker to decide if $Triv$ has type $\|A\|$.  By construction, it can't decide your problem, and thus can't typecheck $Triv : \|A\|$.</p>

<p>Note that this problem is specific to squash types with canonically named inhabitants.  Agda has a form of judgmental truncation, which goes by the name "irrelevant arguments" or "irrelevant fields", without canonically named inhabitants.  Agda maintains decidable typechecking, though I think it doesn't manage to throw away the proofs, and has to carry them around (perhaps only for technical implementation reasons).  (This would be something to ask about on the Agda mailing list.)  These suffer the drawback, mentioned above, of not being able to eliminate into any non-irrelevant types.</p>

CC BY-SA 3.0
2015-02-21T18:07:42.463Z
> having squash types makes typechecking undecidable

But why this is so?
Konstantin Solomatov
CC BY-SA 3.0
2015-02-22T10:36:07.033Z
I've added an argument to this effect for squash types as defined in the book you linked to.
Jason Gross
CC BY-SA 3.0
2015-02-21T06:56:36.237Z
2015-02-22T10:35:19.450Z
2015-02-22T10:35:19.450Z
Jason Gross
<p>Homotopy type theory has a notion of propositional truncation type. It seems to me that it's strongly related to a notion of squash types. (See <a href="https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf">https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf</a> p. 265). It seems that squash types have serious problems with definitions (see the book), and prop. trunc don't. Why this is so? What are these problems? (The book mentions them, but I can't  understand well what they are, they have an example for subtypes but, AFAIU it doesn't apply to squash types).</p>

<lo.logic><type-theory><homotopy-type-theory>
Squash type vs Propositional truncation type
Konstantin Solomatov
# Squash type vs Propositional truncation type

(Asked by: username_0 on 2015-02-18)

Homotopy type theory has a notion of propositional truncation type. It seems to me that it's strongly related to a notion of squash types. (See <https://www.cs.kent.ac.uk/people/staff/sjt/TTFP/ttfp.pdf> p. 265). It seems that squash types have serious problems with definitions (see the book), and prop. trunc don't. Why this is so? What are these problems? (The book mentions them, but I can't understand well what they are, they have an example for subtypes but, AFAIU it doesn't apply to squash types).

**Tags:** lo.logic, type-theory, homotopy-type-theory


---

## 1 answers

### Answer by username_1 on 2015-02-21. Score: 6 | Accepted answer

Squash types correspond to *judgmental* truncation, not *propositional* truncation. In a type theory without a type for judgmental equality, there's non much of a way to make use of an inhabitant of a squash type; there's no way to write an eliminator into any type except another squash type. Relatedly, having squash types, as presented in the book you linked, makes typechecking undecidable; having propositional truncation types does not result in this drawback.

Why do squash types result in undecidable typechecking? Quoting the book you linked:

> The first approach to representing the proposition is to consider the ‘squash’
> type, defined in [C+86a] to be
>
> $\|A\| ≡\_{df} \{ t : \top\ \mid\ A \}$
>
> which will be inhabited by the object $Triv$ if and only if there is some proof
> object $a : A$.

Now let $A$ be your favorite undecidable problem, and ask your typechecker to decide if $Triv$ has type $\|A\|$. By construction, it can't decide your problem, and thus can't typecheck $Triv : \|A\|$.

Note that this problem is specific to squash types with canonically named inhabitants. Agda has a form of judgmental truncation, which goes by the name "irrelevant arguments" or "irrelevant fields", without canonically named inhabitants. Agda maintains decidable typechecking, though I think it doesn't manage to throw away the proofs, and has to carry them around (perhaps only for technical implementation reasons). (This would be something to ask about on the Agda mailing list.) These suffer the drawback, mentioned above, of not being able to eliminate into any non-irrelevant types.

> **Comments:**
> **username_0**: > having squash types makes typechecking undecidable  But why this is so?  
> **username_1**: I've added an argument to this effect for squash types as defined in the book you linked to.  

---

