This article is about support of a set. For other notions of support, see support.
basic constructions:
strong axioms
further
The support $[X]$ of any set $X$ is the image of the unique function into any singleton $X \to 1$. By definition of image the support is thus a subsingleton, and a singleton if $X$ is pointed. Note that this is different from the support of the unique function $X \to 1$, which is always the empty set $\emptyset$.
The above definition could be interpreted not just in Set but in any category with a terminal object. This leads to the notions of a support object.
The support object of an object $A$ of a category is the image of its map to the terminal object. In the internal logic of a category, this corresponds to the propositional truncation.
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Created on October 17, 2022 at 04:55:14. See the history of this page for a list of all contributions to it.