nLab decidable subsingleton



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 SS comes with an injection i:S1i \colon S \to 1 into a singleton 11, and is thus is a (structural) subset of 11. A subsingleton is also decidable in the subset sense: defining the relation x 1Sx \in_1 S as

x 1Sy1.i(x)=yx \in_1 S \coloneqq \exists y \in 1.i(x) = y

for all elements x1x \in 1, x 1Sx \in_1 S or ¬(x 1S)\neg (x \in_1 S).

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.