In classical mathematics, a subsingleton could either be defined as
However, in constructive mathematics, the two notions of subsingleton are no longer the same, because the axiom of excluded middle no longer holds true. Instead, one usually defines a subsingleton as the first definition, and the second definition is then referred to as about decidable subsingletons.
Every subsingleton comes with an injection into a singleton , and is thus is a (structural) subset of . A subsingleton is also decidable in the subset sense: defining the relation as
for all elements , or .
Decidable subsingletons could be generalized from Set to any coherent category: they are precisely the decidable subterminal objects in a coherent category.
Last revised on August 2, 2023 at 18:25:50. See the history of this page for a list of all contributions to it.