In dependent type theory, a strict singleton or a strict contractible type is a pointed strict proposition, or equivalently a strict proposition which is also a singleton or contractible type. In dependent type theories where strict propositions instead of h-propositions are used to represent the predicate logic of the type theory, strict singletons represent the notion of truth in the theory.
The strict unit type with judgmental computation rules is a strict singleton.
Given a type $A$, the strict function type $\emptyset \to A$ from the empty type to $A$, with judgmental computation rules, is a strict singleton.
The squash type of any pointed type is a strict singleton.
Last revised on September 17, 2023 at 17:11:50. See the history of this page for a list of all contributions to it.