- 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$
| $\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}{} \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”, 1966DA, Kelly, Max, “Doctrinal adjunction”, 1974
Draft stuff:
Test: $\tilde f ', {\tilde f}', \tilde{f'}, {f^\circ}', {f'}^\circ $
No comments:
Post a Comment