nLab
two-valued object

Two-valued object

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

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 2\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) 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 two-valued object is unique up to isomorphism.

Properties

As an initial object

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

Coproducts

The two-valued 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 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: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 March 21, 2021 at 10:53:16. See the history of this page for a list of all contributions to it.