nLab squash type



A version of propositional truncation which takes types and turns them into strict propositions.


Direct definition

Provided that function types and dependent function types have judgmental computation rules, given a type of strict propositions sProp\mathrm{sProp}, the squash type could be defined in the same manner as propositional truncations:

[A] s P:sProp(AP)P[A]_s \coloneqq \prod_{P:\mathrm{sProp}} (A \to P) \to P

Inference rules

Without a type of strict propositions sProp\mathrm{sProp}, or if either function types or dependent function types only have typal computation rules, the squash type would have to be defined using inference rules.

ΓAtypeΓ[A] stypeΓAtypeΓ,x:[A] s,y:[A] sxy:[A] sΓx:AΓsquash(x):[A] s\frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma \vdash [A]_s \; \mathrm{type}} \qquad \frac{\Gamma \vdash A \; \mathrm{type}}{\Gamma, x:[A]_s, y:[A]_s \vdash x \equiv y:[A]_s} \qquad \frac{\Gamma \vdash x:A}{\Gamma \vdash \mathrm{squash}(x):[A]_s}
ΓAtypeΓPtypeΓ,p:P,q:Ppq:PΓf:APΓx:[A] sΓunsquash P(f,x):P\frac{\Gamma \vdash A \; \mathrm{type} \quad \Gamma \vdash P \; \mathrm{type} \quad \Gamma, p:P, q:P \vdash p \equiv q:P \quad \Gamma \vdash f:A \to P \quad \Gamma \vdash x:[A]_s}{\Gamma \vdash \mathrm{unsquash}_P(f, x):P}

Similarly to propositional truncations, the recursion rule for squash types is sufficient to define the induction rule for squash types.


Last revised on January 16, 2024 at 16:05:15. See the history of this page for a list of all contributions to it.