nLab two-valued object

Idea

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 $\mathbf{2}$ with exactly two elements does in Set.

Definition

In a topos or cartesian closed category

An two-valued object in a topos (or any cartesian closed category) $E$ with terminal object $1$ is

• an object $\mathbf{2}$ in $E$

• equipped with

  • a morphism $zero:1 \rightarrow \mathbf{2}$ from the terminal object $1$;

  • a morphism $one:1 \rightarrow \mathbf{2}$ from the terminal object $1$;

• such that for every other tuple $(A, t, f)$ there is a morphism $u : \mathbf{2} \to A$ such that

By the universal property, the two-valued object is unique up to isomorphism.

Properties

As an initial object

The two-valued object $\mathbf{2}$ is an initial object in the category of bi-pointed objects.

Coproducts

The two-valued object $\mathbf{2}$ is the disjoint coproduct of the terminal object $1$ 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.)

Products

… (Same thing as above but with binary products and dependent products.)

Subobject classifier

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.

Type theory

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 $(A, t:1\rightarrow A, f:1\rightarrow A)$ 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 $(A, q:1\rightarrow A, f:A\rightarrow A)$ representing infinite sequences.

See also

• natural numbers object

• bi-pointed object

• subobject classifier

• two-valued type, two-valued topos, two-valued logic