Subsection 1.2.2 (0008): $\webleft (-1\webright )$-Categories

Style	Class	Font	Theorem Environments
Style 1	`book`	Alegreya Sans	`tcbthm`
Style 2	`book`	Alegreya Sans	`amsthm`
Style 3	`book`	Arno*	`amsthm`
Style 4	`book`	Computer Modern	`amsthm`

1.2.2 $\webleft (-1\webright )$-Categories

Definition 1.2.2.1.1 ▶ $\webleft (-1\webright )$-Categories

A $\webleft (-1\webright )$-category is a classical truth value.

Remark 1.2.2.1.2 ▶ Motivation for $\webleft (-1\webright )$-Categories

^[1]$\webleft (-1\webright )$-categories should be thought of as being “categories enriched in $\webleft (-2\webright )$-categories”, having a collection of objects and, for each pair of objects, a $\textup{Hom}$-object $\textup{Hom}\webleft (x,y\webright )$ that is a $\webleft (-2\webright )$-category (i.e. trivial).

Therefore, a $\webleft (-1\webright )$-category $\mathcal{C}$ is either (pp. 33–34 of [Baez–Shulman, Lectures on $n$-Categories and Cohomology]):

Empty, having no objects;
Contractible, having a collection of objects $\webleft\{ a,b,c,\ldots \webright\} $, but with $\textup{Hom}_{\mathcal{C}}\webleft (a,b\webright )$ being a $\webleft (-2\webright )$-category (i.e. trivial) for all $a,b\in \text{Obj}\webleft (\mathcal{C}\webright )$, forcing all objects of $\mathcal{C}$ to be uniquely isomorphic to each other.

As such, there are only two $\webleft (-1\webright )$-categories, up to equivalence:

The $\webleft (-1\webright )$-category $\mathsf{false}$ (the empty one);
The $\webleft (-1\webright )$-category $\mathsf{true}$ (the contractible one).

Definition 1.2.2.1.3 ▶ The Poset of Truth Values

The poset of truth values^[2] is the poset $\smash {\webleft (\{ \mathsf{true},\mathsf{false}\} ,\preceq \webright )}$ consisting of

The Underlying Set. The set $\{ \mathsf{true},\mathsf{false}\} $ whose elements are the truth values $\mathsf{true}$ and $\mathsf{false}$.
The Partial Order. The partial order

\[ \preceq \colon \{ \mathsf{true},\mathsf{false}\} \times \{ \mathsf{true},\mathsf{false}\} \to \{ \mathsf{true},\mathsf{false}\} \]

on $\{ \mathsf{true},\mathsf{false}\} $ defined by ^[3]

\begin{align*} \mathsf{false}\preceq \mathsf{false}& \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathsf{true},\\ \mathsf{true}\preceq \mathsf{false}& \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathsf{false},\\ \mathsf{false}\preceq \mathsf{true}& \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathsf{true},\\ \mathsf{true}\preceq \mathsf{true}& \mathrel {\smash {\overset {\mathclap {\scriptscriptstyle \text{def}}}=}}\mathsf{true}. \end{align*}

Notation 1.2.2.1.4 ▶ Further Notation for The Poset of Truth Values

We also write $\{ \mathsf{t},\mathsf{f}\} $ for the poset $\{ \mathsf{true},\mathsf{false}\} $.

Proposition 1.2.2.1.5 ▶ Cartesian Closedness of the Poset of Truth Values

The poset of truth values $\{ \mathsf{t},\mathsf{f}\} $ is Cartesian closed with product given by ^[4]

\begin{align*} \mathsf{t}\times \mathsf{t}& = \mathsf{t},\\ \mathsf{t}\times \mathsf{f}& = \mathsf{f},\\ \mathsf{f}\times \mathsf{t}& = \mathsf{f},\\ \mathsf{f}\times \mathsf{f}& = \mathsf{f}, \end{align*}

and internal Hom $\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }$ given by the partial order of $\{ \mathsf{t},\mathsf{f}\} $, i.e. by

\begin{align*} \mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright ) & = \mathsf{t},\\ \mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright ) & = \mathsf{f},\\ \mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright ) & = \mathsf{t},\\ \mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright ) & = \mathsf{t}. \end{align*}

Proof of Proposition 1.2.2.1.5.

Existence of Products

We claim that the products $\mathsf{t}\times \mathsf{t}$, $\mathsf{t}\times \mathsf{f}$, $\mathsf{f}\times \mathsf{t}$, and $\mathsf{f}\times \mathsf{f}$ satisfy the universal property of the product in $\{ \mathsf{t},\mathsf{f}\} $. Indeed, consider the diagrams

Here:

If $P_{1}=\mathsf{t}$, then $p^{1}_{1}=p^{1}_{2}=\text{id}_{\mathsf{t}}$, and there’s indeed a unique morphism from $P_{1}$ to $\mathsf{t}$ making the diagram commute, namely $\text{id}_{\mathsf{t}}$;
If $P_{1}=\mathsf{f}$, then $p^{1}_{1}=p^{1}_{2}$ are given by the unique morphism from $\mathsf{f}$ to $\mathsf{t}$, and there’s indeed a unique morphism from $P_{1}$ to $\mathsf{t}$ making the diagram commute, namely the unique morphism from $\mathsf{f}$ to $\mathsf{t}$;
If $P_{2}=\mathsf{t}$, then there is no morphism $p^{2}_{2}$.
If $P_{2}=\mathsf{f}$, then $p^{2}_{1}$ is the unique morphism from $\mathsf{f}$ to $\mathsf{t}$ while $p^{2}_{2}=\text{id}_{\mathsf{f}}$, and there’s indeed a unique morphism from $P_{2}$ to $\mathsf{f}$ making the diagram commute, namely $\text{id}_{\mathsf{f}}$;
The proof for $P_{3}$ is similar to the one for $P_{2}$;
If $P_{4}=\mathsf{t}$, then there is no morphism $p^{4}_{1}$ or $p^{4}_{2}$.
If $P_{4}=\mathsf{f}$, then $p^{4}_{1}=p^{4}_{2}=\text{id}_{\mathsf{f}}$, and there’s indeed a unique morphism from $P_{4}$ to $\mathsf{f}$ making the diagram commute, namely $\text{id}_{\mathsf{f}}$.

Cartesian Closedness

We claim there’s a bijection

\[ \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (A\times B,C\webright )\cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (A,\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (B,C\webright )\webright ) \]

natural in $A,B,C\in \{ \mathsf{t},\mathsf{f}\} $. Indeed:

For $\webleft (A,B,C\webright )=\webleft (\mathsf{t},\mathsf{t},\mathsf{t}\webright )$, we have

\begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{t},\mathsf{t}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\\ & = \webleft\{ \text{id}_{\mathsf{true}}\webright\} \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\webright ). \end{align*}
For $\webleft (A,B,C\webright )=\webleft (\mathsf{t},\mathsf{t},\mathsf{f}\webright )$, we have

\begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{t},\mathsf{f}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\\ & = \emptyset \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\webright ). \end{align*}
For $\webleft (A,B,C\webright )=\webleft (\mathsf{t},\mathsf{f},\mathsf{t}\webright )$, we have

\begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{f},\mathsf{t}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \text{pt}\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\webright ). \end{align*}
For $\webleft (A,B,C\webright )=\webleft (\mathsf{t},\mathsf{f},\mathsf{f}\webright )$, we have

\begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{f},\mathsf{f}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \webleft\{ \text{id}_{\mathsf{false}}\webright\} \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\webright ). \end{align*}
For $\webleft (A,B,C\webright )=\webleft (\mathsf{f},\mathsf{t},\mathsf{t}\webright )$, we have

\begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{t},\mathsf{t}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \text{pt}\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\webright ). \end{align*}
For $\webleft (A,B,C\webright )=\webleft (\mathsf{f},\mathsf{t},\mathsf{f}\webright )$, we have

\begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{t},\mathsf{f}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \webleft\{ \text{id}_{\mathsf{false}}\webright\} \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\webright ). \end{align*}
For $\webleft (A,B,C\webright )=\webleft (\mathsf{f},\mathsf{f},\mathsf{t}\webright )$, we have

\begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{f},\mathsf{t}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \text{pt}\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\webright ). \end{align*}
For $\webleft (A,B,C\webright )=\webleft (\mathsf{f},\mathsf{f},\mathsf{f}\webright )$, we have

\begin{align*} \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{f},\mathsf{f}\webright ) & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & = \webleft\{ \text{id}_{\mathsf{false}}\webright\} \\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \textup{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\webright ). \end{align*}

The proof of naturality is omitted.

Footnotes

[1] For more motivation, see p. 13 of [Baez–Shulman, Lectures on $n$-Categories and Cohomology].

[2] Further Terminology: Also called the poset of $\webleft (-1\webright )$-categories.

[3] This partial order coincides with logical implication.

[4] Note that $\times $ coincides with the “and” operator, while $\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }$ coincides with the logical implication operator.

Noticed something off, or have any comments? Feel free to reach out!

You can also use the contact form below: