The category structures on 2

• $\cattwo$ as a metacategory (CWM 1.1)
• $\cattwo$ as an internal category in $\Set$, i.e., $\cattwo\in\Cat(\Set)$ (CWM 1.2)
• $\cattwo$ as a category enriched in $\Set$, i.e., as a $\Set$-category, i.e., $\cattwo\in\Set$-$\Cat$ (CWM 1.8, 7.7)
• $\bftwo$ as a category enriched in itself, i.e., as a $\bftwo$-category, i.e., $\bftwo\in\bftwo$-$\Cat$ (BCECT 1.6.3)
• $\Set$ and $\cattwo$ as $\text{ccccc}$s - complete and cocomplete cartesian closed categories
• Relations between the categories

---

$\cattwo$ as a metacategory (CWM 1.1)

(The metacategory $\cattwo$) has data consisting of:
two objects, $\bot$ and $\top$, and three arrows, $1_\bot:\bot\to\bot$, ${\lt}:\bot\to\top$, and $1_\top:\top\to\top$
(${\lt}:\bot\to\top$ is of course usually denoted $\bot\lt\top$).
(Its identity arrows) are evident, and (its composition operation) is defined by (the unit axiom).
Note that no mention of sets has been made.

---

$\cattwo$ as an internal category in $\Set$, i.e., $\cattwo\in\Cat(\Set)$ (CWM 1.2)

(The internal category $\cattwo$ in $\Set$) has data consisting of
a set of objects $\boxed{\cattwo_0 = \{\bot,\top\}}$ and
a set of arrows $\boxed{\cattwo_1 = \{1_\bot,{\lt},1_\top\}}$,
together with (source, target, identity, and composition functions) which implement (the operations defined for the metacategory $\cattwo$).
The only difference between the definition of $\cattwo$ (as a metacategory) and (as an internal category in $\Set$) is (the explicit mention of sets and functions).

---

$\cattwo$ as a category enriched in $\Set$, i.e., as a $\Set$-category, i.e., $\cattwo\in\Set$-$\Cat$ (CWM 1.8, 7.7)

Again, we have the set of objects $\{\bot,\top\}$, now denoted by $\boxed{\ob\cattwo}$ (because the subscript $()_0$ will soon be given another meaning).
We also have a hom-function $\boxed{ \hom - \cattwo - : \ob\cattwo \times \ob\cattwo \to \Set}$,
taking each (pair of objects) to {the set of arrows from (the first, source, object) to (the second, target, object)}.
We represent the hom-function as a table:

target	$\top$		$\{\lt\}$	$\{1_\top\}$
	$\bot$		$\{1_\bot\} $	$\emptyset$
$\hom {\langle\text{source}\rangle} {\cattwo} {\langle\text{target}\rangle}$		$\bot$	$\top$
		source

---

$\bftwo$ as a category enriched in itself, i.e., as a $\bftwo$-category, i.e., $\bftwo\in\bftwo$-$\Cat$ (BCECT 1.6.3)

(The internal hom for $\bftwo$) is shown in (the center of the display below), where it can be easily compared to (some related functions).

The $\Set$-valued hom-function (the external hom) for the $\Set$-category $\cattwo$ target $\top$ $\{ \bot \xrightarrow{\textstyle \lt} \top \}$ $\{ \top \xrightarrow{\textstyle 1_\top} \top \}$ $\bot$ $\{ \bot \xrightarrow{\textstyle 1_\bot} \bot\}$ $\emptyset$ $\hom {\langle\text{source}\rangle} {\cattwo} {\langle\text{target}\rangle}$ $\bot$ $\top$ source	The $\bftwo$-valued hom-function (the internal hom) for the $\bftwo$-category $\bftwo$ target $\top$ $\top$ $\top$ $\bot$ $\top$ $\bot$ $\hom {\langle\text{source}\rangle} \bftwo {\langle\text{target}\rangle}$ or $[\langle\text{source}\rangle,\langle\text{target}\rangle]$ $\bot$ $\top$ source	The truth-table for implication ($\Rightarrow$) consequent $\top$ $\top$ $\top$ $\bot$ $\top$ $\bot$ $\langle\text{ant.}\rangle \Rightarrow \langle\text{cons.}\rangle$ $\bot$ $\top$ antecedent
	The $\Set$-valued hom-function for the full subcategory $\cal T$ (for “tiny”) determined by $\emptyset$ and $\{\emptyset\}$ of the $\Set$-category $\Set$ target $\{\emptyset\}$ $\big\{\emptyset\to\{\emptyset\}\big\}$ $\big\{\{\emptyset\} \xrightarrow{\textstyle 1_{\{\emptyset\}} } \{\emptyset\}\big\}$ $\emptyset$ $\big\{\emptyset \xrightarrow{\textstyle 1_\emptyset } \emptyset\big\}$ $\emptyset$ $\hom {\langle\text{source}\rangle} \Set {\langle\text{target}\rangle}$ or $[\langle\text{source}\rangle,\langle\text{target}\rangle]$ $\emptyset$ $\{\emptyset\}$ source

We can compare (the two $\Set$-categories, $\cattwo$ and $\Set$) to (the $\bftwo$-category $\bftwo$) with (the following two diagrams).
The labels above the arrows are the names of the arrows in the $\Set$-categories
(for the last arrow on each line, there is no label above, indicating that there is no such arrow in the $\Set$-category; the $\Set$ arrow $\emptyset\to\{\emptyset\}$ exists, but is here unnamed);
labels below arrows indicate the value of $\big( \hom {\langle\text{source}\rangle} \bftwo {\langle\text{target}\rangle} = [\langle\text{source}\rangle,\langle\text{target}\rangle] \big)$ for the indicated source and target. \[\begin{array}{ccccccccccl} \bot & \xrightarrow[\textstyle \top]{\textstyle 1_\bot} & \bot & \xrightarrow[\textstyle \top]{\textstyle \lt} & \top & \xrightarrow[\textstyle \top]{\textstyle 1_\top} & \top & \xrightarrow[\textstyle \bot]{} & \bot & \mkern6em & \cattwo \text{ above, } \bftwo \text{ below} \\ \\ \emptyset & \xrightarrow{\textstyle 1_\emptyset} & \emptyset & \xrightarrow{} & \{\emptyset\} & \xrightarrow{\textstyle 1_{\{\emptyset\}}} & \{\emptyset\} & \xrightarrow{} & \emptyset && \Set \text{ above} \\ \end{array}\]

There is a lot of information packed into those hom-tables. For example:
[That (the edge corresponding to ($\langle\text{source}\rangle=\bot$)) is all $\top$] is equivalent to ($\bot$ being initial in $\bftwo_0$).
[That (the edge corresponding to ($\langle\text{target}\rangle=\top$)) is all $\top$] is equivalent to ($\top$ being terminal in $\bftwo_0$).
[That (the edge corresponding to ($\langle\text{source}\rangle=\top$)) is identical to its input] is equivalent to ($[\top,-] \xlongequal{\textstyle i} 1_\bftwo$). (The letter $i$ comes from a generalization in the paper [CC].)
[That (the edge corresponding to ($\langle\text{target}\rangle=\bot$)) interchanges truth values] is equivalent to ($[-,\bot] = \neg$ (negation)).

---

The subscript $()_0$ changes meaning when going between (internal category theory) and (enriched category theory)

On the one hand, (an internal category $\catA$ in a category $\calE$) can be viewed as (a truncated simplicial object in $\calE$),
with $\catA_0$ = the object of objects, $\catA_1$ = the object of arrows, $\catA_2$ = the object of composable pairs of arrows, and $\catA_3$ = the object of composable triples of arrows.
That is a useful point of view, and it sets the meaning in internal category theory for $\catA_0$.

On the other hand, in (enriched category theory), there is a long tradition, starting with the Eilenberg-Kelly paper “Closed Categories” and continuing through Kelly’s basic text, Basic Concepts of Enriched Category Theory, where (the $()_0$ subscript) has a different meaning when applied to (an enriched category).
If $\catA$ is (an enriched category), $\catA_0$ is NOT ($\catA$’s set of objects) (Kelly denotes that by $\ob\catA$, while some other authors use $|\catA|$),
but rather ($\catA$’s underlying ordinary ($\Set$-enriched) category), as defined in section 1.3 of [BCECT].
We wish to emphasize (the enriched categorical point of view), so we adopt its notation.
Thus henceforth $\boxed{\bftwo_0}$ is not the mere set $\{\bot,\top\}$, but rather an isomorph of the ordinary category, and linear order, $\cattwo$.

---

$\bftwo$ and $\Set$ as $\text{ccccc}$s - complete and cocomplete cartesian closed categories

We assume as already known the fact that $\bftwo$ and $\Set$ are complete and cocomplete cartesian closed categories, whose operations include:

$\bftwo$ and $\Set$ as $\text{ccccc}$s (complete and cocomplete cartesian closed categories)

		completeness				cocompleteness				internal hom
arity:		nullary	binary	arbitrary		nullary	binary	arbitrary		binary
$\bftwo$		$\top$	$\wedge$	$\forall$ or $\bigwedge$		$\bot$	$\vee$	$\exists$ or $\bigvee$		$\Rightarrow$
$\Set$		$1$	$\times$	$\displaystyle\prod$		$\emptyset$	$+$	$\sum$ or $\displaystyle\coprod$		$[,]$

We denote the internal hom in $\Set$ (the set of functions from, say, set $\setX$ to set $\setY$), often denoted by exponentiation $\setY^\setX$, by $[\setX,\setY]$.
The other operations necessary for completeness and cocompleteness in $\Set$ are equalizers and coequalizers.
For $\Set$ equalizers are easy, while coequalizers involve completing a parallel pair of functions into an equivalence relation, then taking the quotient of that relation.

---

References

CWM, Mac Lane, Saunders, Categories for the Working Mathematician (1971,1998)
BCECT, Kelly, Max, Basic Concepts of Enriched Category Theory (1982/2005)
CC, Eilenberg and Kelly, “Closed Categories” (1966)
NAMC, Janelidze and Kelly, “Note on Actions of a Monoidal Category” (2001)

---

Draft stuff:

---

Relations between the categories

This section is a rough draft:

From (the total order $\cattwo$) to (the $\bftwo$-category $\bftwo$):
The total order $(\cattwo,{\le})$ has
binary products = binary meets = conjunction = $\land$,
and, for each $\objB\in\cattwo$, the order-preserving function $\boxed{-\land\objB : \cattwo\to\cattwo}$
has a right adjoint, denoted $\boxed{\objB\Rightarrow -}$ or $\boxed{[\objB,-]}$ or, combining the previous two notations, $\boxed{[\objB\Rightarrow-]}$ , thus we have:
\[ \pi: \big( \objA\land\objB \le \objC \big) \text{ iff } \big( \objA \le [\objB\Rightarrow\objC] \big), \mkern6em \text{a special case of} \mkern6em \hom {\objectA\tensor\objectB} {(\cal V_0)} {\objectC} \mathop\cong\limits^{\textstyle\pi}_{\text{II, $\S$3}} \hom \objectA {(\cal V_0)} {[\objectB,\objectC]} \mkern6em \text{for $\calV_0 = \cattwo$} \;. \]

From (the $\bftwo$-category $\bftwo$) to (its underlying total order $\bftwo_0$):
Given the internal hom $[,]$, i.e., $\Rightarrow$, define \[ v: \big( \objA\le\objB \big) \text{ iff } \big( \top = [\objA\Rightarrow\objB] \big), \mkern6em \text{which is almost a special case of} \mkern6em \hom \objectA {(\cal V_0)} {\objectB} \mathop\cong\limits^{\textstyle v}_{\text{II (3.12)}} \hom \objectI {(\cal V_0)} {[\objectA,\objectB]} \;. \] (The general cases indicated above) are standard situations in (the theory of closed categories; see section II.3 of [CC]).
The references below the $\cong$ symbols are references to that paper.
The “almost” qualifier is required because (the situation in which it appears) is (a definition of $\le$ in $\cal V_0$), not (an isomorphism between already existing objects).
(The order relation thus defined on $\{\bot,\top\}$) is exactly the same as (that given by fiat on $\{\bot,\top\}$ in the definition of $\cattwo$ as a metacategory, etc.).
Thus $\bftwo_0$ and $\cattwo$ are isomorphic total orders.

---

\[\begin{array}{} \boxed{\begin{array}{} \textstyle \ar\cattwo \atop {\Rule{2em}{1px}{1px}} \\ 1_\bot \\ \lt \\ 1_\top \\ \end{array}} & \cong & \boxed{\begin{array}{} {\textstyle \le_2} \atop {\Rule{3em}{1px}{1px}} \\ \langle\bot,\bot\rangle \\ \langle\bot,\top\rangle \\ \langle\top,\top\rangle \\ \end{array}} & \cong & \mkern2em \boxed{\begin{array}{} \textstyle \ar(\bftwo_0) \atop {\Rule{4em}{1px}{1px}} \\ \top=\hom \bot\bftwo\bot \\ \top=\hom \bot\bftwo\top \\ \top=\hom \top\bftwo\top \\ \end{array}} & \to & 1 \\ & \searrow & \big\downarrow & \swarrow && \lrcorner & \big\downarrow \rlap\top \\ 1 & \xrightarrow{\textstyle \langle\objectA,\objectB\rangle} & \boxed{\begin{array}{} \{\bot,\top\} \times \{\bot,\top\} \\ \langle\bot,\bot\rangle \\ \langle\bot,\top\rangle \\ \langle\top,\top\rangle \\ \langle\top,\bot\rangle \\ \end{array}} & {}\rlap{\xrightarrow[\boxed{\begin{array}{} \textstyle \hom - \bftwo - \\ [,]_2 \\ \Rightarrow_2 \\ \le_2 \\ \end{array}} ]{\mkern13em}} &&& \boxed{\begin{array}{} \{\bot,\top\} \\ \bot \\ \top \\ \end{array}} \\ && \llap{\text{projections from cartesian product}} \bigg\downarrow \bigg\downarrow \\ && \boxed{\begin{array}{} \{\bot,\top\} \\ \bot \\ \top \\ \end{array}} \\ \end{array}\]

2 as the Boolean subobject classifier

Version of 2019-01-07:

Our aim is to illustrate the meaning of the term “subobject classifier” (Wikipedia, nLab)
by giving some examples of how the set $\bftwo = \{\ladjbot, \radjtop\}$
serves as a (“the”) subobject classifier in the familiar Boolean topos $\Set$.
Notation: The symbol “$\lrcorner$” indicates that (the square in which it is contained) is (a pullback square),
with (the pullback object) being (that which is bounded by the “$\lrcorner$”).

---

Basic examples of subobject classification

$\bbox[2ex, border:1px black solid] { \begin{array}{} && \emptyset & \xrightarrow[]{} & \bfone \\ && \llap{\emptyset = 1_\emptyset} \Big\Vert & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow\rlap\radjtop & \\ && \emptyset & \xrightarrow[\displaystyle \emptyset]{} &\bftwo \\ \end{array} }$				$2^0 = {0 \choose 0} = 1$
$\bbox[2ex, border:1px black solid] { \begin{array}{} & \emptyset & \xrightarrow[]{} & \bfone \\ & \llap{\emptyset}\Big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow\rlap\radjtop & \\ & \bfone & \xrightarrow[\displaystyle \ladjbot]{} &\bftwo \\ \end{array} }$			$\bbox[2ex, border:1px black solid] { \begin{array}{} & \bfone & \xrightarrow[]{} & \bfone \\ & \llap{1_\bfone} \Big\Vert & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow\rlap\radjtop & \\ & \bfone & \xrightarrow[\displaystyle \radjtop]{} &\bftwo \\ \end{array} }$	$2^1 = {1 \choose 0} + {1 \choose 1} = 1 + 1 = 2$
$\bbox[2ex, border:1px black solid] { \begin{array}{} & \emptyset & \xrightarrow[]{} & \bfone \\ & \llap{\emptyset}\Big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow\rlap\radjtop & \\ & \bftwo & \xrightarrow[\displaystyle !\ladjbot]{} &\bftwo \\ \end{array} }$	$\bbox[2ex, border:1px black solid] { \begin{array}{} \{\radjtop\} \cong \bfone & \xrightarrow[]{} & \bfone \\ \llap{\radjtop}\Big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow\rlap\radjtop & \\ \bftwo & \xrightarrow[\displaystyle 1_\bftwo]{} &\bftwo \\ \end{array} }$	$\bbox[2ex, border:1px black solid] { \begin{array}{} \{\ladjbot\} \cong \bfone & \xrightarrow[]{} & \bfone \\ \llap{\ladjbot}\Big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow\rlap\radjtop & \\ \bftwo & \xrightarrow[\displaystyle \neg\vphantom{1_\bftwo}]{} &\bftwo \\ \end{array} }$	$\bbox[2ex, border:1px black solid] { \begin{array}{} & \bftwo & \xrightarrow[]{} & \bfone \\ & \llap{1_\bftwo} \Big\Vert & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow\rlap\radjtop & \\ & \bftwo & \xrightarrow[\displaystyle !\radjtop]{} &\bftwo \\ \end{array} }$	$\begin{array}{l} 2^2 = (1+1)^2 = (1+1)\cdot(1+1) = \\ = 1\cdot 1 + 1\cdot 1 + 1\cdot 1 + 1\cdot 1 = \\ = 1 + 1 + 1 + 1 = \\ = {2\choose 0} + {2\choose 1} + {2\choose 2} = 1+2+1 =4\\ \bftwo^2 \cong (\ladjbot+\radjtop)^2 = (\ladjbot+\radjtop) \times (\ladjbot+\radjtop) \cong \\ {} \cong \ladjbot\times\ladjbot + \ladjbot\times\radjtop + \radjtop\times\ladjbot + \radjtop\times\radjtop \sim \\ {} \sim {!\ladjbot} + 1_\bftwo + {\neg} + {!\radjtop} \\ \end{array}$
$\bbox[2ex, border:1px black solid] { \begin{array}{lccc} \text{graph} & \radjtop \\ \text{of }\mkern.25em !\ladjbot & \ladjbot & \text{X} & \text{X} \\ \text{output} & & \ladjbot & \ladjbot \\ \text{input} & & \ladjbot & \radjtop \\ \end{array} }$	$\bbox[2ex, border:1px black solid] { \begin{array}{lccc} \text{graph} & \radjtop & & \class {red} {\text{X}} \\ \text{of }\mkern.25em 1_\bftwo & \ladjbot & \text{X} \\ \text{output} & & \ladjbot & \class {red} {\radjtop} \\ \text{input} & & \ladjbot & \radjtop \\ \end{array} }$	$\bbox[2ex, border:1px black solid] { \begin{array}{lccc} \text{graph} & \radjtop & \class {red} {\text{X}} \\ \text{of }\mkern.25em \neg & \ladjbot & & \text{X} \\ \text{output} & & \class {red} {\radjtop} & \ladjbot \\ \text{input} & & \ladjbot & \radjtop \\ \end{array} }$	$\bbox[2ex, border:1px black solid] { \begin{array}{lccc} \text{graph} & \radjtop & \class {red} {\text{X}} & \class {red} {\text{X}} \\ \text{of }\mkern.25em !\radjtop & \ladjbot \\ \text{output} & & \class {red} {\radjtop} & \class {red} {\radjtop} \\ \text{input} & & \ladjbot & \radjtop \\ \end{array} }$

---

General theorem: 2 is a subobject classifier for Set

For an arbitrary set $\setX\in\Set$, there is a bijection $\Sub(\setX) \cong \hom \setX \Set \bftwo$.
The correspondence between (subsets $\setA \subseteq \setX$, which are also denoted $i_\setA : \setA \rightarrowtail \setX$) and ($\bftwo$-valued predicates $\functionA : \setX \to \bftwo$) is given by:

From subsets to predicates		From predicates to subsets
$\bbox[2ex, border:1px black solid] { \begin{array}{} & \functionA & \xrightarrow[]{\displaystyle !} & \bfone \\ & \llap{i_\setA}\Big\downarrow & \mkern-10em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow\rlap\radjtop & \\ & X & \xrightarrow[ \displaystyle \boxed{ \begin{array}{} ?\in\functionA\\ (\exists\elta\in\setA)(?=\elta) \\ (\exists\elta)(\elta\in\setA \wedge {?=\elta} \wedge \radjtop) \\ \int^{\elta\in\setA} \hom ? \setX \elta \otimes {!\radjtop} \\ \Lan_{i_\setA} !\radjtop \\ \end{array} } ]{} &\bftwo \\ \end{array} }$		$\bbox[2ex, border:1px black solid] { \begin{array}{} & \boxed{ \begin{array}{} \{ \eltx \mid \functionA_\eltx \}\\ \{ \eltx \mid \functionA_\eltx = \radjtop \}\\ \functionA^{-1}\radjtop\\ \end{array} } & \xrightarrow[]{\displaystyle !} & \bfone \\ & \llap{}\Big\downarrow & \mkern-3em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow\rlap\radjtop & \\ & X & \xrightarrow[\displaystyle \functionA]{} &\bftwo \\ \end{array} }$

Elementary Boolean geometry and logic

Version of 2019-01-11

Draft Outline

The basic building block for Boolean geometry and logic
is the Boolean “object of truth values”: $\bftwo = \{\ladjbot,\radjtop\} = \{\text{false},\text{true}\}$.
We give this set the (linear) order $\ladjbot\lt\radjtop$, in accordance with the ex falso sequitur quodlibet principle of logic.

Boolean geometry then considers powers of $\bftwo$:

the Boolean point	$\bftwo^0 \cong 1$ ,
the Boolean line	$\bftwo^1 \cong \bftwo$ ,
the Boolean plane	$\bftwo^2 \cong \bftwo\times\bftwo$ ,
the Boolean cube	$\bftwo^3\cong \bftwo\times\bftwo\times\bftwo$ , and so on.

The next step is to consider Boolean (i.e., $\bftwo$-valued) functions (which we will call predicates) defined on these geometric objects.
Since (the Boolean object of truth values, $\bftwo$) is (the subobject classifier) for (the category of sets),
such predicates are in bijection with
the subsets of (the source (domain) of the predicate).

---

A comparison of the traditional way of presenting truth tables to
the geometrical way (the graph of the function from $\bftwo\times\bftwo$ to $\bftwo$ determined by the truth table):

Truth table for $\objA\wedge\objB$

$\objA$ $\objB$ $\objA\wedge\objB$ $\radjtop$ $\radjtop$ $\radjtop$ $\ladjbot$ $\radjtop$ $\ladjbot$ $\radjtop$ $\ladjbot$ $\ladjbot$ $\ladjbot$ $\ladjbot$ $\ladjbot$

The graph of the function $\wedge : \bftwo\times\bftwo \rightarrow \bftwo$

$\objB$ $\radjtop$ $\ladjbot$ $\Rule{64px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\objA\wedge\objB$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{64px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$

---

The main point of this document is the relation between the geometry of the Boolean square $\bftwo\times\bftwo$ and Boolean logic;
however for future use it is of great value to show exactly how the four edges of the Boolean square are in fact instances of the categorical notion of pullback.
To that end, the display below shows at the right the vertices and edges of the Boolean square, and labels them appropriately for their use in logic,
while to the left appear the pullback diagrams in the category $\Set$ which exhibit those edges as pullbacks.

Pullback diagrams in $\Set$		The Boolean square $\bftwo\times\bftwo$
$\begin{array}{} \boxed{\begin{array}{} \pi_1^{-1} \ladjbot\\ \ladjbot\times\bftwo\\ \end{array}} & \xrightarrow{\textstyle \ladjbot\times\bftwo} & \bftwo\times\bftwo & \xleftarrow{\textstyle \radjtop\times\bftwo} & \boxed{\begin{array}{} \pi_1^{-1} \radjtop\\ \radjtop\times\bftwo\\ \end{array}} \\ \Big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \llap{\pi_1} \Big\downarrow & \mkern+1.8em{\raise2ex\hbox{$\llcorner$}} & \Big\downarrow \\ \bfone & \xrightarrow[\textstyle \ladjbot]{} & \bftwo & \xleftarrow[\textstyle \radjtop]{} & \bfone \\ \end{array}$	$\begin{array}{} \boxed{\begin{array}{} \pi_2^{-1} \radjtop\\ \bftwo\times\radjtop\\ \end{array}} & \xrightarrow{} & \bfone \\ \llap{\bftwo\times\radjtop} \Big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow \rlap{\radjtop} \\ \bftwo\times\bftwo & \xrightarrow[\textstyle \pi_2]{} & \bftwo \\ \llap{\bftwo\times\ladjbot} \Big\uparrow & \mkern-1.8em{\lower2ex\hbox{$\urcorner$}} & \Big\uparrow \rlap{\ladjbot} \\ \boxed{\begin{array}{} \pi_2^{-1} \ladjbot\\ \bftwo\times\ladjbot\\ \end{array}} & \xrightarrow{} & \bfone \\ \end{array}$	$\objB\in\{\ladjbot,\radjtop\}$ $\vary\in\{0,1\}$ $\Big\uparrow$ $\boxed{ \begin{array}{} \bftwo\times\radjtop\\ \objB\\ \end{array} }$ $1$ $\top$ $\boxed{ \begin{array}{c}\langle \ladjbot, \radjtop \rangle\\\objB - \objA\\\end{array} }$ $\Rule{64px}{2px}{0px}$ $\boxed{ \begin{array}{c}\langle \radjtop, \radjtop \rangle\\\objA\cap\objB\\\end{array} }$ $\boxed{ \begin{array}{} \ladjbot\times\bftwo\\ \neg\objA\\ \end{array} }$ $\Rule{2px}{32px}{32px}$ $\Rule{2px}{32px}{32px}$ $\boxed{ \begin{array}{} \radjtop\times\bftwo\\ \objA\\ \end{array} }$ $0$ $\bot$ $\boxed{ \begin{array}{c}\langle \ladjbot, \ladjbot \rangle\\ \neg\objA\wedge\neg\objB\\ \end{array} }$ $\Rule{64px}{2px}{0px}$ $\boxed{ \begin{array}{c}\langle \radjtop, \ladjbot \rangle\\\objA - \objB\\\end{array} }$ $\longrightarrow \objA\in\{\ladjbot,\radjtop\}, \varx\in\{0,1\}$ $\bot$ $\boxed{ \begin{array}{} \bftwo\times\ladjbot\\ \neg\objB\\ \end{array} }$ $\top$ $0$ $1$

---

${2\times2 \choose 4} = 1$	all			$\objB$ $\radjtop$ $\radjtop$ $\Rule{64px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\radjtop\\1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{64px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$
${2\times2 \choose 3} = 4$	ells angles		$\objB$ $\radjtop$ $\radjtop$ $\Rule{128px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA\vee\objB\\ \neg(\neg\objA\wedge\neg\objB)\\ (\varx+1)(\vary+1)+1\\ \varx\vary+\varx+\vary\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{128px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\radjtop$ $\Rule{96px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA\Rightarrow\objB\\\neg\objA\vee\objB\\\neg(\objA\wedge\neg\objB)\\\varx(\vary+1)+1\\\varx\vary+\varx+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{96px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\ladjbot$ $\Rule{96px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA\Leftarrow\objB\\\objA\vee\neg\objB\\\neg(\neg\objA\wedge\objB)\\(\varx+1)\vary+1\\\varx\vary+\vary+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{96px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\radjtop$ $\Rule{128px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\neg\objA\vee\neg\objB\\\neg(\objA\wedge\objB)\\\varx\vary+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{128px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$
${2\times2 \choose 2} = 6$	lines	$\objB$ $\radjtop$ $\ladjbot$ $\Rule{64px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA\\\varx\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{64px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\radjtop$ $\Rule{128px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objB\\\vary\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{128px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\ladjbot$ $\Rule{96px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA\Leftrightarrow\objB\\\varx+\vary+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{96px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\radjtop$ $\Rule{96px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA \veebar\objB\\\varx+\vary\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{96px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\ladjbot$ $\Rule{128px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\neg\objB\\\vary+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{128px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\radjtop$ $\Rule{64px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\neg\objA\\\varx+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{64px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$
${2\times2 \choose 1} = 4$	points vertices		$\objB$ $\radjtop$ $\ladjbot$ $\Rule{128px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA\wedge\objB\\\varx\vary\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{128px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\radjtop$ $\Rule{96px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c} \objB-\objA\\ \neg\objA\wedge\objB\\ (\varx+1)\vary\\ \varx\vary+\vary\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{96px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\ladjbot$ $\Rule{96px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c} \objA-\objB\\ \objA\wedge\neg\objB\\ \varx(\vary+1)\\ \varx\vary+\varx\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{96px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\ladjbot$ $\Rule{128px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c} \neg\objA\wedge\neg\objB\\ (\varx+1)(\vary+1)\\ \varx\vary+\varx+\vary+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{128px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$
${2\times2 \choose 0} = 1$	none			$\objB$ $\radjtop$ $\ladjbot$ $\Rule{64px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c} \ladjbot\\ 0\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{64px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$

---

\[\begin{array}{} &&& dot & \unicode{0x2500} & dot \\ && \unicode{0x2571} && \unicode{0x2571} \\ & dot & \unicode{0x2500} & dot \\ \\ && dot & \unicode{0x2500} & dot \\ & \unicode{0x2571} && \unicode{0x2571} \\ dot & \unicode{0x2500} & dot \\ \end{array}\]

---

\[\begin{array}{} dot & \unicode{0x2500} & dot \\ & \unicode{0x2572} && \unicode{0x2572} \\ && dot & \unicode{0x2500} & dot \\ \\ & dot & \unicode{0x2500} & dot \\ && \unicode{0x2572} && \unicode{0x2572} \\ &&& dot & \unicode{0x2500} & dot \\ \end{array}\]

Boolean structures: from 2 to predicates to subsets, and back

Background: $\Newextarrow{\xleftrightarrow}{10,10}{0x2194}$
For the predicate/subset bijection, and the nullary and unary logical operations on $\bftwo$, see “$\bftwo$ as the Boolean subobject classifier”.
For the binary logical operations on $\bftwo$ (“the Boolean logical connectives”), see “Elementary Boolean geometry and logic”.

---

Inputs:
Inputs are two predicate/subset pairs, $\objA$ and $\objB$, on a given set $\setX\in\Set$, as shown below, embedded as the right squares in $2 \times 3$ diagrams.
Also shown are two noteworthy special cases, which will be used in the sequel.

$\begin{array}{} \objA\times\objX & \xrightarrow{} & \objA & \xrightarrow{} & \bfone \\ \llap{i_\objA \times\objX} \downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \llap{i_\objA} \downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \downarrow\rlap\radjtop \\ \objX\times\objX & \xrightarrow[\textstyle \pi_1]{} & \objX & \xrightarrow[\textstyle \objA]{} & \bftwo \\ \end{array}$

$\begin{array}{} \objX\times\objB & \xrightarrow{} & \objB & \xrightarrow{} & \bfone \\ \llap{\objX \times i_\objB} \downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \llap{i_\objB} \downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \downarrow\rlap\radjtop \\ \objX\times\objX & \xrightarrow[\textstyle \pi_2]{} & \objX & \xrightarrow[\textstyle \objB]{} & \bftwo \\ \end{array}$

$\begin{array}{} \radjtop\times\bftwo & \xrightarrow{} & \bfone \\ \llap{\radjtop\times\bftwo} \downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \downarrow\rlap\radjtop \\ \bftwo\times\bftwo & \xrightarrow[\textstyle \pi_1]{} & \bftwo \\ \end{array}$

$\begin{array}{} \bftwo\times\radjtop & \xrightarrow{} & \bfone \\ \llap{\bftwo\times\radjtop} \downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \downarrow\rlap\radjtop \\ \bftwo\times\bftwo & \xrightarrow[\textstyle \pi_2]{} & \bftwo \\ \end{array}$

---

Internal:

(Intersection of subsets) and (conjunction of predicates)
(the internal operations in $\Set$) $$\begin{array}{} &&& \eltx \in (\setA\cap\setB) & \xleftrightarrow{} & {\eltx\in\setA} \wedge {\eltx\in\setB} \\ \\ \begin{array}{l} \text{Intersection}\\ \text{of subsets}\\ \text{(internal)}\\ \end{array} &&& \boxed{\begin{array}{} \\ \setA \cap \setB\\ \\ \{ \eltx\in\setX \mid {{\eltx\in\setA} \wedge {\eltx\in\setB} \} }\\ \end{array} } & \longrightarrow & \boxed{ \begin{array}{} \pi_1^{-1}\objA \cap \pi_2^{-1}\objB \\ \setA\times\setX \cap \setX\times\setB\\ \setA \times \setB\\ \{ \langle\eltx,\elty\rangle \in \setX\times\setX \mid {{\eltx\in\setA} \wedge {\elty\in\setB} \} }\\ \end{array} } & \xrightarrow[]{} & \boxed { \begin{array}{} \pi_1^{-1}\radjtop \cap \pi_2^{-1}\radjtop \\ {\radjtop\times\bftwo} \cap {\bftwo\times\radjtop} \\ \radjtop\times\radjtop \\ \{ \langle \radjtop, \radjtop \rangle \} \\ \end{array} } & \xrightarrow[]{} & \bfone \\ &&& \Big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow & \mkern-1.8em{\raise2ex\hbox{$\lrcorner$}} & \Big\downarrow\rlap\radjtop \\ & \eltx & \in & \setX & \xrightarrow[\textstyle \Delta]{} & \setX \times \setX & \xrightarrow[\textstyle \setA\times\setB]{} & \bftwo \times \bftwo & \xrightarrow[\textstyle \boxed{ \begin{array}{}\wedge\\ \pi_1\wedge\pi_2\\ \end{array} } ]{} & \bftwo & \ni & {{\setA_\eltx} \wedge {\setB_\eltx}} \\ &&& \Vert &&&& \Vert \\ &&& \setX && \xrightarrow[\textstyle \langle\functionA,\functionB\rangle]{} && \bftwo \times \bftwo \\ \begin{array}{l} \text{Conjunction}\\ \text{of predicates}\\ \text{(internal)}\\ \end{array} & \Bigg\Vert && \Bigg\Vert &&&&&& \Bigg\Vert && \Bigg\Vert \\ & \eltx & \in & \setX &&& \xrightarrow[\textstyle \; \boxed{\setA\wedge\setB} \; ]{} &&& \bftwo & \ni & {(\setA\wedge\setB)_\eltx} \\ \end{array}$$

---

External plus internal:

(Intersection of subsets) and (conjunction of predicates)
(the external operations on $\Set$, plus projections/evaluations to the internal Boolean algebra $\bftwo$) $$\begin{array}{lcccccccccccc} \text{Intersection of subsets (external)} && \langle\setA,\setB\rangle & \in & \Sub(\setX) \times \Sub(\setX) && \xrightarrow{\textstyle \boxed\cap} && \Sub(\setX) & \ni & \setA\cap\setB \\ && \wr && \Vert\wr &&&& \Vert\wr && \wr \\ && \langle\functionA,\functionB\rangle & \in & \hom \setX \Set \bftwo \times \hom \setX \Set \bftwo & \xrightarrow[\textstyle \times]{} & \hom {\setX\times\setX} \Set {\bftwo\times\bftwo} & \xrightarrow[\textstyle \hom \Delta \Set \wedge]{} & \hom \setX \Set \bftwo & \ni & \functionA \wedge \functionB \\ \text{Conjunction of predicates (external)} && \Vert && \Vert &&&& \Vert && \Vert \\ && \langle\functionA,\functionB\rangle & \in & \hom \setX \Set \bftwo \times \hom \setX \Set \bftwo && \xrightarrow[\textstyle \boxed\wedge]{} && \hom \setX \Set \bftwo & \ni & \functionA \wedge \functionB \\ && \mapsdownto && \Big\downarrow \rlap{\mkern-2.1em E_\eltx\times E_\eltx} &&&& \Big\downarrow \rlap{E_\eltx} && \mapsdownto \\ \text{Conjunction in $\bftwo$ (internal)} && \langle \functionA_\eltx,\functionB_\eltx \rangle & \in & \bftwo\times\bftwo && \xrightarrow[\textstyle \boxed\wedge]{} && \bftwo & \ni & \functionA_\eltx \wedge \functionB_\eltx \\ \end{array}$$

---

The above shows how, given a function in $\Set$ from $\bftwo\times\bftwo$ to $\bftwo$ (an internal binary operation on $\bftwo$),
that function generates binary operations on $\hom \objX \Set \bftwo$ and $\Sub(X)$, for arbitrary sets $\objX\in\Set$ (which in fact are natural with respect to $\setX\in\Set\op$),
a process we call extension.
The process may be reversed.
First, binary operations on $\hom \objX \Set \bftwo$ and $\Sub(X)$ are in bijection, using the predicate/subset bijection.
Second, any binary operation on $\hom \objX \Set \bftwo$ yields a binary operation on $\bftwo$,
by applying the operation to the specific predicates $\pi_1, \pi_2 : \bftwo\times\bftwo \to \bftwo$, a process we call restriction.
If we restrict to binary operations on $\hom \objX \Set \bftwo$ and $\Sub(X)$ which satisfy the categorical condition of naturality,
then these two processes are inverse to each other.
For example, evaluating (the construction of conjunction for predicates) on (the specific predicates $\pi_1, \pi_2 : \bftwo\times\bftwo \to \bftwo$), we have: $$\begin{array}{} \objA,\objB & \xmapsto{} & \objA,\objB,\objA,\objB & \xmapsto{} & \objA,\objB & \xmapsto{} & \objA\wedge\objB \\ \bftwo\times\bftwo && \xrightarrow{\textstyle \text{identity}} && \bftwo\times\bftwo \\ \Vert &&&& \Vert \\ \bftwo\times\bftwo & \xrightarrow[\textstyle \Delta]{} & \bftwo\times\bftwo\times\bftwo\times\bftwo & \xrightarrow[\textstyle \pi_1 \times \pi_2]{} & \bftwo\times\bftwo & \xrightarrow[\textstyle \wedge]{} & \bftwo \\ \Vert &&&&&& \Vert \\ \bftwo\times\bftwo &&& \xrightarrow[\textstyle \pi_1\wedge\pi_2]{} &&& \bftwo\times\bftwo \\ \end{array}$$ thus $\boxed{\pi_1\wedge\pi_2 = \wedge}$, thus extension followed by restricting gives the original function.
To prove the other direction, that first restricting, then extending, gives the original, is more complex.
A proof of that, in greater generality, is at my discussion of the identities-are-free (Yoneda) lemma.

---

Pullback preserves the Boolean structure,
e.g., given a function in $\Set$, $\functionf:\setX\to\setY$,
completing the diagram at left below in either of the two evident ways yields isomorphic results

$\begin{array}{} & \rightarrow & \functionf^{-1}\objBp \\ & \searrow && \searrow \\ && \functionf^{-1}\objB & \rightarrow & \objX\\ \\ & \objB\cap\objBp & \rightarrow & \objBp\\ && \searrow && \searrow & \Bigg\downarrow\rlap\functionf \\ &&& \objB & \rightarrow & \objY \\ \end{array} \mkern1em $ for we have $ \mkern1em \begin{array}{} \eltx \in (\functionf^{-1}\objB \cap \functionf^{-1}\objB') & \xleftrightarrow{\textstyle \cap} & \eltx\in\functionf^{-1}\objB \wedge \eltx\in\functionf^{-1}\objB' \\ \\ \eltx\in\functionf^{-1}(\objB\cap\objB') && \updownarrow \rlap{\functionf^{-1}} \\ \llap{\functionf^{-1}} \updownarrow \\ \eltx\functionf \in \objB\cap\objB' & \xleftrightarrow[\textstyle \cap]{} & \eltx\functionf\in\objB \wedge \eltx\functionf \in \objB' \\ \end{array} \mkern1em $ or $ \mkern1em \begin{array}{} (\functionf^{-1}\objB \wedge \functionf^{-1}\objB')_\eltx & \xlongequal{\textstyle \wedge} & (\functionf^{-1}\objB)_\eltx \wedge (\functionf^{-1}\objB')_\eltx \\ \\ \big(\functionf^{-1}(\objB\wedge\objB')\big)_\eltx && \Vert \rlap{\;\functionf^{-1}} \\ \llap{\functionf^{-1}} \Vert \\ (\objB\wedge\objB')_{\eltx\functionf} & \xlongequal[\textstyle \wedge]{} & \objB_{\eltx\functionf} \wedge {\objB'}_{\eltx\functionf} \\ \end{array}$.

---

Moving up several levels of generality and abstraction, there are the following bijections
(in the three examples of natural transformations, we show their components at $\setX\in\Set\op$):

Description		Bijections		Example
Internal subsets of $\bftwo\times\bftwo$		$\Sub(\bftwo\times\bftwo)$		$\{\langle \radjtop,\radjtop \rangle\} \subset \bftwo\times\bftwo$
predicate/subset bijection		$\Vert\wr$		$\wr$	$ $
Internal predicates on $\bftwo\times\bftwo$		$\hom {\bftwo\times\bftwo} \Set \bftwo $		$\bftwo\times\bftwo \xrightarrow{\textstyle\wedge} \bftwo $
Yoneda bijection		$\Vert\wr$		$\wr$	$ $
Natural transformations between indicated functors		$\hom {\hom - \Set {\bftwo\times\bftwo}} {[\Set\op,\Set]} {\hom - \Set \bftwo} $		$\hom \setX \Set {\bftwo\times\bftwo} \xrightarrow{\textstyle \hom \setX \Set \wedge} \hom \setX \Set \bftwo $
defn. of internal product in $\Set$		$\Vert\wr$		$\wr$	$ $
External operations on predicates		$\hom {{\hom - \Set \bftwo} \times {\hom - \Set \bftwo}} {[\Set\op,\Set]} {\hom - \Set \bftwo} $		${\hom \setX \Set \bftwo} \times {\hom \setX \Set \bftwo} \xrightarrow{\textstyle \wedge} {\hom \setX \Set \bftwo} $
predicate/subset bijection		$\Vert\wr$		$\wr$	$ $
External operations on subsets		$\hom {\Sub \times \Sub} {[\Set\op,\Set]} \Sub $		${\Sub(\setX)} \times {\Sub(\setX)} \xrightarrow{\textstyle\cap} {\Sub(\setX)} $

The cartesian closed category 2

\[\begin{array}{l} & \objA \Longrightarrow [ \objB \Rightarrow \objC ] \\ \neg\big( \objA \wedge \neg[ \objB \Rightarrow \objC ] \big) && \neg\objA \vee [ \objB \Rightarrow \objC ] \\ \neg\big( \objA \wedge \neg\neg( \objB \wedge \neg\objC ) \big) \\ \neg\big( \objA \wedge ( \objB \wedge \neg\objC ) \big) && \neg\objA \vee \neg( \objB \wedge \neg \objC ) \\ \neg\big( \objA \wedge \objB \wedge \neg\objC \big) && \neg\objA \vee \neg\objB \vee \objC \\ \neg\big( (\objA \wedge \objB) \wedge \neg\objC \big) && \neg(\objA \wedge \objB) \vee \objC \\ & \objA \wedge \objB \Longrightarrow \objC \\ \end{array}\]

---

\[\begin{array}{} &&& \radjtop & \unicode{0x2500} & \radjtop \\ && \unicode{0x2571} && \unicode{0x2571} \\ & \radjtop & \unicode{0x2500} & \radjtop \\ \\ && \radjtop & \unicode{0x2500} & \ladjbot \\ & \unicode{0x2571} && \unicode{0x2571} \\ \radjtop & \unicode{0x2500} & \radjtop \\ \end{array}\]

---

		$\objB$
		$\Big\uparrow$	$\objB$
$\top$			$\Rule{100px}{2px}{0px}$
$\neg\objA$		$\Rule{2px}{50px}{50px}$		$\Rule{2px}{50px}{50px}$	$\objA$
$\bot$			$\Rule{100px}{2px}{0px}$		$\longrightarrow \objA$
		$\bot$	$\neg\objB$	$\top$

---

$\top$		$\top$	$\Rule{100px}{2px}{0px}$	$\top$
		$\Rule{2px}{50px}{50px}$		$\Rule{2px}{50px}{50px}$
$\bot$		$\top$	$\Rule{100px}{2px}{0px}$	$\bot$
		$\bot$		$\top$

---

\[\begin{array}{} \bbox[100px, border:1px black solid]{AA} \end{array}\]

Relations between the categories Set and 2

• The (realization $\dashv$ nerve) adjunction $(\functorf = - \cdot \top) \dashv (\functoru = \hom \top \cattwo -)$ between $\Set$ and $\cattwo$
• Relations between the cartesian monoidal structures: the monoidal functors $\big( \functorF = \langle \functorf, \tilde\functorf, \functorf^\circ \rangle \big)$ and $\big( \functorU = \langle \functoru, \tilde\functoru, \functoru^\circ \rangle \big)$
• Composition of monoidal functors
• Monoidal natural transformations between monoidal functors
• $\langle \functorf\functoru, \eta \rangle$ as an idempotent monad on $\Set$
• The category of algebras $\functorf\functoru\mathord-\Alg$ for $\functorf\functoru$

There is a (realization $\dashv$ nerve) adjunction between $\Set$ and $\cattwo$: $\big( \functorf = - \cdot \top : \setX \mapsto \setX\cdot\top = \bigvee\limits_{\smash\setX} \top \big) \dashv \big( \functoru = \hom \top \cattwo - : \objectA \mapsto \hom \top \cattwo \objectA \big) : \cattwo \to \Set$ : \[\begin{array}{} && && && && && && && {} \rlap{\mkern2.5em \href {https://ncatlab.org/nlab/show/triangle+identities} {\text{triangle identities}}} \\ && && && && && && && {} \rlap{\mkern-.5em \Rule {14em} {2px} {0px}} \\ && && && && \setX && && && \hom \top \cattwo \objectA & = & \hom \top \cattwo \objectA & = & \objectA\functoru \\ && && && \setX & \mathop\mapsto\limits^{\smash{\textstyle \eta}} & \llap{\setX\eta} \downarrow & \searrow\rlap{\forall\functionh} & && && \downarrow \rlap{\objectA\functoru\eta} \\ && && && && \mkern1.2em \hom \top \cattwo {(\setX\cdot\top)} & \mathop\dashrightarrow\limits_{\smash{\textstyle \hom \top \cattwo \functionk }} & \hom \top \cattwo \objectA && && \mkern2em \hom \top \cattwo {((\hom \top \cattwo \objectA) \cdot \top)} && \smash{\Bigg\Vert \rlap{1_{(\hom \top \cattwo \objectA)}}} && \smash{\Bigg\Vert \rlap{1_{\objectA\functoru}}} \\ && && && && && && && \llap\Vert \downarrow \rlap{\objectA\epsilon\functoru} \\ && && && && \setX\cdot\top & \mathop\dashrightarrow\limits_{\smash{\textstyle \exists!\functionk}} & \objectA && && \hom \top \cattwo \objectA & = & \hom \top \cattwo \objectA & = & \objectA\functoru \\ \\ \functionh & \in & \mkern1.5em \hom \setX \Set {(\hom \top \cattwo \objectA)} & \mkern2em \smash{\Rule {2px} {2ex} {11ex}} \mkern1em & && \Set && \xrightarrow{\mkern3em} && \Set && \xrightarrow{\mkern3em} && \Set \\ && \wr\Vert && & \llap\setX \nearrow & \llap\functionk \Big\Downarrow & \llap\functorf \searrow & \Big\Downarrow \rlap\eta & \llap\functoru \nearrow & \llap\Vert \Big\Downarrow \rlap\epsilon & \llap\functorf \searrow & \Big\Downarrow \rlap\eta & \llap\functoru \nearrow \rlap{\hom \top \cattwo -}\\ \functionk & \in & \hom {(\setX\cdot\top)} \cattwo \objectA \mkern1.4em && \catI && \xrightarrow[\textstyle \objectA]{\smash{\mkern3em}} && \cattwo && \xrightarrow[\mkern3em]{\smash{}} && \cattwo \\ \\ && && && && \setX & \mathop\dashrightarrow\limits^{\smash{\textstyle \exists!\functionh}} & \hom \top \cattwo \objectA && && \setX\cdot\top & = & \setX\cdot\top & = & \setX\functorf \\ && && && && && && && \downarrow \rlap{\setX\eta\functorf} \\ && && && && \setX\cdot\top & \mathop\dashrightarrow\limits^{\smash{\textstyle \functionh\cdot\top }} & \big( \hom \top \cattwo \objectA \big) \cdot \top && && \big( \hom \top \cattwo {(\setX\cdot\top)} \big) \cdot \top && \smash{\Bigg\Vert \rlap{1_{(\setX\cdot\top)}}} && \smash{\Bigg\Vert \rlap{1_{\setX\functorf}}} \\ && && && && & \llap{\forall\functionk}\searrow & \llap\Vert \downarrow \rlap{\objectA\epsilon} && && \llap\Vert \downarrow \rlap{\setX\functorf\epsilon} \\ && && && && && \objectA && && \setX\cdot\top & = & \setX\cdot\top & = & \setX\functorf \\ \end{array}\]

---

		$\begin{array}{} | \emptyset \downarrow \functoru | \\ \wr\Vert \\ | \bot \downarrow \cattwo| \\ \end{array}$	$\begin{array}{} | (\setX\neq\emptyset) \downarrow \functoru | \\ \wr\Vert \\ | \top \downarrow \cattwo| \\ \end{array}$
$\objectA\in\cattwo$	$\begin{array}{}\objectA\functoru = \top\functoru = \hom \top \cattwo \top \cong 1\\ \objectA=\top\\ \end{array}$	$\begin{array}{} \mkern2.5em \hom \emptyset \Set {(\hom \top \cattwo \top \cong 1)} \\ \wr\Vert \\ \hom {(\emptyset\cdot\top = \bot)} \cattwo \top \mkern2.2em \\ \end{array}$	$\begin{array}{} \mkern.75em \hom {(\setX\neq\emptyset)} \Set {(\hom \top \cattwo \top \cong 1)} \\ \wr\Vert \\ \hom {((\setX\neq\emptyset)\cdot\top = \top)} \cattwo \top \mkern4em \\ \end{array}$	$\begin{array}{} | \Set \downarrow 1 | \\ \wr\Vert \\ | \functorf \downarrow \top | \\ \end{array}$
	$\begin{array}{}\objectA\functoru = \bot\functoru = \hom \top \cattwo \bot = \emptyset\\ \objectA=\bot\\ \end{array}$	$\begin{array}{} \mkern2.6em \hom \emptyset \Set {(\hom \top \cattwo \bot = \emptyset)} \\ \wr\Vert \\ \hom {(\emptyset\cdot\top = \bot)} \cattwo \bot \mkern2.3em \\ \end{array}$	$\begin{array}{} \mkern1em \hom {(\setX\neq\emptyset)} \Set {(\hom \top \cattwo \bot - \emptyset)} \\ \wr\Vert \\ \hom {((\setX\neq\emptyset)\cdot\top = \top)} \cattwo \bot \mkern4em \\ \end{array}$	$\begin{array}{} | \Set \downarrow \emptyset | \\ \wr\Vert \\ | \functorf \downarrow \bot | \\ \end{array}$
$\begin{array}{} \mkern1.3em \hom \setX \Set {(\hom \top \cattwo \objectA)} \\ \wr\Vert \\ \hom {(\setX\cdot\top)} \cattwo \objectA \mkern1.4em \\ \end{array}$ $\begin{array}{} \Set \downarrow \functoru \\ \wr\Vert \\ \functorf \downarrow \cattwo \\ \end{array}$		$\begin{array}{} \setX=\emptyset\\ \setX\functorf = \emptyset\functorf = \emptyset\cdot\top = \bot\\ \end{array}$	$\begin{array}{} \setX\neq\emptyset\\ (\setX\neq\emptyset)\functorf = (\setX\neq\emptyset)\cdot\top = \top\\ \end{array}$
		$\setX\in\Set$

---

\[\begin{array}{} && \catI & \xrightarrow[\mkern3em]{\textstyle \setX} & \Set & \mkern8em & && \catI && \xrightarrow[\mkern3em]{\textstyle \setX} && \Set \\ & \nearrow & \llap\functionh \Downarrow & \nearrow \rlap{\functoru = \hom \top \cattwo -} & & \equiv & & \nearrow & \llap\functionk \Downarrow & \searrow \rlap{\mkern-2em \setX\cdot\top } & \Downarrow \rlap{\setX\eta} & \nearrow \rlap{\functoru = \hom \top \cattwo -} \\ \setX\downarrow\functoru & \xrightarrow[\textstyle \objectA]{\mkern3em} & \cattwo && && \setX\downarrow\functoru && \xrightarrow[\textstyle \objectA]{\mkern3em} && \cattwo \\ \end{array}\]
\[\begin{array}{} && \catI & \xrightarrow[\mkern3em]{\textstyle \emptyset} & \Set & \mkern8em & && \catI && \xrightarrow[\mkern4em]{\textstyle \emptyset} && \Set \\ & \nearrow & \llap\functionh \Downarrow & \nearrow \rlap{\functoru = \hom \top \cattwo -} & & \equiv & & \nearrow & \llap\functionk \Downarrow & \searrow \rlap{\mkern-2.8em \boxed{\emptyset\cdot\top = \bot} } & \Downarrow \rlap{\emptyset\eta} & \nearrow\rlap{\functoru = \hom \top \cattwo -} \\ \emptyset\downarrow\functoru & \xrightarrow[\textstyle \objectA]{\mkern3em} & \cattwo && && \emptyset\downarrow\functoru && \xrightarrow[\textstyle \objectA]{\mkern4em} && \cattwo \\ \langle \emptyset \xrightarrow[\functionh]{} \hom \top \cattwo \top , \top \rangle & \mathop\mapsto\limits_{\functorA} & \top && && \langle \emptyset \xrightarrow[\functionh]{} \hom \top \cattwo \top , \top\rangle && \mathop\mapsto\limits_{\functorA} && \top \\ \langle \emptyset \xrightarrow[\functionh]{\emptyset\eta} \hom \top \cattwo \bot , \bot \rangle & \mathop\mapsto\limits_{\functorA} & \bot && && \langle \emptyset \xrightarrow[\functionh]{\emptyset\eta} \hom \top \cattwo \bot , \bot \rangle && \mathop\mapsto\limits_{\functorA} && \bot \\ \end{array}\]
\[\begin{array}{} && \catI & \xrightarrow[\mkern3em]{\textstyle \setX \ne \emptyset} & \Set & \mkern8em & && \catI && \xrightarrow[\mkern4em]{\textstyle \setX \ne \emptyset} && \Set \\ & \nearrow & \llap\functionh \Downarrow & \nearrow \rlap{\functoru = \hom \top \cattwo -} & & \equiv & & \nearrow & \llap\functionk \Downarrow & \searrow \rlap{\mkern-2.8em \boxed{\setX\cdot\top = \top} } & \Downarrow \rlap{\setX\eta} & \nearrow\rlap{\functoru = \hom \top \cattwo -} \\ (\setX \ne \emptyset) \downarrow\functoru & \xrightarrow[\textstyle \objectA]{\mkern3em} & \cattwo && && (\setX \ne \emptyset) \downarrow\functoru && \xrightarrow[\textstyle \objectA]{\mkern4em} && \cattwo \\ \langle \setX \xrightarrow[\functionh]{} \hom \top \cattwo \top , \top \rangle & \mathop\mapsto\limits_{\functorA} & \top && && \langle \setX \xrightarrow[\functionh]{} \hom \top \cattwo \top , \top \rangle && \mathop\mapsto\limits_{\functorA} && \top \\ \end{array}\]

---

The following diagrams, special cases of the “mates” bijection of DA, Theorem 1.2,
relate the adjunction $(\functorf = - \cdot \top) \dashv (\functoru = \hom \top \cattwo -)$ with the cartesian monoidal structures,
(cartesian product $\times$) and (the single element set $1$) on $\Set$, and (conjunction $\land$) and (top (or “true”) $\top$) on $\cattwo$.
The first relates the units ($1\in\Set$) and ($\top\in\cattwo$) (compare DA (2.1)).
The second, relating $\times$ and $\land$, is a special case of DA (1.2), with DA (2.2), the evaluation of (the mates diagram) at $\setX,\setY$ to yield $\smash{\langle\setX,\setY\rangle \tilde\functorf '}$, on its right. \[\begin{array}{} && && && & \mkern3em \smash{\Rule {2px} {2ex} {23ex}} \mkern1em & \boxed{\functoru^\circ} & \mkern2em && \boxed{{\functorf^\circ}'} && \boxed{\functorf^\circ} \\ && && && && 1 && \mathop\mapsto\limits^{\smash{\textstyle\functionf}} & 1 \cdot \top & = & 1 \cdot \top \\ \catI && \xrightarrow[\mkern3em]{\smash{\textstyle 1}} && \Set && && \llap{\wr\Vert} \downarrow \rlap{\functoru^\circ = 1_\top} && \mathop\mapsto\limits^{\textstyle\functionf} & \downarrow \rlap{\smash{\functoru^\circ\functionf = 1_\top \cdot \top}} \\ & \llap{\smash{\boxed{{\functorf^\circ}'}} : \mkern8em \top} \searrow & \llap{\wr\Vert} \bigg\Downarrow \rlap{\boxed{\functoru^\circ}} & \nearrow \rlap\functoru & \llap \Vert \bigg\Downarrow \rlap\epsilon & \searrow \rlap{\functorf = - \cdot \top} & && \hom \top \cattwo \top && \mathop\mapsto\limits^{\smash{\textstyle\functionf}} & ( \hom \top \cattwo \top ) \cdot \top && \smash{\llap\Vert \Bigg\uparrow \rlap{\boxed{\functorf^\circ}}} \\ && \cattwo && \xrightarrow[\mkern3em]{} && \cattwo &&& && \llap{\Vert} \downarrow \rlap{\top\epsilon} \\ && && && && &&& \top & = & \top \\ \end{array}\]

---

\[\begin{array}{} && \setX,\setY && \xlongequal{} && \setX,\setY & \mathop\mapsto\limits^{\smash{\textstyle\times}} && \setX\times\setY &&& \mkern2em \smash{\Rule {2px} {1ex} {57ex}} \mkern1em \\ \\ && &&&& \hom \top \cattwo \objectA, \hom \top \cattwo \objectB & \mathop\mapsto\limits^{\smash{\textstyle\times}} && \hom \top \cattwo \objectA \times \hom \top \cattwo \objectB && && \boxed{\langle\setX,\setY\rangle \tilde\functorf '} && \boxed{\langle\setX,\setY\rangle \tilde\functorf} \\ && &&&&&&& \llap{\wr\Vert} \bigg\downarrow \rlap{\boxed{\langle\objectA,\objectB\rangle \tilde\functoru} \mkern1em \text{monoidal $\langle \functoru, \tilde\functoru \rangle$}} \\ && &&&&&&& \hom \top \cattwo {\objectA\land\objectB} &&& & (\setX\times\setY)\cdot\top & = & \langle \setX,\setY \rangle \mathord\times\functorf \\ && &&&&&&&&&&& \big\downarrow \rlap{(\setX\eta\times\setY\eta)\cdot\top} \\ && \Set\times\Set && \xrightarrow{\mkern2em} && \Set\times\Set & \xrightarrow[\mkern5em]{\textstyle \times} && \Set &&&& \big( \hom \top \cattwo {(\setX\cdot\top)} \times \hom \top \cattwo {(\setY\cdot\top)} \big) \cdot \top \\ && & \llap{\smash{\boxed{\tilde\functorf '}}: \mkern6em \functorf\times\functorf} \searrow & \bigg\Downarrow \rlap{\mkern-1.5em \eta\times\eta} & \nearrow\rlap{\functoru\times\functoru} && \llap{\wr\Vert} \bigg\Downarrow \rlap{\boxed{\tilde\functoru}} & \llap{\functoru}\nearrow\rlap{\hom \top \cattwo -} & \llap\Vert \bigg\Downarrow \rlap{\epsilon} & \llap{\functorf}\searrow\rlap{{\mathord-}\cdot\top} &&& \bigg\downarrow \rlap{\langle\setX\cdot\top,\setY\cdot\top\rangle \tilde\functoru \cdot \top} && \smash{\llap\Vert \Bigg\uparrow \rlap{\boxed{\langle \setX,\setY \rangle \tilde\functorf}}} \\ && && \cattwo\times\cattwo && \xrightarrow[\textstyle \land]{} & \cattwo && \xrightarrow[\mkern2em]{} && \cattwo && \big( \hom \top \cattwo {(\setX\cdot\top) \land (\setY\cdot\top)} \big) \cdot \top \\ && &&&&&&&&&&& \llap\Vert \big\downarrow \rlap{\big((\setX\cdot\top) \land (\setY\cdot\top)\big)\epsilon} \\ && && \objectA,\objectB && \mathop\mapsto\limits_{\smash{\textstyle\land}} & \objectA\land\objectB &&&&&& (\setX\cdot\top) \land (\setY\cdot\top) & = & \langle \setX,\setY \rangle (\functorf\times\functorf) \mathord\land \\ && &&&&&&&&& (\setX\times\setY)\cdot\top \\ && &&&&&&&&& \llap\Vert \bigg\downarrow \rlap{\boxed{\langle\setX,\setY\rangle \tilde\functorf '} \mkern.5em \text{op-monoidal $\langle \functorf, {\tilde\functorf}' \rangle$}} \\ && && {}\rlap{\mkern-3em \setX\cdot\top,\setY\cdot\top} && \mathop\mapsto\limits_{\smash{\textstyle\land}} & {}\rlap{\mkern-3.5em (\setX\cdot\top) \land (\setY\cdot\top)} && \xlongequal{} && {}\rlap{\mkern-3.7em (\setX\cdot\top)\land(\setY\cdot\top)} \\ \end{array}\]

Note that $\tilde\functorf$ goes in the opposite direction to ${\tilde\functorf}'$, and likewise for $\functorf^\circ$ and ${\functorf^\circ}'$.
In this case they are in fact inverse.
Note that while ($\eta$ and $\epsilon$) mediate (a mates bijection between $\tilde\functoru$ and ${\tilde\functorf}'$),
they cannot mediate (a bijection between $\tilde\functorf$ and a hypothetical ${\tilde\functoru}'$),
because $\tilde\functorf$, unlike ($\tilde\functoru$ and ${\tilde\functorf}'$), “goes in the opposite direction” to ($\eta$ and $\epsilon$).

We have:
$\functorF = \langle \functorf,\tilde\functorf,\functorf^\circ \rangle$ is strict monoidal (because $\tilde\functorf$ and $\functorf^\circ$ are equalities).
$\functorU = \langle \functoru,\tilde\functoru,\functoru^\circ \rangle$ is strong monoidal (because $\tilde\functoru$ and $\functoru^\circ$ are isomorphisms, here bijections of sets).
(The term monoidal functor without qualification) usually, e.g. CC II.1, means (lax monoidal).

---

Composition of monoidal functors: $\widetilde{(\functorf\functoru)}$ and $(\functorf\functoru)^\circ$

Monoidal functors compose to give another monoidal functor,
as in the composite $\big( \functorF = \langle \functorf,\tilde\functorf,\functorf^\circ \rangle \big) \circ \big( \functorU = \langle \functoru,\tilde\functoru,\functoru^\circ \rangle \big) = \big( \functorF\functorU = \langle \functorf\functoru,\widetilde{(\functorf\functoru)}, (\functorf\functoru)^\circ \rangle \big)$ : \[\begin{array}{} && \Set\times\Set & \xrightarrow[\mkern3em]{\textstyle \times} & \Set && && \setX\functorf\functoru \times \setY\functorf\functoru & = & \setX\functorf\functoru \times \setY\functorf\functoru && 1 & = & 1 \\ && \llap{\functoru\times\functoru} \bigg\uparrow & \llap{\tilde\functoru} \bigg\Downarrow & \llap{\functoru} \bigg\uparrow & \llap{\smash{\lower2ex\hbox{$\functoru^\circ \mkern-.4em \Downarrow$}}} \nwarrow \rlap{1} & && \bigg\downarrow \rlap{\langle \setX\functorf,\setY\functorf \rangle \tilde\functoru} && && \bigg\downarrow\rlap{\functoru^\circ} \\ && \cattwo\times\cattwo & \xrightarrow{\smash{\textstyle \land}} & \cattwo & \xleftarrow[\mkern3em]{\smash{\textstyle \top}} & \catI & \mkern4em & (\setX\functorf \land \setY\functorf) \rlap\functoru && \smash{\Bigg\downarrow \rlap{\boxed{\langle \setX,\setY \rangle \widetilde{(\functorf\functoru)}}}} & \mkern6em & \top\functoru && \smash{\Bigg\downarrow\rlap{\boxed{(\functorf\functoru)^\circ}}} \\ && \llap{\functorf\times\functorf} \bigg\uparrow & \llap{\tilde\functorf} \bigg\Downarrow & \llap{\functorf} \bigg\uparrow & \llap{\smash{\raise2ex\hbox{$\functorf^\circ \mkern-.4em \Downarrow$}}} \swarrow \rlap{1} & && \bigg\downarrow \rlap{\langle \setX, \setY \rangle \tilde\functorf \functoru} && && \bigg\downarrow\rlap{\functorf^\circ\functoru} \\ \langle \setX,\setY \rangle & \in & \Set\times\Set & \xrightarrow[\textstyle \times]{\mkern3em} & \Set && && (\setX \times \setY) \rlap{\functorf\functoru} & = & (\setX \times \setY) \rlap{\functorf\functoru} && 1\functorf\functoru & =& 1\functorf\functoru \\ \end{array}\]

---

Monoidal natural transformation $\eta$ : $\tilde\eta$ and $\eta^\circ$

Note that whereas $\tilde\functoru$ and $\functoru^\circ$ were structures, i.e., arrows, $\tilde\eta$ and $\eta^\circ$ are properties, i.e., equalities of arrows. \[\begin{array}{} && \widetilde{\text{MN}} = \tilde\eta && &&& \text{MN}^\circ = \eta^\circ \\ \\ \setX \times \setY & {}\rlap{\mkern-3em\xlongequal[\mkern28em]{\textstyle \langle \setX,\setY \rangle \widetilde{(1_\Set)}}} &&& \setX \times \setY && 1 & \xlongequal[\mkern3em]{\textstyle (1_\Set)^\circ} & 1 \\ \Bigg\downarrow \rlap{\mkern-2.32em\setX\eta\times\setY\eta} && \smash{\boxed{\widetilde{\text{MN}} = \langle \setX,\setY \rangle \tilde\eta}} && \Bigg\downarrow \rlap{\mkern-2.2em(\setX\times\setY)\eta} & \mkern8em & \llap{\functoru^\circ} \Bigg\downarrow & \searrow \rlap{\mkern-3em \lower2ex\hbox{$(\functorf\functoru)^\circ$} \mkern1em \smash{\raise2ex\hbox{$\boxed{\eta^\circ}$}}} & \Bigg\downarrow \rlap{1\eta} \\ \setX\functorf\functoru \times \setY\functorf\functoru & {}\rlap{\mkern-3em\xrightarrow[\smash{\textstyle \langle \setX,\setY \rangle \widetilde{(\functorf\functoru)}}]{\mkern28em}} &&& (\setX\times\setY) \rlap{\functorf\functoru} && \top\functoru & \xrightarrow[\smash{\textstyle \functorf^\circ\functoru}]{} & 1\functorf\functoru \\ \Vert &&&& \Vert && \Vert && \Vert \\ \setX\functorf\functoru \times \setY\functorf\functoru & \xrightarrow[\smash{\textstyle \langle \setX\functorf,\setY\functorf \rangle \tilde\functoru}]{} & \big((\setX\functorf)\land(\setY\functorf)\big)\functoru & \xrightarrow[\smash{\textstyle \langle \setX,\setY \rangle \tilde\functorf \functoru}]{} & (\setX\times\setY) \rlap{\functorf\functoru} && \hom \top \cattwo \top & \xrightarrow[\smash{\textstyle \hom \top \cattwo {\functorf^\circ}}]{} & \hom \top \cattwo {1\cdot\top} \\ \Vert && \Vert && \Vert \\ \hom \top \cattwo {\setX\cdot\top} \times \hom \top \cattwo {\setY\cdot\top} & \xrightarrow[\textstyle \langle \setX\cdot\top,\setY\cdot\top \rangle \tilde\functoru]{} & \hom \top \cattwo {(\setX\cdot\top)\land(\setY\cdot\top)} & \xrightarrow[\textstyle \hom \top \cattwo {\langle \setX,\setY \rangle \tilde\functorf}]{} & \hom \top \cattwo {(\setX\times\setY)\cdot\top} \\ \end{array}\]

---

To prove Proposition 1.3 of DA in this situation, that in this situation
[($\eta$ and $\epsilon$ are monoidal natural transformations) iff (${\tilde\functorf}'$ is, respectively, a pre- and post- inverse for $\tilde\functorf$)],
we need only consult the display below, and recall that
$\langle \functoru\doctrineD, \eta\doctrineD \rangle$ is an absolute left extension and $\langle \functoru, \epsilon \rangle$ is an absolute right lift.

$\begin{array}{lcl} {\tilde\functorf}' \cdot \tilde\functorf & \xlongequal{\textstyle \text{defn. of ${\tilde\functorf}'$}} & \eta\doctrineD \cdot \tilde\functoru \cdot \epsilon \cdot \tilde\functorf \\ & \xlongequal{\textstyle \epsilon \text{ natural}} & \eta\doctrineD \cdot \tilde\functoru \cdot \tilde\functorf \cdot \epsilon \\ & \xlongequal{\textstyle\tilde\eta \cdot \epsilon} & \eta \cdot \epsilon \\ & \xlongequal{\textstyle \triangle \dashv} & 1_{(\mathord\times \cdot \functorf)} \\ \end{array}$

$\begin{array}{} \Set\doctrineD &{}\rlap{\xrightarrow{\mkern6em}} &&& \Set\doctrineD \\ & \llap{\functorf\doctrineD} \searrow & \Downarrow\rlap{\eta\doctrineD} & \nearrow \rlap{\functoru\doctrineD} & \Downarrow \rlap{\epsilon\doctrineD} & \searrow \rlap{\functorf\doctrineD} \\ && \cattwo\doctrineD &{}\rlap{\xrightarrow{\mkern8em}} &&& \cattwo\doctrineD \\ \smash{\llap\times \Bigg\downarrow} & && & \smash{\Bigg\downarrow \rlap\times} & \\ & \smash{\llap{\tilde\functorf}} \Bigg\Downarrow && \smash{\Bigg\Downarrow \rlap{\tilde\functoru}} && \smash{\Bigg\Downarrow \rlap{\tilde\functorf}} \\ && \smash{\llap\land \Bigg\Downarrow} &&&& \smash{\Bigg\downarrow \rlap\land} \\ \Set &{}\rlap{\xrightarrow{\mkern6em}} &&& \Set \\ & \llap{\functorf} \searrow & \Downarrow\rlap\eta & \nearrow \rlap{\functoru} & \Downarrow\rlap\epsilon & \searrow \rlap\functorf \\ && \cattwo &{}\rlap{\xrightarrow{\mkern8em}} &&& \cattwo \\ \end{array}$

$\begin{array}{rcl} \tilde\functorf \cdot {\tilde\functorf}' & \xlongequal{\textstyle \text{defn. of ${\tilde\functorf}'$}} & \tilde\functorf \cdot \eta\doctrineD \cdot \tilde\functoru \cdot \epsilon \\ & \xlongequal{\textstyle \tilde\functorf \text{ natural}} & \eta\doctrineD \cdot \tilde\functorf \cdot \tilde\functoru \cdot \epsilon \\ & \xlongequal{\textstyle \eta\doctrineD \cdot \tilde\epsilon} & \eta\doctrineD \cdot \epsilon\doctrineD \\ & \xlongequal{\textstyle \triangle \dashv} & 1_{(\functorf\doctrineD \cdot \mathord\land)} \\ \end{array}$

---

The above enriches (the adjunction in $\CAT$), $$\big( \functorf = - \cdot \top : \setX \mapsto \setX\cdot\top = \bigvee\limits_{\smash\setX} \top \big) \dashv \big( \functoru = \hom \top \cattwo - : \objectA \mapsto \hom \top \cattwo \objectA \big) : \cattwo \to \Set \; ,$$ into (a monoidal adjunction in $\CAT$), i.e., (an ordinary adjunction in the 2-category $\MONCAT$ (CC II.1.3)), $$\boxed{\big( \functorF = \langle \functorf,\tilde\functorf,\functorf^\circ \rangle \big) \dashv \big( \functorU = \langle \functoru,\tilde\functoru,\functoru^\circ \rangle \big) : \langle \cattwo,\land,\top \rangle \to \langle \Set,\times,1 \rangle}$$ \[\begin{array}{} \functionh & \in & \mkern1.5em \hom \setX \Set {(\hom \top \cattwo \objectA)} & \mkern2em \smash{\Rule {2px} {2ex} {11ex}} \mkern1em & && \langle \Set,\times,1 \rangle && \xrightarrow{\mkern3em} && \langle \Set,\times,1 \rangle && \xrightarrow{\mkern3em} && \langle \Set,\times,1 \rangle \\ && \wr\Vert && & \llap\setX \nearrow & \llap\functionk \Big\Downarrow & \searrow \rlap{\mkern-3em \langle \functorf,\tilde\functorf,\functorf^\circ \rangle} & \Big\Downarrow \rlap\eta & \nearrow \rlap{\mkern-2.5em \langle \functoru,\tilde\functoru,\functoru^\circ \rangle} & \llap\Vert \Big\Downarrow \rlap\epsilon & \searrow \rlap{\mkern-3em \langle \functorf,\tilde\functorf,\functorf^\circ \rangle} & \Big\Downarrow \rlap\eta & \nearrow \rlap{\functorU = \langle \functoru,\tilde\functoru,\functoru^\circ \rangle} \\ \functionk & \in & \hom {(\setX\cdot\top)} \cattwo \objectA \mkern1.4em && \catI && \xrightarrow[\textstyle \objectA]{\smash{\mkern3em}} && \langle \cattwo,\land,\top \rangle && \xrightarrow[\mkern3em]{\smash{}} && \langle \cattwo,\land,\top \rangle \\ \end{array}\]

---

References

CC, Eilenberg and Kelly, “Closed Categories”, 1966
DA, Kelly, Max, “Doctrinal adjunction”, 1974

---

Draft stuff:

---

Test: $\tilde f ', {\tilde f}', \tilde{f'}, {f^\circ}', {f'}^\circ $

Change of base for enriched categories

The following is a very incomplete preliminary draft

$\begin{array}{lccccccc} \text{The 2-cell} && && \twocellctblr \eta \Phi {\Phi'} \calV {\mkern.5em \calV'} & \mkern6em & \subset & \MONCAT\\ && && \smash{\lower1.6ex\hbox{_}} \\ \text{is mapped by the 2-functor (see CC II.6.3)} \mkern4em && && \Bigg\downarrow \rlap{()_\ast} &&& \smash{\Bigg\downarrow\rlap{()_\ast}} \\ \\ \text{to the 2-cell on the right in} && \catI & \twocellctb \functorT \catA {\catA'} & \twocellctblr {\eta_\ast} {\Phi_\ast} {\Phi_\ast'} {\calV\mathord-\Cat} {\mkern.5em \calV'\mathord-\Cat} && \subset & \CAT \\ \end{array}$

Evaluating the above, we get (the diamond-shaped diagram in $\calV'\mathord-\Cat$ at left below);
evaluating (that diamond-diagram in $\calV'\mathord-\Cat$) at (objects $\objecta,\objecta'$ in $\catA$) (and thus also in $\catA\Phi_\ast$),
we get (the diagram of hom-objects and arrows in $\calV'$ shown at its right): \[\begin{array}{} & {}\rlap{\mkern-2em\calV\mathord-\Cat} & && \calV'\mathord-\Cat && && && && && \calV' \\ \\ && && \catI && && && && && \hom \objecta {(\catA\Phi_\ast)} {\objecta'} \\ && && \llap\objecta \downdownarrows \rlap{\objecta'} && && && && && \Vert \rlap{\text{CC I(6.2)}} \\ && \mkern-3em \catA && \catA\Phi_\ast && \Phi_\ast && && && \llap{\hom \objecta {(\functorT\Phi_\ast)} {\objecta'}} \swarrow && (\hom \objecta \catA {\objecta'}) \phi && \searrow \rlap{ \hom \objecta {(\catA\eta_\ast)} {\objecta'} }\\ & \mkern-1em \llap\functorT \swarrow & & \llap{\functorT\Phi_\ast} \swarrow && \searrow \rlap{\catA\eta_\ast} && \mkern-1.5em \searrow\mkern-.85em\searrow \rlap{\eta_\ast} && && && \llap{(\hom {\objecta} \functorT {\objecta'})\phi} \swarrow && \searrow \rlap{(\hom \objecta \catA {\objecta'})\eta} \\ \catA' && \catA'\Phi_\ast && \functorT\eta_\ast && \catA\Phi_\ast' && \mkern-1.3em \Phi_\ast' & \mkern2em \smash{\mathop\mapsto\limits^{\textstyle \hom \objecta {()} {\objecta'}}} \mkern2em & \hom {\objecta\functorT} {(\catA'\Phi_\ast)} {\objecta'\functorT} & = & (\hom {\objecta\functorT} {\catA'} {\objecta'\functorT}) \phi && (\hom \objecta \functorT {\objecta'}) \eta && (\hom {\objecta} {\catA} {\objecta'}) \phi' & = & \hom {\objecta} {(\catA\Phi_\ast')} {\objecta'} \\ && & \llap{\catA'\eta_\ast} \searrow && \swarrow \rlap{\functorT\Phi_\ast'} && && && && \llap{(\hom {\objecta\functorT} {\catA'} {\objecta'\functorT}) \eta} \searrow && \swarrow \rlap{(\hom {\objecta} {\functorT} {\objecta'}) \phi'} \\ && && \catA'\Phi_\ast' && && && && \llap{\hom \objecta {(\catA'\eta_\ast)} {\objecta'}} \searrow && (\hom {\objecta\functorT} {\catA'} {\objecta'\functorT}) \phi' && \swarrow \rlap{\hom \objecta {(\functorT\Phi_\ast')} {\objecta'}} \\ && && && && && && && \Vert \rlap{\text{CC I(6.2)}} \\ && && && && && && && \hom {\objecta\functorT} {(\catA'\Phi_\ast')} {\objecta'\functorT} \\ \end{array}\]

---

References

CC, Eilenberg and Kelly, “Closed Categories”, 1966

Relations between the 2-categories Set-Cat and 2-Cat

There is a strict 2-functor $\boxed{\big( ()\mathord-\Cat = ()_\ast \big) : \MONCAT \to \CAT : \calV \mapsto (\calV\mathord-\Cat = \calV_\ast)}$
between (the indicated strict 2-categories); see CC II.6.3, also RE2C ¶1.3.2;
the notation $\calV\mathord-\Cat$ is now more standard, see e.g. BCECT,
but CC uses the briefer notations $\calV_\ast$, $\Phi_\ast$ and $\eta_\ast$ for the effect on monoidal categories, monoidal functors and monoidal natural transformations.
(Also, CC calls 2-categories “hypercategories”, a term no longer used for 2-categories.)
(The $()_\ast$ notation) is consistent with (other usages of $()_\ast$):
if we severely overload (the symbol $\setX$) so that it stands for (a) a $\calV$-category and (b) that $\calV$-category's set (or class) of objects, with (c) $\hom - \setX -$ denoting $\setX$'s hom-function,
then (the hom-function of $\setX\Phi_\ast$) is defined as: \[ \hom - {(\setX\Phi_\ast)} - : \setX\times\setX \xrightarrow[\mkern2em]{\textstyle \hom - \setX -} \calV \xrightarrow[\mkern2em]{\textstyle \phi} \calV' : \langle \objectx,\objecty \rangle \mapsto \hom \objectx \setX \objecty \phi = \hom \objectx {(\setX\Phi_\ast)} \objecty \;. \] For its brevity we adopt this notation for the effects of $\big( ()\mathord-\Cat = ()_\ast \big)$ on monoidal functors and monoidal natural transformations: thus $\functorF_\ast$ and $\eta_\ast$,
while using the notation $\calV\mathord-\Cat$ for the effect on monoidal categories.

Recall (the monoidal adjunction in $\CAT$), i.e., (the ordinary adjunction in the 2-category $\MONCAT$): $$\big( \functorF = \langle \functorf,\tilde\functorf,\functorf^\circ \rangle \big) \dashv \big( \functorU = \langle \functoru,\tilde\functoru,\functoru^\circ \rangle \big) : \langle \cattwo,\land,\top \rangle \to \langle \Set,\times,1 \rangle$$ \[\begin{array}{} \functionh & \in & \mkern1.5em \hom \setX \Set {(\hom \top \cattwo \objectA)} & \mkern2em \smash{\Rule {2px} {2ex} {11ex}} \mkern1em & && \langle \Set,\times,1 \rangle && \xrightarrow{\mkern3em} && \langle \Set,\times,1 \rangle && \xrightarrow{\mkern3em} && \langle \Set,\times,1 \rangle \\ && \wr\Vert && & \llap\setX \nearrow & \llap\functionk \Big\Downarrow & \searrow \rlap{\mkern-3em \langle \functorf,\tilde\functorf,\functorf^\circ \rangle} & \Big\Downarrow \rlap\eta & \nearrow \rlap{\mkern-2.5em \langle \functoru,\tilde\functoru,\functoru^\circ \rangle} & \llap\Vert \Big\Downarrow \rlap\epsilon & \searrow \rlap{\mkern-3em \langle \functorf,\tilde\functorf,\functorf^\circ \rangle} & \Big\Downarrow \rlap\eta & \nearrow \rlap{\langle \functoru,\tilde\functoru,\functoru^\circ \rangle = \functorU} \\ \functionk & \in & \hom {(\setX\cdot\top)} \cattwo \objectA \mkern1.4em && \catI && \xrightarrow[\textstyle \objectA]{\smash{\mkern3em}} && \langle \cattwo,\land,\top \rangle && \xrightarrow[\mkern3em]{\smash{}} && \langle \cattwo,\land,\top \rangle \\ \end{array}\] 2-functors take adjunctions to adjunctions (¶2.3.1 of RE2C), thus
[the image under the 2-functor $\big( ()\mathord-\Cat = ()_\ast \big)$]
of (the above adjunction in the 2-category $\MONCAT$)
is (an adjunction in the 2-category $\CAT$): \[\boxed{\begin{array}{} \functionh & \in & \mkern1em \hom \setX {\Set\mathord-\Cat} {\objectA \functorU_\ast} & \mkern2em \smash{\Rule {2px} {2ex} {11ex}} \mkern1em & && \langle \Set,\times,1 \rangle\mathord-\Cat && \xrightarrow{\mkern3em} && \langle \Set,\times,1 \rangle\mathord-\Cat && \xrightarrow{\mkern3em} && \langle \Set,\times,1 \rangle\mathord-\Cat \\ && \wr\Vert && & \llap\setX \nearrow & \llap\functionk \Big\Downarrow & \searrow \rlap{\functorF_\ast} & \Big\Downarrow \rlap{\eta_\ast} & \nearrow \rlap{\functorU_\ast} & \llap\Vert \Big\Downarrow \rlap{\epsilon_\ast} & \searrow \rlap{\functorF_\ast} & \Big\Downarrow \rlap{\eta_\ast} & \nearrow \rlap{\functorU_\ast = \langle \functoru,\tilde\functoru,\functoru^\circ \rangle _\ast} \\ \functionk & \in & \mkern.6em \hom {\setX \functorF_\ast} {\cattwo\mathord-\Cat} \objectA && \catI && \xrightarrow[\textstyle \objectA]{\smash{\mkern3em}} && \langle \cattwo,\land,\top \rangle\mathord-\Cat && \xrightarrow[\mkern3em]{\smash{}} && \langle \cattwo,\land,\top \rangle\mathord-\Cat \\ \end{array}}\] (The monoidal structures $\functoru^\circ$, $\tilde\functoru$, $\functorf^\circ$, and $\tilde\functorf$) combine with (the functors $\functoru$ and $\functorf$ themselves)
to produce ($\functorU_\ast$ and $\functorF_\ast$):
the units (CC I(6.3)) and compositions (CC II(6.1)) of ($\objectA\functorU_\ast$ and $\objectX\functorF_\ast$) are defined by: \[\mkern-3em \begin{array}{} && && && && & \hom \objecta {(\objectA\functorU_\ast)} \objectb \times \hom \objectb {(\objectA\functorU_\ast)} \objectc &&&& &&&& &&&& & \hom \objectx {(\objectX\functorF_\ast)} \objecty \land \hom \objecty {(\objectX\functorF_\ast)} \objectz \\ && && && && & \Vert &&&& &&&& &&&& & \Vert \\ && 1 & = & 1 && && & (\hom \objecta \objectA \objectb)\functoru \times (\hom \objectb \objectA \objectc)\functoru &&&&&& \top & = & \top &&&&& (\hom \objectx \objectX \objecty)\functorf \land (\hom \objecty \objectX \objectz)\functorf \\ && \llap{\wr\Vert} \big\downarrow & \functoru^\circ & \llap{\wr\Vert} \big\downarrow & && && \llap{\wr\Vert} \big\downarrow \rlap{\langle \hom \objecta \objectA \objectb, \hom \objectb \objectA \objectc \rangle \tilde\functoru} &&&& && \llap{\Vert} \big\downarrow & \functorf^\circ & \llap{\Vert} \big\downarrow &&&&& \llap{\Vert} \big\downarrow \rlap{\langle \hom \objectx \objectX \objecty, \hom \objecty \objectX \objectz \rangle \tilde\functorf} \\ \top & \mathop\mapsto\limits^\functoru& \top\functoru & = & \hom \top \cattwo \top &&& \hom \objecta \objectA \objectb \land \hom \objectb \objectA \objectc & \mathop\mapsto\limits^\functoru & \big( \hom \objecta \objectA \objectb \land \hom \objectb \objectA \objectc \big)\functoru &&&& 1 & \mathop\mapsto\limits^\functorf & 1\functorf & = & 1\cdot\top &&& \hom \objectx \objectX \objecty \times \hom \objecty \objectX \objectz & \mathop\mapsto\limits^\functorf & \big( \hom \objectx \objectX \objecty \times \hom \objecty \objectX \objectz \big)\functorf \\ \llap{\text{refl}} \big\downarrow & \mathop\mapsto\limits^\functoru & \llap{\text{refl}\functoru} \big\downarrow & = & \big\downarrow \rlap{\hom \top \cattwo {\text{refl}}} &&& \llap{\text{trans}} \big\downarrow & \mathop\mapsto\limits^\functoru & \llap{\text{trans}\functoru} \big\downarrow &&&& \llap{\objectx\arrowj} \big\downarrow & \mathop\mapsto\limits^\functorf & \llap{\objectx\arrowj\functorf} \big\downarrow & = & \big\downarrow \rlap{(\objectx\arrowj)\cdot\top} &&& \llap{\Mforcomp} \big\downarrow & \mathop\mapsto\limits^\functorf & \big\downarrow \rlap {\Mforcomp\functorf} \\ \hom \objecta \objectA \objecta & \mathop\mapsto\limits^\functoru & \hom \objecta \objectA \objecta \functoru & = & \hom \top \cattwo {\hom \objecta \objectA \objecta} &&& \hom \objecta \objectA \objectc & \mathop\mapsto\limits^\functoru & \hom \objecta \objectA \objectc \functoru &&&& \hom \objectx \objectX \objectx & \mathop\mapsto\limits^\functorf & \hom \objectx \objectX \objectx \functorf & = & \hom \objectx \objectX \objectx \cdot\top &&& \hom \objectx \objectX \objectz & \mathop\mapsto\limits^\functorf & \hom \objectx \objectX \objectz \functorf \\ && \Vert && && && & \Vert &&&& && \Vert && &&&& & \Vert \\ && {} \rlap{\mkern-2em \hom \objecta {(\objectA\functorU_\ast)} \objecta} && && && & {} \rlap{\mkern-2em \hom \objecta {(\objectA\functorU_\ast)} \objectc} &&&& && \hom \objectx {(\objectX\functorF_\ast)} \objectx && &&&& & \hom \objectx {(\objectX\functorF_\ast)} \objectz \\ \end{array}\]

Here of course ($\text{refl}$ and $\text{trans}$) are the implementations in ($\cattwo$-category theory)
of (the reflexive and transitive axioms for preorders);
in (the notation of CC) they would be denoted $\objecta\arrowj$ and $(\Mforcomp = \Mforcomp^\objectb_{\objecta\objectc})$ respectively.

---

References

CC, Eilenberg and Kelly, “Closed Categories”, 1966
RE2C, Kelly and Street, “Review of the Elements of 2-Categories”, 1974
BCECT, Kelly, Basic Concepts of Enriched Category Theory, 1982/2005

Fibred categories of subsets and slices over Set

Each (function $\functionf:\setX\to\setY$) in $\Set$ (the large 1-category of small sets)
generates (the following diagram of categories and functors) in $\CAT$ (the very large 2-category of large categories).
Note: below (the diagram in $\CAT$) we show (the function $\functionf:\setX\to\setY$ in $\Set$) that generates it. $$\begin{array}{cccl} \Set\downarrow\setX & \begin{array}{} \xrightarrow{\textstyle \;\;\sum_\functionf = \functionf_!\;\;}\\ \xleftarrow{\textstyle \functionf^\star}\\ \xrightarrow{\textstyle \prod_\functionf = \functionf_\star}\\ \end{array} & \Set\downarrow\setY \mkern2em & \text{functors between categories of oversets} \\ \llap{\sigma_\setX}\Bigg\downarrow \dashv \Bigg\uparrow \rlap{i_\setX} && \llap{\sigma_\setY} \Bigg\downarrow \dashv \Bigg\uparrow \rlap{i_\setY} & \text{reflections of oversets (supersets) into subsets} \\ \Sub(\setX) & \begin{array}{} \xrightarrow{\textstyle \;\;\exists_\functionf = \functionf_!\;\;}\\ \xleftarrow{\textstyle \functionf^\inv}\\ \xrightarrow{\textstyle \forall_\functionf = \functionf_\star}\\ \end{array} & \Sub(\setY) & \text{order-preserving maps between posets of subsets} \\ \\ \\ \setX & \xrightarrow[\textstyle \functionf]{} & \setY & \text{an arrow (function) in $\Set$} \\ \end{array}$$ Each horizontal triple of arrows, upper and lower, is an adjoint triple, i.e. an adjoint string of length 3.

Draft

Version of 2018-12-05 or later

Draft Outline

The basic building block for Boolean geometry and logic
is the Boolean “object of truth values”: $\bftwo = \{\ladjbot,\radjtop\} = \{\text{false},\text{true}\}$.
We give this set the (linear) order $\ladjbot\lt\radjtop$, in accordance with the ex falso sequitur quodlibet principle of logic.

Boolean geometry then considers powers of $\bftwo$:

the Boolean point	$\bftwo^0 \cong 1$ ,
the Boolean line	$\bftwo^1 \cong \bftwo$ ,
the Boolean plane	$\bftwo^2 \cong \bftwo\times\bftwo$ ,
the Boolean cube	$\bftwo^3\cong \bftwo\times\bftwo\times\bftwo$ , and so on.

The next step is to consider Boolean (i.e., $\bftwo$-valued) functions (which we will call predicates) defined on these geometric objects.
Since (the Boolean object of truth values, $\bftwo$) is (the subobject classifier) for (the category of sets),
such predicates are in bijection with
the subsets of (the source (domain) of the predicate).

---

A comparison of the traditional way of presenting truth tables to
the geometrical way (the graph of the function from $\bftwo\times\bftwo$ to $\bftwo$ determined by the truth table):

Truth table for $\objA\wedge\objB$

$\objA$ $\objB$ $\objA\wedge\objB$ $\radjtop$ $\radjtop$ $\radjtop$ $\ladjbot$ $\radjtop$ $\ladjbot$ $\radjtop$ $\ladjbot$ $\ladjbot$ $\ladjbot$ $\ladjbot$ $\ladjbot$

The graph of the function $\wedge : \bftwo\times\bftwo \rightarrow \bftwo$

$\objB$ $\radjtop$ $\ladjbot$ $\Rule{64px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\objA\wedge\objB$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{64px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$

---

			$\objB\in\{\ladjbot,\radjtop\}$
			$\vary\in\{0,1\}$
			$\Big\uparrow$	$\objB$
$1$	$\top$		$\begin{array}{c}\langle \ladjbot, \radjtop \rangle\\\objB - \objA\\\end{array}$	$\Rule{64px}{2px}{0px}$	$\begin{array}{c}\langle \radjtop, \radjtop \rangle\\\objA\cap\objB\\\end{array}$
	$\neg\objA$		$\Rule{2px}{32px}{32px}$		$\Rule{2px}{32px}{32px}$	$\objA$
$0$	$\bot$		$\begin{array}{c}\langle \ladjbot, \ladjbot \rangle\\\end{array}$	$\Rule{64px}{2px}{0px}$	$\begin{array}{c}\langle \radjtop, \ladjbot \rangle\\\objA - \objB\\\end{array}$		$\longrightarrow \objA\in\{\ladjbot,\radjtop\}, \varx\in\{0,1\}$
			$\bot$	$\neg\objB$	$\top$
			$0$		$1$

---

${2\times2 \choose 4} = 1$	all			$\objB$ $\radjtop$ $\radjtop$ $\Rule{64px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\radjtop\\1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{64px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$
${2\times2 \choose 3} = 4$	ells angles		$\objB$ $\radjtop$ $\radjtop$ $\Rule{128px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA\vee\objB\\(\varx+1)(\vary+1)+1\\\varx\vary+\varx+\vary\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{128px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\radjtop$ $\Rule{96px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\neg\objA\vee\objB\\\objA\Rightarrow\objB\\\neg(\objA\wedge\neg\objB)\\\varx(\vary+1)+1\\\varx\vary+\varx+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{96px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\ladjbot$ $\Rule{96px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA\vee\neg\objB\\\objA\Leftarrow\objB\\\neg(\neg\objA\wedge\objB)\\(\varx+1)\vary+1\\\varx\vary+\vary+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{96px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\radjtop$ $\Rule{128px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\neg\objA\vee\neg\objB\\\neg(\objA\wedge\objB)\\\varx\vary+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{128px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$
${2\times2 \choose 2} = 6$	lines	$\objB$ $\radjtop$ $\ladjbot$ $\Rule{64px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA\\\varx\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{64px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\radjtop$ $\Rule{128px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objB\\\vary\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{128px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\ladjbot$ $\Rule{96px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA\Leftrightarrow\objB\\\varx+\vary+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{96px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\radjtop$ $\Rule{96px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA \veebar\objB\\\varx+\vary\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{96px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\ladjbot$ $\Rule{128px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\neg\objB\\\vary+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{128px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\radjtop$ $\Rule{64px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\neg\objA\\\varx+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{64px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$
${2\times2 \choose 1} = 4$	points vertices		$\objB$ $\radjtop$ $\ladjbot$ $\Rule{128px}{2px}{0px}$ $\radjtop$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA\wedge\objB\\\varx\vary\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{128px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\radjtop$ $\Rule{96px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\neg\objA\wedge\objB\\(\varx+1)\vary\\\varx\vary+\vary\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{96px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\ladjbot$ $\Rule{96px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\objA\wedge\neg\objB\\\varx(\vary+1)\\\varx\vary+\varx\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{96px}{2px}{0px}$ $\radjtop$ $\ladjbot$ $\neg\objB$ $\radjtop$	$\objB$ $\radjtop$ $\ladjbot$ $\Rule{128px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\neg\objA\wedge\neg\objB\\(\varx+1)(\vary+1)\\\varx\vary+\varx+\vary+1\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\radjtop$ $\Rule{128px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$
${2\times2 \choose 0} = 1$	none			$\objB$ $\radjtop$ $\ladjbot$ $\Rule{64px}{2px}{0px}$ $\ladjbot$ $\neg\objA$ $\Rule{2px}{32px}{32px}$ $\begin{array}{c}\ladjbot\\0\end{array}$ $\Rule{2px}{32px}{32px}$ $\objA$ $\ladjbot$ $\ladjbot$ $\Rule{64px}{2px}{0px}$ $\ladjbot$ $\ladjbot$ $\neg\objB$ $\radjtop$

---

\[\begin{array}{} &&& dot & \unicode{0x2500} & dot \\ && \unicode{0x2571} && \unicode{0x2571} \\ & dot & \unicode{0x2500} & dot \\ \\ && dot & \unicode{0x2500} & dot \\ & \unicode{0x2571} && \unicode{0x2571} \\ dot & \unicode{0x2500} & dot \\ \end{array}\]