Classically, a truth value is either (True) or (False). (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.
|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||(-1)-groupoid/truth value||(0,1)-sheaf||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||h-2-groupoid|
|h-level 5||3-truncated||homotopy 3-type||3-groupoid||(4,1)-sheaf||h-3-groupoid|