Recall that a topos is a category that behaves likes the category Set of sets.
An two-valued object internal to a topos is an object that behaves in that topos like the set with exactly two elements does in Set.
An two-valued object in a topos (or any cartesian closed category) with terminal object is
an object in
equipped with
a morphism from the terminal object ;
a morphism from the terminal object ;
such that for every other tuple there is a morphism such that
By the universal property, the two-valued object is unique up to isomorphism.
The two-valued object is an initial object in the category of bi-pointed objects.
The two-valued object is the disjoint coproduct of the terminal object with itself.
… (One should be able to define binary coproducts using the dependent sum functor and the two-valued object, as dependent sums exist in topoi and cartesian closed categories.)
… (Same thing as above but with binary products and dependent products.)
A topos with a subobject classifier that is also a two-valued object is a two-valued topos. The internal logic of such a topos is two-valued logic.
Two-valued objects are the categorical semantics of the two-valued type in type theory. The inductive property of the two-valued type, case analysis or if/else expressions, corresponds to the initiality of the two-valued object in the subcategory of triples representing bi-pointed objects, similar to how the principle of induction over natural numbers corresponds to the initiality of the natural numbers object in the subcategory of triples representing infinite sequences.
Last revised on March 21, 2021 at 14:53:16. See the history of this page for a list of all contributions to it.