In logic, the true proposition, or truth, is the proposition which is always true.
The truth is commonly denoted $true$, $T$, $\top$, or $1$.
In classical logic, there are two truth values: true and false. Classical logic is perfectly symmetric between truth and falsehood; see de Morgan duality.
In constructive logic, $true$ is the top element in the poset of truth values.
Constructive logic is still two-valued in the sense that any truth value which is not true is false.
In terms of the internal logic of a topos (or other category), $true$ is the top element in the poset of subobjects of any given object (where each object corresponds to a context in the internal language).
However, not every topos is two-valued, so there may be other truth values besides $true$ and $false$.
In homotopy type theory the true is represented by any contractible type.
In the archetypical topos Set, the terminal object is the singleton set $\{*\}$ (the point) and the poset of subobjects of that is classically $\{\emptyset \hookrightarrow *\}$. Then truth is the singleton set $\{*\}$, seen as the improper subset of itself. (See Internal logic of Set for more details).
The same is true in the archetypical (∞,1)-topos ∞Grpd. From that perspective it makes good sense to think of
a set as a 0-truncated $\infty$-groupoid: a 0-groupoid;
a subsingleton set as a $(-1)$-truncated $\infty$-groupoid: a (−1)-groupoid;
the singleton set as the $(-2)$-truncated $\infty$-groupoid: the unique (up to equivalence) (−2)-groupoid.
In this sense, the object $true$ in Set or ∞Grpd may canonically be thought of as being the unique (−2)-groupoid.
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 |
h-level $n+2$ | $n$-truncated | homotopy n-type | n-groupoid | (n+1,1)-sheaf | h-$n$-groupoid |
h-level $\infty$ | untruncated | homotopy type | ∞-groupoid | (∞,1)-sheaf/∞-stack | h-$\infty$-groupoid |