nLab strict singleton



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.


Last revised on September 17, 2023 at 17:11:50. See the history of this page for a list of all contributions to it.