A subsingleton generally refers to a subset (of some ambient set ) having at most one element. That is, it is a subset of such that any two elements of are equal.
Of course, classically any subsingleton is either empty or a singleton, but constructively this need not hold. In a topos, the “object of subsingletons in ” is the partial map classifier for , often denoted .
Sometimes a slightly different convention is used: There what we call subsingletons are called subterminals, and a subset of is a subsingleton if and only if there exists an element such that every element of is equal to . With this nomenclature, any subsingleton is a subterminal, but the converse doesn’t hold in general. (See flabby sheaf for a class of examples where the converse does hold.)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Last revised on August 2, 2023 at 17:06:29. See the history of this page for a list of all contributions to it.