A **subsingleton** generally refers to a subset (of some ambient set $A$) having at most one element. That is, it is a subset $B$ of $A$ such that any two elements of $B$ 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 $A$” is the partial map classifier for $A$, often denoted $A_\bot$.

Sometimes a slightly different convention is used: There what we call subsingletons are called **subterminals**, and a subset $B$ of $A$ is a *subsingleton* if and only if there exists an element $a \in A$ such that every element of $B$ is equal to $a$. 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.