nLab boolean domain object

Boolean domain object


Topos Theory

topos theory



Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory


Boolean domain object


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.


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

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

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


As an initial object

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


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.)


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

See also

Last revised on November 9, 2023 at 17:57:28. See the history of this page for a list of all contributions to it.