A $\webleft (-1\webright )$-category is a classical truth value.
3.2.2 $\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 $\operatorname {\mathrm{Hom}}$-object $\operatorname {\mathrm{Hom}}\webleft (x,y\webright )$ that is a $\webleft (-2\webright )$-category (i.e. trivial).
As a result, a $\webleft (-1\webright )$-category $\mathcal{C}$ is either:2
-
1.
Empty, having no objects.
-
2.
Contractible, having a collection of objects $\left\{ a,b,c,\ldots \right\} $, but with $\operatorname {\mathrm{Hom}}_{\mathcal{C}}\webleft (a,b\webright )$ being a $\webleft (-2\webright )$-category (i.e. trivial) for all $a,b\in \operatorname {\mathrm{Obj}}\webleft (\mathcal{C}\webright )$, forcing all objects of $\mathcal{C}$ to be uniquely isomorphic to each other.
Thus there are only two $\webleft (-1\webright )$-categories up to equivalence:
-
1.
The $\webleft (-1\webright )$-category $\mathsf{false}$ (the empty one);
-
2.
The $\webleft (-1\webright )$-category $\mathsf{true}$ (the contractible one).
- 1For more motivation, see p. 13 of [BS, Lectures on $n$-Categories and Cohomology].
- 2See pp. 33–34 of [BS, Lectures on $n$-Categories and Cohomology].
The poset of truth values1 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 by2
\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*}
- 1Further Terminology: Also called the poset of $\webleft (-1\webright )$-categories.
- 2This partial order coincides with logical implication.
We also write $\{ \mathsf{t},\mathsf{f}\} $ for the poset $\{ \mathsf{true},\mathsf{false}\} $.
The poset of truth values $\{ \mathsf{t},\mathsf{f}\} $ is Cartesian closed with product given by1
\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*}
- 1Note that $\times $ coincides with the “and” operator, while $\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }$ coincides with the logical implication operator.
Proof of Proposition 3.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, suppose we have diagrams of the form 
-
1.
If $P_{1}=\mathsf{t}$, then $p^{1}_{1}=p^{1}_{2}=\operatorname {\mathrm{id}}_{\mathsf{t}}$, so there’s a unique morphism from $P_{1}$ to $\mathsf{t}$ making the diagram commute, namely $\operatorname {\mathrm{id}}_{\mathsf{t}}$.
-
2.
If $P_{1}=\mathsf{f}$, then $p^{1}_{1}=p^{1}_{2}$ are given by the unique morphism from $\mathsf{f}$ to $\mathsf{t}$, so there’s a unique morphism from $P_{1}$ to $\mathsf{t}$ making the diagram commute, namely the unique morphism from $\mathsf{f}$ to $\mathsf{t}$.
-
3.
If $P_{2}=\mathsf{t}$, then there is no morphism $p^{2}_{2}$.
-
4.
If $P_{2}=\mathsf{f}$, then $p^{2}_{1}$ is the unique morphism from $\mathsf{f}$ to $\mathsf{t}$ while $p^{2}_{2}=\operatorname {\mathrm{id}}_{\mathsf{f}}$, so there’s a unique morphism from $P_{2}$ to $\mathsf{f}$ making the diagram commute, namely $\operatorname {\mathrm{id}}_{\mathsf{f}}$.
-
5.
The proof for $P_{3}$ is similar to the one for $P_{2}$.
-
6.
If $P_{4}=\mathsf{t}$, then there is no morphism $p^{4}_{1}$ or $p^{4}_{2}$.
-
7.
If $P_{4}=\mathsf{f}$, then $p^{4}_{1}=p^{4}_{2}=\operatorname {\mathrm{id}}_{\mathsf{f}}$, so there’s a unique morphism from $P_{4}$ to $\mathsf{f}$ making the diagram commute, namely $\operatorname {\mathrm{id}}_{\mathsf{f}}$.
This finishes the existence of products part of the proof.
Cartesian Closedness
We claim there’s a bijection
\[ \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (A\times B,C\webright )\cong \operatorname {\mathrm{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*} \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{t},\mathsf{t}\webright ) & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\\ & = \left\{ \operatorname {\mathrm{id}}_{\mathsf{true}}\right\} \\ & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{t}\webright )\\ & \cong \operatorname {\mathrm{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*} \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{t},\mathsf{f}\webright ) & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\\ & = \text{Ø}\\ & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t},\mathsf{f}\webright )\\ & \cong \operatorname {\mathrm{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*} \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{f},\mathsf{t}\webright ) & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \mathrm{pt}\\ & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \operatorname {\mathrm{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*} \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{t}\times \mathsf{f},\mathsf{f}\webright ) & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \left\{ \operatorname {\mathrm{id}}_{\mathsf{false}}\right\} \\ & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \operatorname {\mathrm{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*} \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{t},\mathsf{t}\webright ) & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \mathrm{pt}\\ & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \operatorname {\mathrm{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*} \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{t},\mathsf{f}\webright ) & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \left\{ \operatorname {\mathrm{id}}_{\mathsf{false}}\right\} \\ & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \operatorname {\mathrm{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*} \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{f},\mathsf{t}\webright ) & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \mathrm{pt}\\ & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{t}\webright )\\ & \cong \operatorname {\mathrm{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*} \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f}\times \mathsf{f},\mathsf{f}\webright ) & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & = \left\{ \operatorname {\mathrm{id}}_{\mathsf{false}}\right\} \\ & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\\ & \cong \operatorname {\mathrm{Hom}}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathbf{Hom}_{\{ \mathsf{t},\mathsf{f}\} }\webleft (\mathsf{f},\mathsf{f}\webright )\webright ). \end{align*}
Since $\{ \mathsf{t},\mathsf{f}\} $ is posetal, naturality is automatic (Chapter 11: Categories, Item 4 of Proposition 11.2.7.1.2).
