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

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

    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. 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. 1.

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

    2. 2.

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

    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*}


    1. 1Further Terminology: Also called the poset of $\webleft (-1\webright )$-categories.
    2. 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*}


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

    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
    where the $\operatorname {\mathrm{\mathrm{pr}}}_{1}$ and $\operatorname {\mathrm{\mathrm{pr}}}_{2}$ morphisms are the only possible ones (since $\{ \mathsf{t},\mathsf{f}\} $ is posetal). We claim that there are unique morphisms making the diagrams
    commute. Indeed:

    1. 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. 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. 3.

      If $P_{2}=\mathsf{t}$, then there is no morphism $p^{2}_{2}$.

    4. 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. 5.

      The proof for $P_{3}$ is similar to the one for $P_{2}$.

    6. 6.

      If $P_{4}=\mathsf{t}$, then there is no morphism $p^{4}_{1}$ or $p^{4}_{2}$.

    7. 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).


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


You can also use the contact form below: