nLab strict singleton

Idea

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.

Examples

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

 Related concepts

• judgmental equality

• strict proposition