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


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.

  • $\begingroup$ > having squash types makes typechecking undecidable But why this is so? $\endgroup$ – Konstantin Solomatov Feb 21 '15 at 18:07
  • $\begingroup$ I've added an argument to this effect for squash types as defined in the book you linked to. $\endgroup$ – Jason Gross Feb 22 '15 at 10:36

Your Answer

