In set theory, the support of a set turns the set into a subsingleton. In dependent type theory, propositional truncation or the bracket type is an operation which takes a type and turns it into a h-propositions, which are the type theoretic equivalent of subsingletons. By the relation between type theory and category theory and the relation between set theory and topos theory, it should be possible to do the same process and turn an object of a category into a subterminal object. These are the support objects, bracket objects, or propositional truncation objects in category theory.
The support object of an object in a category with a terminal object is the image of the unique morphism .
As a result, that all support objects exist is equivalent to the condition that every morphism into the terminal object has an image factorization.
In any well-pointed pretopos , the support is the coequalizer of the product projection morphisms and
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
Last revised on October 17, 2022 at 05:06:01. See the history of this page for a list of all contributions to it.