Classically, a truth value is either (true) or (false), hence an element of the boolean domain.
(In constructive mathematics, this is not so simple, although it still holds that any truth value that is not true is false.)
More generally, a truth value in a topos is a morphism (where is the terminal object and is the subobject classifier) in . By definition of , this is equivalent to an (equivalence class of) monomorphisms . In a two-valued topos, it is again true that every truth value is either or , while in a Boolean topos this is true in the internal logic.
Truth values form a poset (the poset of truth values) by declaring that precedes iff the conditional is true. In a topos , precedes if the corresponding subobject is contained in . Classically (or in a two-valued topos), one can write this poset as .
The poset of truth values is a Heyting algebra. Classically (or internal to a Boolean topos), this poset is even a Boolean algebra. It is also a complete lattice; in fact, it can be characterised as the initial complete lattice. As a complete Heyting algebra, it is a frame, corresponding to the one-point locale.
When the set of truth values is equipped with the specialization topology, the result is Sierpinski space.
A truth value may be interpreted as a -poset or as a -groupoid. It is also the best interpretation of the term ‘-category’, although this doesn't fit all the patterns of the periodic table.
In synthetic topology with a dominance, some truth values are open.
homotopy level | n-truncation | homotopy theory | higher category theory | higher topos theory | homotopy type theory |
---|---|---|---|---|---|
h-level 0 | (-2)-truncated | contractible space | (-2)-groupoid | true/unit type/contractible type | |
h-level 1 | (-1)-truncated | contractible-if-inhabited | (-1)-groupoid/truth value | (0,1)-sheaf/ideal | mere proposition/h-proposition |
h-level 2 | 0-truncated | homotopy 0-type | 0-groupoid/set | sheaf | h-set |
h-level 3 | 1-truncated | homotopy 1-type | 1-groupoid/groupoid | (2,1)-sheaf/stack | h-groupoid |
h-level 4 | 2-truncated | homotopy 2-type | 2-groupoid | (3,1)-sheaf/2-stack | h-2-groupoid |
h-level 5 | 3-truncated | homotopy 3-type | 3-groupoid | (4,1)-sheaf/3-stack | h-3-groupoid |
h-level | -truncated | homotopy n-type | n-groupoid | (n+1,1)-sheaf/n-stack | h--groupoid |
h-level | untruncated | homotopy type | ∞-groupoid | (∞,1)-sheaf/∞-stack | h--groupoid |
Last revised on January 26, 2024 at 20:08:47. See the history of this page for a list of all contributions to it.