boolean domain object in nLab

Boolean domain object

Boolean domain object

Idea

Recall that a topos is a category that behaves likes the category Set of sets.

A boolean domain object internal to a topos is an object that behaves in that topos like the boolean domain Bool\mathrm{Bool} does in Set.

Definition

In a topos or cartesian closed category

A boolean domain object in a topos (or any cartesian closed category) EE with terminal object 11 is

• an object 2\mathbf{2} in EE

• equipped with

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

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

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

By the universal property, the boolean domain object is unique up to isomorphism.

Properties

As an initial object

The boolean domain object 2\mathbf{2} is an initial object in the category of bi-pointed objects.

Coproducts

The boolean domain object 2\mathbf{2} is the disjoint coproduct of the terminal object 11 with itself.

… (One should be able to define binary coproducts using the dependent sum functor and the boolean domain 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 boolean domain object is a two-valued topos. The internal logic of such a topos is two-valued logic.

Type theory

Boolean domain objects are the categorical semantics of the boolean domain in type theory. The inductive property of the boolean domain type, case analysis or if/else expressions, corresponds to the initiality of the boolean domain object in the subcategory of triples (A,t:1→A,f:1→A)(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→A,f:A→A)(A, q:1\rightarrow A, f:A\rightarrow A) representing infinite sequences.

See also

• natural numbers object

• bi-pointed object

• subobject classifier

• boolean domain

• two-valued topos, two-valued logic