nLab
squash type
Contents
Idea
A version of propositional truncation which takes types and turns them into strict propositions.
Definition
Direct definition
Provided that function types and dependent function types have judgmental computation rules, given a type of strict propositions , the squash type could be defined in the same manner as propositional truncations:
Inference rules
Without a type of strict propositions , 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.
Similarly to propositional truncations, the recursion rule for squash types is sufficient to define the induction rule for squash types.
References
Last revised on January 16, 2024 at 16:05:15.
See the history of this page for a list of all contributions to it.