Contents

(0,1)-category

(0,1)-topos

# Contents

## Idea

In logic, the true proposition, or truth, is the proposition which is always true.

The truth is commonly denoted $true$, $T$, $\top$, or $1$. These may be pronounced ‘true’ even where it would be ungrammatical for an adjective to appear in ordinary English.

## Definitions

### In classical logic

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

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 linear logic

In linear logic, there is both additive truth, denoted $\top$, and multiplicative truth, denoted $1$. As the notation suggests, it is $\top$ that is the top element of the lattice of linear truth values. (In particular, $1 \vdash \top$ but $\top \nvdash 1$.)

### In a topos

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 (even if it is boolean, so there may be other truth values besides $true$ and $false$.

### In type theory

In type theory with propositions as types, truth is represented by the unit type.

### In homotopy type theory

In homotopy type theory, truth is represented by any contractible type.

## Examples

### In the topos $Set$

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 leveln-truncationhomotopy theoryhigher category theoryhigher topos theoryhomotopy type theory
h-level 0(-2)-truncatedcontractible space(-2)-groupoidtrue/​unit type/​contractible type
h-level 1(-1)-truncatedcontractible-if-inhabited(-1)-groupoid/​truth value(0,1)-sheaf/​idealmere proposition/​h-proposition
h-level 20-truncatedhomotopy 0-type0-groupoid/​setsheafh-set
h-level 31-truncatedhomotopy 1-type1-groupoid/​groupoid(2,1)-sheaf/​stackh-groupoid
h-level 42-truncatedhomotopy 2-type2-groupoid(3,1)-sheaf/​2-stackh-2-groupoid
h-level 53-truncatedhomotopy 3-type3-groupoid(4,1)-sheaf/​3-stackh-3-groupoid
h-level $n+2$$n$-truncatedhomotopy n-typen-groupoid(n+1,1)-sheaf/​n-stackh-$n$-groupoid
h-level $\infty$untruncatedhomotopy type∞-groupoid(∞,1)-sheaf/​∞-stackh-$\infty$-groupoid

Last revised on February 16, 2017 at 10:43:05. See the history of this page for a list of all contributions to it.