Basic examples of Kan extension in logic and set theory

We give (some basic examples) of (simple Kan extensions) which are used in (both logic and all branches of mathematics). $\Newextarrow{\xRightarrow}{2,2}{0x21D2}$
We show how (several seemingly different examples) in fact are (manifestations of the same general pattern), interpreted in (different target cartesian closed categories).

---

These examples (are simple) because we extend, not over (a general functor between categories), but merely over (a function between (small) sets).
Thus we start with (a function $\functionf:\setX\to\setY$ between sets).
This fits into (the categorical framework) by considering (the embeddings of $\Set$ into $\bftwo$-$\Cat$ and $\Set$-$\Cat$), which take (sets to discrete enriched categories).

We give two examples of target categories: $\bftwo = \{\bot\lt\top\}$, and $\Set$ itself, basic respectively to Boolean logic and mathematics.
Each is a $\text{ccccc}$ (complete and cocomplete cartesian closed category) thus supports the following operations (among others):

$\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]$.

Given the above, we are interested in situations as shown in (the box at left below).
((The box at right below) will be discussed later.) $$\begin{array}{} \text{the extension situation} && \text{(enriched categorical) formulas for pointwise Kan extension} \\ \boxed{ \begin{smallmatrix}{} \textstyle\setX \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \functionA \mkern1em} & & \mkern{10mu} \textstyle\calV \\ & \llap{\lower3pt\hbox{$\functionf$}}\textstyle\searrow \\ & & \textstyle\setY \\ \end{smallmatrix} } & \mkern8em & \boxed{ \begin{array}{l} \functionA \Ranl\functionf & = & \displaystyle\int_{\eltx\in\setX} \hom - \setY {\eltx\functionf} \power \functionA_\eltx & \text{(4.24)} & \href{https://ncatlab.org/nlab/show/end}{\text{end } (\int_\eltx)} \text{ and } \href{https://ncatlab.org/nlab/show/power}{\text{(cotensor or power) } (\power)} \\ \\ \functionA \Lanl\functionf & = & \displaystyle\int^{\eltx\in\setX} \hom {\eltx\functionf} \setY - \copower \functionA_\eltx & \text{(4.25)} & \href{https://ncatlab.org/nlab/show/end}{\text{coend } (\int^\eltx)} \text{ and } \href{https://ncatlab.org/nlab/show/copower}{\text{(tensor or copower) } (\copower)} \\ \end{array} } \\ \end{array}$$ Here, as above, ($\functionf:\setX\to\setY$) is merely (an arbitrary function in the category $\Set$).
($\functionA:\setX\to\calV$) is (a function/functor) into (either of the cccccs $\bftwo$ or $\Set$);
(an $\functionA:\setX\to\bftwo$) is called (a predicate on $\setX$),
(an $\functionA:\setX\to\Set$) is called (an $\setX$-indexed family of sets).
(By analogy, (a predicate $\functionA:\setX\to\bftwo$) could be called (an “$\setX$-indexed family of Boolean truth values”).)
We are interested in ways of extending $\functionA$ over $\functionf$.

To illustrate, let us take a simple case, where (the $\calV=\bftwo$) and ($\functionf$ is an inclusion of a subset, $\functionf:\setX\subseteq\setY$).
There are $2^{|\setY|-|\setX|}$ possible extensions, where $|\setX|$ denotes the number of elements in $\setX$, etc.
In the partially ordered set of the $2^{|\setY|-|\setX|}$ possible extensions:
one extension is least, taking all of $\setY-\setX$ to $\bot$; it will turn out to be (the left Kan extension $\functionA\Lanl{\setX\subseteq\setY}$);
one extension is greatest, taking all of $\setY-\setX$ to $\top$; it will turn out to be (the right Kan extension $\functionA\Ranl{\setX\subseteq\setY}$).

We wish to generalize this to (arbitrary functions $\functionf$ in $\Set$),
and to include the case when (the target $\calV$ is $\Set$ instead of $\bftwo$).
To do this we use formulas which give (pointwise Kan extensions) into (arbitrary suitably complete and cocomplete enriched categories)
(see, e.g., Max Kelly’s Basic Concepts of Enriched Category Theory or nLab),
specialized to (the situation in the left box above).
(The formulas thus specialized) are shown in (the right box above).
((The numbers in parentheses) refer to (the formulas in Kelly’s BCECT);
following (the reference numbers) are (the names of the operators in the formulas).)

The only (slight) challenge is interpreting (the general operations of enriched category theory) in (the specific target cccccs $\bftwo$ and $\Set$),
then performing (the calculations appropriate in (that particular category))
to transform (the general formula) into (a more familiar form).
We do this in the following display,
first for (the right Kan extensions) for (the targets $\bftwo$ and $\Set$), then for (the left Kan extensions), again for (both targets):

---

$$\begin{array}{} \text{$\bftwo$-$\Cat$} & \text{formulae common to both} & \text{$\Set$-$\CAT$} && \text{$\bftwo$-$\Cat$} \\ \\ \begin{smallmatrix}{} \textstyle\setX \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \functionA \mkern1em} & & \textstyle\bftwo \\ & \llap{\lower3pt\hbox{$\functionf$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Uparrow$} & \textstyle\nearrow & & \mkern-1em \textstyle \functionA\Ranl\functionf = \displaystyle\int_{\eltx\in\setX} \hom - \setY {\eltx\functionf} \power \functionA_\eltx = \boxed{\forall_\functionf \functionA} \\ & & \textstyle\setY \\ \end{smallmatrix} && \begin{smallmatrix}{} \textstyle\setX \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \functionA \mkern1em} & & \textstyle\Set \\ & \llap{\lower3pt\hbox{$\functionf$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Uparrow$} & \textstyle\nearrow & & \mkern-2.5em \textstyle \functionA\Ranl\functionf = \displaystyle\int_{\eltx\in\setX} \hom - \setY {\eltx\functionf} \power \functionA_\eltx = \boxed{\textstyle\prod_\functionf \functionA} = \boxed{\functionA\functionf_\star} \\ & & \textstyle\setY \\ \end{smallmatrix} \\ \\ \\ & (\functionA\Ranl\functionf)_\elty \\ & \mkern4em \displaystyle\int_{\eltx\in\setX} \hom \elty \setY {\eltx\functionf} \power \functionA_\eltx \mkern4em & \\ (\forall\eltx\in\setX) \big[\hom \elty \setY {\eltx\functionf} \Rightarrow \functionA_\eltx \big] && \displaystyle\prod_{\eltx\in\setX} [\hom \elty \setY {\eltx\functionf}, \functionA_\eltx] && \displaystyle\bigwedge_{\eltx\in\setX} [\hom \elty \setY {\eltx\functionf} \Rightarrow \functionA_\eltx] \\ (\forall\eltx\in\setX) \big[ (\elty={\eltx\functionf}) \Rightarrow (\eltx\in\setA) \big] && \left( \displaystyle\prod_{\eltx\notin\functionf\inv\elty} [\emptyset, \functionA_\eltx] \right) \times \left( \displaystyle\prod_{\eltx\in\functionf\inv\elty} [1, \functionA_\eltx] \right) && \left( \displaystyle\bigwedge_{\eltx\notin\functionf\inv\elty} [\bot \Rightarrow \functionA_\eltx] \right) \wedge \left( \displaystyle\bigwedge_{\eltx\in\functionf\inv\elty} [\top \Rightarrow \functionA_\eltx] \right) \\ (\forall\eltx\in\setX) \big[ (\eltx\in\functionf\inv\elty) \Rightarrow (\eltx\in\setA) \big] && 1 \times \left( \displaystyle\prod_{\eltx\in\functionf\inv\elty} \functionA_\eltx \right) && \top \wedge \left( \displaystyle\bigwedge_{\eltx\in\functionf\inv\elty} \functionA_\eltx \right) \\ \functionf\inv\elty \subseteq \setA && \displaystyle\prod_{\eltx\in\functionf\inv\elty} \functionA_\eltx && \displaystyle\bigwedge_{\eltx\in\functionf\inv\elty} \functionA_\eltx \\ (\forall_\functionf \functionA)_\elty && (\prod_\functionf \functionA)_\elty && (\bigwedge_\functionf \functionA)_\elty \\ \\ \Rule{20em}{1px}{1px} & \Rule{10em}{1px}{1px} & \Rule{20em}{1px}{1px} \\ \\ \\ \begin{smallmatrix}{} \textstyle\setX \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \functionA \mkern1em} & & \textstyle\bftwo \\ & \llap{\lower3pt\hbox{$\functionf$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Downarrow$} & \textstyle\nearrow & & \mkern-1em \textstyle \functionA \Lanl\functionf = \displaystyle\int^{\eltx\in\setX} \hom {\eltx\functionf} \setY - \copower \functionA_\eltx = \boxed{\exists_\functionf \functionA} \\ & & \textstyle\setY \\ \end{smallmatrix} && \begin{smallmatrix}{} \textstyle\setX \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \functionA \mkern1em} & & \textstyle\Set \\ & \llap{\lower3pt\hbox{$\functionf$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Downarrow$} & \textstyle\nearrow & & \mkern-2.5em \textstyle \functionA \Lanl\functionf = \displaystyle\int^{\eltx\in\setX} \hom {\eltx\functionf} \setY - \copower \functionA_\eltx = \boxed{\textstyle\sum_\functionf \functionA} = \boxed{\functionA \functionf_!} \\ & & \textstyle\setY \\ \end{smallmatrix} \\ \\ \\ & (\functionA \Lanl\functionf)_\elty \\ & \displaystyle\int^{\eltx\in\setX} \hom {\eltx\functionf} \setY \elty \copower \functionA_\eltx & \\ (\exists\eltx\in\setX)(\hom {\eltx\functionf} \setY \elty \wedge \functionA_\eltx) && \displaystyle\sum_{\eltx\in\setX} (\hom {\eltx\functionf} \setY \elty \times \functionA_\eltx) && \displaystyle\bigvee_{\eltx\in\setX} (\hom {\eltx\functionf} \setY \elty \wedge \functionA_\eltx) \\ (\exists\eltx\in\setX)({\eltx\functionf}=\elty \wedge \eltx\in\setA) && \left(\displaystyle\sum_{\eltx\notin\functionf\inv\elty} \emptyset \times \functionA_\eltx\right) + \left(\displaystyle\sum_{\eltx\in\functionf\inv\elty} 1 \times \functionA_\eltx\right) && \left(\displaystyle\bigvee_{\eltx\notin\functionf\inv\elty} \bot \wedge \functionA_\eltx\right) \vee \left(\displaystyle\bigvee_{\eltx\in\functionf\inv\elty} \top \wedge \functionA_\eltx\right) \\ (\exists\eltx\in\setA){(\eltx\functionf}=\elty) && \emptyset + \left( \displaystyle\sum_{\eltx\in\functionf\inv\elty} \functionA_\eltx \right) && \bot \vee \left( \displaystyle\bigvee_{\eltx\in\functionf\inv\elty} \functionA_\eltx \right) \\ \elty\in\setA\functionf && \displaystyle\sum_{\eltx\in\functionf\inv\elty} \functionA_\eltx && \displaystyle\bigvee_{\eltx\in\functionf\inv\elty} \functionA_\eltx \\ (\exists_\functionf \functionA)_\elty && (\sum_\functionf \functionA)_\elty && (\bigvee_\functionf \functionA)_\elty \\ \end{array}$$

---

The special cases

$$\begin{array}{} \text{$\bftwo$-$\Cat$} & \mkern10em & \text{$\Set$-$\CAT$} \\ \\ \begin{smallmatrix}{} \textstyle\setX \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \functionA \mkern1em} & & \textstyle\bftwo \\ & \llap{\lower3pt\hbox{$!_\setX$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Uparrow$} & \textstyle\nearrow & & \mkern-1em \textstyle \forall_{!_\setX}\functionA = (\forall\eltx\in\setX)\functionA_\eltx\\ & & \textstyle 1\\ \end{smallmatrix} && \begin{smallmatrix}{} \textstyle\setX \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \functionA \mkern1em} & & \textstyle\Set \\ & \llap{\lower3pt\hbox{$!_\setX$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Uparrow$} & \textstyle\nearrow & & \mkern-2.5em \textstyle \prod_{!_\setX}\functionA = \displaystyle\prod_{\eltx\in\setX} \functionA_\eltx \\ & & \textstyle 1 \\ \end{smallmatrix} \\ \\ \begin{smallmatrix}{} \textstyle\setX \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \functionA \mkern1em} & & \textstyle\bftwo \\ & \llap{\lower3pt\hbox{$!_\setX$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Downarrow$} & \textstyle\nearrow & & \mkern-1em \textstyle \exists_{!_\setX}\functionA = (\exists\eltx\in\setX)\functionA_\eltx\\ & & \textstyle 1\\ \end{smallmatrix} && \begin{smallmatrix}{} \textstyle\setX \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \functionA \mkern1em} & & \textstyle\Set \\ & \llap{\lower3pt\hbox{$!_\setX$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Downarrow$} & \textstyle\nearrow & & \mkern-2.5em \textstyle \sum_{!_\setX}\functionA = \displaystyle\sum_{\eltx\in\setX} \functionA_\eltx \\ & & \textstyle 1 \\ \end{smallmatrix} \\ \\ \\ \\ \begin{smallmatrix}{} \textstyle\emptyset \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \Box_\bftwo \mkern1em} & & \textstyle\bftwo \\ & \llap{\lower3pt\hbox{$\Box_1 = {!_\emptyset}$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Uparrow$} & \textstyle\nearrow & & \mkern-1em \textstyle \forall_{\Box_1}\Box_\bftwo = (\forall\eltx\in\emptyset) = \top \\ & & \textstyle 1 \\ \end{smallmatrix} && \begin{smallmatrix}{} \textstyle\emptyset \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \Box_\Set \mkern1em} & & \textstyle\Set \\ & \llap{\lower3pt\hbox{$\Box_1 = {!_\emptyset}$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Uparrow$} & \textstyle\nearrow & & \mkern-2.5em \textstyle \prod_{\Box_1}\Box_\Set = \displaystyle\prod_{\eltx\in\emptyset} = 1 \\ & & \textstyle 1 \\ \end{smallmatrix} \\ \\ \begin{smallmatrix}{} \textstyle\emptyset \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \Box_\bftwo \mkern1em} & & \textstyle\bftwo \\ & \llap{\lower3pt\hbox{$\Box_1 = {!_\emptyset}$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Downarrow$} & \textstyle\nearrow & & \mkern-1em \textstyle \exists_{\Box_1}\Box_\bftwo = (\exists\eltx\in\emptyset) = \bot \\ & & \textstyle 1 \\ \end{smallmatrix} && \begin{smallmatrix}{} \textstyle\emptyset \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \Box_\Set\mkern1em} & & \textstyle\Set \\ & \llap{\lower3pt\hbox{$\Box_1 = {!_\emptyset}$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Downarrow$} & \textstyle\nearrow & & \mkern-2.5em \textstyle \sum_{\Box_1}\Box_\Set = \displaystyle\sum_{\eltx\in\emptyset} = \emptyset \\ & & \textstyle 1 \\ \end{smallmatrix} \\ \\ \\ \\ \\ \begin{smallmatrix}{} \textstyle\emptyset \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \Box_\bftwo \mkern1em} & & \textstyle\bftwo \\ & \llap{\lower3pt\hbox{$\Box_\setY$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Uparrow$} & \textstyle\nearrow & & \mkern-1em \textstyle \forall_{\Box_\setY}\Box_\bftwo = (\forall\eltx\in\emptyset) = {!_\setY\top} \\ & & \textstyle\setY \\ \end{smallmatrix} && \begin{smallmatrix}{} \textstyle\emptyset \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \Box_\Set\mkern1em} & & \textstyle\Set \\ & \llap{\lower3pt\hbox{$\Box_\setY$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Uparrow$} & \textstyle\nearrow & & \mkern-2.5em \textstyle \prod_{\Box_\setY}\Box_\Set = \displaystyle\prod_{\eltx\in\emptyset} = {!_\setY 1} \\ & & \textstyle\setY \\ \end{smallmatrix} \\ \\ \begin{smallmatrix}{} \textstyle\emptyset \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \Box_\bftwo\mkern1em} & & \textstyle\bftwo \\ & \llap{\lower3pt\hbox{$\Box_\setY$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Downarrow$} & \textstyle\nearrow & & \mkern-1em \textstyle \exists_{\Box_\setY}\Box_\bftwo = (\exists\eltx\in\emptyset) = {!_\setY\bot} \\ & & \textstyle\setY \\ \end{smallmatrix} && \begin{smallmatrix}{} \textstyle\emptyset \mkern{10mu} & & \xrightarrow{\textstyle \mkern1em \Box_\Set \mkern1em} & & \textstyle\Set \\ & \llap{\lower3pt\hbox{$\Box_\setY$}}\textstyle\searrow & \raise10pt\hbox{$\textstyle\big\Downarrow$} & \textstyle\nearrow & & \mkern-2.5em \textstyle \sum_{\Box_\setY}\Box_\Set = \displaystyle\sum_{\eltx\in\emptyset} = {!_\setY\emptyset} \\ & & \textstyle\setY \\ \end{smallmatrix} \\ \end{array}$$

---

Kan extension adjunctions

A little notation: We use $\calV$ as a variable standing for (either of the $\text{ccccc}$s $\bftwo$ or $\Set$).
As $\text{ccccc}$s, either can be used as a base for enrichment, as in the theory of enriched categories,
and (using $\calV$ for an arbitrary base for enrichment) is fairly standard (at least it is what is used in Kelly’s book BCECT).
$[ \setX, \calV ]$ denotes the (ordinary, mere) category of functors and natural transformations from the discrete category $\setX$ to $\calV$, and likewise for the discrete category $\setY$.
With these notations, we have, for each function $\functionf:\setX\to\setY$ in $\Set$, an adjoint triple (adjoint string of length 3).
The adjoint triple is shown (in $\CAT$) twice, once oriented vertically and once horizontally; each has its advantages. $$\mkern-3.5em \begin{array}{cccccccl} &&& {} \rlap { \mkern-280mu \boxed { \mkern1ex \begin{array}{} \setX \\ & \searrow \raise4pt\hbox{$\mkern-10mu \functionA$} \\ \llap\functionf \Big\downarrow & {\mkern-1em \Downarrow\Uparrow} & \mkern-1em\calV \\ & \nearrow \lower4pt\hbox{$\mkern-10mu \functionB$} \\ \setY \\ \end{array} } \mkern2em \boxed { \begin{array}{} [ \setX, \calV ] \\ (\Lan_\functionf = \functionf_!) \Bigg\downarrow \dashv \functionf^\star \Bigg\uparrow \dashv \Bigg\downarrow (\Ran_\functionf = \functionf_\star) \\ [ \setY, \calV ] \\ \end{array} } } && \subset & \CAT \\ &&& {} \rlap { \mkern-125mu \boxed { [\setX,\calV] \mkern1em \begin{array}{} \xrightarrow{\textstyle \;\;\Lan_\functionf = \functionf_!\;\;} \\ \xleftarrow{\textstyle \functionf^\star} \\ \xrightarrow{\textstyle \Ran_\functionf = \functionf_\star} \\ \end{array} \mkern1em [\setY,\calV] } } && \subset & \CAT \\ &&& {} \rlap { \mkern-110mu \boxed { \begin{array}{} \setX && \xrightarrow{\textstyle \mkern1em \functionf \mkern1em } && \setY \\ & \llap{\functionA} \searrow & \smash{\textstyle\llap\alpha\Rightarrow \atop {\textstyle\Leftarrow\rlap\gamma}} & \swarrow \rlap{\functionB} \\ && \calV \\ \end{array} } } && \subset & \CAT \\ \\ &&& {} \rlap{\mkern-96mu \boxed { \mkern1ex \begin{array}{} \setX & \xlongequal{} & \setX & \xlongequal{} & \setX \\ && \Big\downarrow \rlap{\mkern-14mu\functionf} \\ \smash { \llap{\functionA}\Bigg\downarrow } & \xRightarrow{\smash{\textstyle\alpha}} & \setY & \xRightarrow{\smash{\textstyle\gamma}} & \smash { \Bigg\downarrow\rlap{\functionA} } \\ && \Big\downarrow\rlap{\mkern-15mu\functionB} \\ \calV & \xlongequal{} & \calV & \xlongequal{} & \calV \\ \end{array} \mkern1ex } } && \subset & \CAT \\ &&& \Bigg\vert \mkern-1mu \Bigg\vert \mkern-1mu \Bigg\vert \\ &&& {} \rlap{\mkern-228mu \boxed { \mkern1ex \begin{array}{} \setX && \xlongequal{\phantom{\Longrightarrow}} && \setX && \xlongequal{\phantom{\Longrightarrow}} && \setX \\ &&&& \Big\downarrow \rlap{\mkern-14mu\functionf} \\ \smash { \llap{\functionA}\Bigg\downarrow } & \xRightarrow{ \smash { \textstyle\mkern1ex \boxed{\functionA\eta} \mkern1ex } } & \setY & \xlongequal{} & \setY & \xlongequal{} & \setY & \xRightarrow{ \smash { \textstyle\mkern1ex \boxed{\functionA\epsilon} \mkern1ex } } & \smash { \Bigg\downarrow\rlap{\functionA} } \\ && \Big\downarrow\rlap{\mkern-20mu\functionA\functionf_!} & \xRightarrow[\smash{\textstyle\beta}]{} & \Big\downarrow\rlap{\mkern-15mu\functionB} & \xRightarrow[\smash{\textstyle\delta}]{} & \Big\downarrow\rlap{\mkern-20mu\functionA\functionf_\star} \\ \calV & \xlongequal{} & \calV & \xlongequal{} & \calV & \xlongequal{} & \calV & \xlongequal{} & \calV \\ \end{array} \mkern1ex } } && \subset & \CAT \\ \\ (\Lan_\functionf = \functionf_!) & \dashv & \functionf^\star & \mkern2em & \functionf^\star & \dashv & (\functionf_\star = \Ran_\functionf) & \text{the two adjunctions} \\ \functionA & \xRightarrow{\textstyle \boxed{\functionA\eta} } & \big( \functionA \functionf_! \functionf^\star = \functionf (\functionA \functionf_!) = (\functionA \functionf_!)_\functionf \big) & & \big( \functionA \functionf_\star\functionf^\star = \functionf (\functionA \functionf_\star) = (\functionA \functionf_\star)_\functionf \big) & \xRightarrow{\textstyle \boxed{\functionA\epsilon}} & \functionA & \text{(unit $\functionA\eta$ for $\functionf_! \dashv \functionf^\star$) and (counit $\functionA\epsilon$ for $\functionf^\star \dashv \functionf_\star$), both transformations in $[\setX,\calV]$} \\ \\ \Rule{3em}{1px}{1px} & \Rule{2em}{1px}{1px} & \Rule{8em}{1px}{1px} & & \Rule{8em}{1px}{1px} & \Rule{2em}{1px}{1px} & \Rule{3em}{1px}{1px} & \Rule{20em}{1px}{1px} \\ \\ \functionA & \xRightarrow{\smash { \textstyle \alpha} } & ( \functionB\functionf^\star = \functionf\functionB = \functionB_\functionf ) & & ( \functionB\functionf^\star = \functionf\functionB = \functionB_\functionf ) & \xRightarrow{\smash { \textstyle \gamma } } & \functionA \\ &&&&&&& \text{$\eltx_0$-component of transformations in $[\setX,\calV]$} \\ \functionA_{\eltx_0} & \xrightarrow{\smash { \textstyle \alpha_{\eltx_0} } } & \functionB_{\eltx_0\functionf} & & \functionB_{\eltx_0\functionf} & \xrightarrow{\smash { \textstyle \gamma_{\eltx_0} } } &\functionA_{\eltx_0} \\ &&&&&&& \text{“name of” bijection ($v$) (ECT (1.25))} \\ \objI & \xrightarrow{\smash { \textstyle \alpha_{\eltx_0} } } & [\functionA_{\eltx_0},\functionB_{\eltx_0\functionf}] & & \objI & \xrightarrow{\smash { \textstyle \gamma_{\eltx_0} } } & [\functionB_{\eltx_0\functionf},\functionA_{\eltx_0}] \\ &&&&&&& \href{http://kwhmath.blogspot.com/2014/03/the-identities-are-free-yoneda-lemma.html}{\text{Yoneda (identities-are-free) bijection (ECT (1.46) and ff.)} } \\ \hom {\eltx_0\functionf} \setY \elty & \xrightarrow{} & [\functionA_{\eltx_0},\functionB_\elty] & & \hom \elty \setY {\eltx_0\functionf} & \xrightarrow{} &[\functionB_\elty,\functionA_{\eltx_0}] \\ &&&&&&& \text{definition of copower ($\copower$)} \\ \phantom{\int^\eltx} \hom {\eltx_0\functionf} \setY \elty \copower \functionA_{\eltx_0} & \xrightarrow{} & \setB_\elty && \hom \elty \setY {\eltx_0\functionf} \copower \setB_\elty & \xrightarrow{} & \functionA_{\eltx_0} & \text{in the $\Ran$ case, extra step added to show the symmetry} \\ &&&&&&& \text{definition of power ($\power$)} \\ \phantom{\int^\eltx} \hom {\eltx_0\functionf} \setY \elty \copower \functionA_{\eltx_0} && & & && \phantom{\int_\eltx} \hom \elty \setY {\eltx_0\functionf} \power \functionA_{\eltx_0} \\ \mkern34mu\llap{\hom \elty \iota {\eltx_0}} \Bigg\downarrow \rlap{\text{univ. cocone}} & \mkern2em \searrow \mkern-1em\rlap{\raise1ex{\text{cocone to the vertex (sink) $\functionB_\elty$}}} & & & & \llap{\raise1ex{\text{cone from the vertex (source) $\functionB_\elty$}}} \nearrow & \mkern30mu \llap{\text{univ. cone}}\Bigg\uparrow\rlap{\hom \elty \pi {\eltx_0}} & \text{universal properties of coend ($\int^\eltx, \iota$) and end ($\int_\eltx, \pi$)} \\ \int^\eltx \hom {\eltx\functionf} \setY \elty \copower \functionA_\eltx & \xrightarrow[\smash{\textstyle \beta_\elty}]{} & \setB_\elty & & \setB_\elty & \xrightarrow[\smash{\textstyle \delta_\elty}]{} & \int_\eltx \hom \elty \setY {\eltx\functionf} \power \functionA_\eltx \\ &&&&&&& \text{$\elty$-component of transformations in $[\setY,\calV]$} \\ (\functionA\functionf_! = \functionA\Lanl\functionf) & \xRightarrow[\smash{\textstyle \beta}]{} & \functionB & & \functionB & \xRightarrow[\smash{\textstyle \delta}]{} & (\functionA\functionf_\star = \functionA\Ranl\functionf) \\ \\ \Rule{3em}{1px}{1px} & \Rule{2em}{1px}{1px} & \Rule{8em}{1px}{1px} & & \Rule{8em}{1px}{1px} & \Rule{2em}{1px}{1px} & \Rule{3em}{1px}{1px} & \Rule{20em}{1px}{1px} \\ \\ (\functionB\functionf^\star\functionf_! = \functionB_\functionf \Lanl\functionf) & \xRightarrow[\textstyle \boxed{\functionB\epsilon}]{} & \functionB & & \functionB & \xRightarrow[\textstyle \boxed{\functionB \eta}]{} & (\functionB\functionf^\star\functionf_\star = \functionB_\functionf \Ranl\functionf) & \text{(counit $\functionB\epsilon$ for $\functionf_! \dashv \functionf^\star$) and (unit $\functionB\eta$ for $\functionf^\star \dashv \functionf_\star$), both transformations in $[\setY,\calV]$} \\ \\ \end{array}$$

---

Units and counits of the Kan adjunctions

(The units $\eta$ and counits $\epsilon$) of the adjunctions $\big((\Lan_\functionf = \functionf_!) \dashv \functionf^\star\big)$ and $\big(\functionf^\star \dashv (\Ran_\functionf = \functionf_\star)\big)$ may be computed by
setting (the bottom or top arrows in the center part of the above display) to be identities, then following through (the chains of bijections).
(The following) performs (that computation),
first for $\functionA\eta$ and $\functionA\epsilon$ in $[\setX,\calV]$,
then for $\functionB\epsilon$ and $\functionB\eta$ in $[\setY,\calV]$:

$$\mkern-3.5em \begin{array}{cccccccl} \functionf_! & \dashv & \functionf^\star & \mkern2em & \functionf^\star & \dashv & \functionf_\star \\ \\ &&& {} \rlap{\mkern-106mu \boxed { \mkern1ex \begin{array}{} \setX & \xlongequal{} & \setX & \xlongequal{} & \setX \\ && \Big\downarrow \rlap{\mkern-14mu\functionf} \\ \smash { \llap{\functionA}\Bigg\downarrow } & \Longrightarrow & \setY & \Longrightarrow & \smash { \Bigg\downarrow\rlap{\functionA} } \\ && \Big\downarrow\rlap{\mkern-15mu\functionB} \\ \calV & \xlongequal{} & \calV & \xlongequal{} & \calV \\ \end{array} \mkern1ex } } && \subset & \CAT \\ &&& \Bigg\vert \mkern-1mu \Bigg\vert \mkern-1mu \Bigg\vert \\ &&& {} \rlap{\mkern-230mu \boxed { \mkern1ex \begin{array}{} \setX && \xlongequal{\phantom{\Longrightarrow}} && \setX && \xlongequal{\phantom{\Longrightarrow}} && \setX \\ &&&& \Big\downarrow \rlap{\mkern-14mu\functionf} \\ \smash { \llap{\functionA}\Bigg\downarrow } & \xRightarrow{ \smash { \textstyle \mkern1ex \boxed{\functionA\eta} \mkern1ex } } & \setY & \xlongequal{} & \setY & \xlongequal{} & \setY & \xRightarrow{ \smash { \textstyle\mkern1ex \boxed{\functionA\epsilon} \mkern1ex } } & \smash { \Bigg\downarrow\rlap{\functionA} } \\ && \Big\downarrow\rlap{\mkern-20mu\functionA\functionf_!} & \Longrightarrow & \Big\downarrow\rlap{\mkern-15mu\functionB} & \Longrightarrow & \Big\downarrow\rlap{\mkern-20mu\functionA\functionf_\star} \\ \calV & \xlongequal{} & \calV & \xlongequal{} & \calV & \xlongequal{} & \calV & \xlongequal{} & \calV \\ \end{array} \mkern1ex } } && \subset & \CAT \\ \\ \functionA & \xRightarrow{\textstyle \boxed{\functionA\eta} } & \big( \functionA\functionf_!\functionf^\star = \functionf(\functionA\functionf_!) = (\functionA\functionf_!)_\functionf \big) & & \big( \functionA\functionf_\star\functionf^\star = \functionf(\functionA\functionf_\star) = (\functionA\functionf_\star)_\functionf \big) & \xRightarrow{\textstyle \boxed{\functionA\epsilon} } & \functionA \\ &&&&&&& \\ \objI \copower \functionA_{\eltx_0} & \xrightarrow{\textstyle 1_{\eltx_0\functionf}\copower\functionA_{\eltx_0}} & \hom {\eltx_0\functionf} \setY {\eltx_0\functionf} \copower \functionA_{\eltx_0} && \hom {\eltx_0\functionf} \setY {\eltx_0\functionf} \power \functionA_{\eltx_0} & \xrightarrow{\textstyle 1_{\eltx_0\functionf} \power \functionA_{\eltx_0}} & \objI \power \functionA_{\eltx_0} & \text{equivalent forms of the components} \\ \llap{(1.4) \;} {\wr\vert\vert} && \downarrow \rlap{\hom {\eltx_0\functionf} \iota {\eltx_0}} && \llap{\hom {\eltx_0\functionf} \pi {\eltx_0}} \uparrow && \wr\vert\vert \rlap{\; (1.26)} \\ \functionA_{\eltx_0} & \xrightarrow{ \smash { \textstyle (\functionA\eta)_{\eltx_0} } } & \big( (\functionA\functionf_!)_{\eltx_0\functionf} = \int^\eltx \hom {\eltx\functionf} \setY {\eltx_0\functionf} \copower \functionA_\eltx \big) & & \big( (\functionA\functionf_\star)_{\eltx_0\functionf} = \int_\eltx \hom {\eltx_0\functionf} \setY {\eltx\functionf} \power \functionA_\eltx \big) & \xrightarrow { \smash { \textstyle (\functionA\epsilon)_{\eltx_0} } } & \setA_{\eltx_0} & \text{$\eltx_0$-components of transformations $\functionA\eta$ and $\functionA\epsilon$} \\ &&&&&&& \text{“name of” bijection (ECT (1.25))} \\ \objI & {} \xrightarrow[\smash { \textstyle 1_{\eltx_0\functionf} }]{} \hom {\eltx_0\functionf} \setY {\eltx_0\functionf} \xrightarrow [ \smash { \textstyle \widetilde{ \hom {\eltx_0\functionf} \iota {\eltx_0} } } ]{} {} & \Big[ \functionA_{\eltx_0},\int^\eltx \hom {\eltx\functionf} \setY {\eltx_0\functionf} \copower \functionA_\eltx \Big] & & I & {} \xrightarrow[ \smash { \textstyle 1_{\eltx_0\functionf} } ]{} \hom {\eltx_0\functionf} \setY {\eltx_0\functionf} \xrightarrow[ \smash { \textstyle \overline{\hom {\eltx_0\functionf} \pi {\eltx_0} } } ]{} {} & \Big[ \int_\eltx \hom {\eltx_0\functionf} \setY {\eltx\functionf} \power \functionA_\eltx , \setA_{\eltx_0} \Big] \\ &&&&&&& \href{http://kwhmath.blogspot.com/2014/03/the-identities-are-free-yoneda-lemma.html}{\text{Yoneda (identities-are-free) bijection (ECT (1.46) and ff.)} } \\ \hom {\eltx_0\functionf} \setY \elty & \xrightarrow [ \smash { \textstyle \widetilde{ \hom \elty \iota {\eltx_0} } } ]{} & \Big[ \functionA_{\eltx_0},\int^\eltx \hom {\eltx\functionf} \setY \elty \copower \functionA_\eltx \Big] & & \hom \elty \setY {\eltx_0\functionf} & \xrightarrow [ \smash { \textstyle \overline { \hom \elty {\pi} {\eltx_0} } } ]{} & \Big[ \int_\eltx \hom \elty \setY {\eltx\functionf} \power \functionA_\eltx , \setA_{\eltx_0} \Big] \\ &&&&&&& \text{definitions of copower ($\copower$) and power ($\power$)} \\ \phantom{\int^\eltx} \hom {\eltx_0\functionf} \setY \elty \copower \functionA_{\eltx_0} && & & && \phantom{\int_\eltx} \hom \elty \setY {\eltx_0\functionf} \power \functionA_{\eltx_0} \\ \mkern34mu\llap{\hom \elty \iota {\eltx_0}} \Bigg\downarrow & \searrow \raise6pt\hbox{$\mkern-10mu \hom \elty \iota {\eltx_0}$} & & & & \raise6pt\hbox{$\hom \elty \pi {\eltx_0}$} \mkern-10mu \nearrow & \mkern30mu\Bigg\uparrow\rlap{\hom \elty \pi {\eltx_0}} & \text{universal maps of coend ($\int^\eltx, \iota$) and end ($\int_\eltx, \pi$)} \\ \int^\eltx \hom {\eltx\functionf} \setY \elty \copower \functionA_\eltx & \xrightarrow[\smash { \textstyle 1_{(\functionA\functionf_!)_\elty} } ]{} & \int^\eltx \hom {\eltx\functionf} \setY \elty \copower \functionA_\eltx & & \int_\eltx \hom \elty \setY {\eltx\functionf} \power \functionA_\eltx & \xrightarrow[\smash { \textstyle 1_{(\functionA\functionf_\star)_\elty} } ]{} & \int_\eltx \hom \elty \setY {\eltx\functionf} \power \functionA_\eltx \\ &&&&&&& \\ (\functionA\functionf_! = \functionA\Lanl\functionf) & \xRightarrow[\smash { \textstyle 1_{\functionA\functionf_!} } ]{} & (\functionA\functionf_! = \functionA\Lanl\functionf) & & (\functionA\functionf_\star = \functionA\Ranl\functionf) & \xRightarrow[\smash { \textstyle 1_{\functionA\functionf_\star} } ]{} & (\functionA\functionf_\star = \functionA\Ranl\functionf) & \text{identity transformations on $\functionA\functionf_!$ and $\functionA\functionf_\star$} \\ \\ \Rule{3em}{1px}{1px} & \Rule{2em}{1px}{1px} & \Rule{8em}{1px}{1px} & & \Rule{8em}{1px}{1px} & \Rule{2em}{1px}{1px} & \Rule{3em}{1px}{1px} & \Rule{20em}{1px}{1px} \\ \\ \functionB_\functionf & \xRightarrow{\textstyle 1_{\functionB\functionf^\star} = 1_{\functionB_\functionf}} & \big( \functionB\functionf^\star = \functionf\functionB = \functionB_\functionf \big) & & \big( \functionB\functionf^\star = \functionf\functionB = \functionB_\functionf \big) & \xRightarrow{\textstyle 1_{\functionB\functionf^\star} = 1_{\functionB_\functionf}} & \functionB_\functionf & \text{identity transformation on $\functionB\functionf^\star$} \\ &&&&&&& \\ \functionB_{\eltx\functionf} & \xrightarrow{\smash { \textstyle 1_{\functionB_{\eltx\functionf}} } } & \functionB_{\eltx\functionf} & & \functionB_{\eltx\functionf} & \xrightarrow{\smash { \textstyle 1_{\functionB_{\eltx\functionf}} } } & \functionB_{\eltx\functionf} \\ &&&&&&& \text{“name of” bijection (ECT (1.25))} \\ \objI & \xrightarrow{\smash { \textstyle 1_{\functionB_{\eltx\functionf}} } } & [\functionB_{\eltx\functionf},\functionB_{\eltx\functionf}] & & \objI & \xrightarrow{\smash { \textstyle 1_{\functionB_{\eltx\functionf}} } } & [\functionB_{\eltx\functionf},\functionB_{\eltx\functionf}] \\ &&&&&&& \href{http://kwhmath.blogspot.com/2014/03/the-identities-are-free-yoneda-lemma.html}{\text{Yoneda (identities-are-free) bijection (ECT (1.46) and ff.)} } \\ \hom {\eltx\functionf} \setY \elty & \xrightarrow[ \smash { \textstyle \hom {\eltx\functionf} \functionB \elty } ]{} & [\functionB_{\eltx\functionf},\functionB_\elty] & & \hom \elty \setY {\eltx\functionf} & \xrightarrow[ \smash { \textstyle \hom \elty \functionB {\eltx\functionf} } ]{}&[\functionB_\elty,\functionB_{\eltx\functionf}] \\ &&&&&&& \text{definitions of copower ($\copower$) and power ($\power$)} \\ \phantom{\int^\eltx} \hom {\eltx\functionf} \setY \elty \copower \functionB_{\eltx\functionf} && & & && \phantom{\int_\eltx} \hom \elty \setY {\eltx\functionf} \power \functionB_{\eltx\functionf} \\ \mkern34mu\llap{\hom \elty \iota \eltx} \Bigg\downarrow & \searrow \raise6pt\hbox{$\mkern-10mu \widetilde{\hom {\eltx\functionf} \functionB \elty}$} & & & & \raise6pt\hbox{$\overline{\hom \elty \functionB {\eltx\functionf}}$} \mkern-10mu \nearrow & \mkern30mu\Bigg\uparrow\rlap{\hom \elty \pi \eltx} & \text{universal properties of coend ($\int^\eltx, \iota$) and end ($\int_\eltx, \pi$)} \\ \int^\eltx \hom {\eltx\functionf} \setY \elty \copower \functionB_{\eltx\functionf} & \xrightarrow[\smash{\textstyle (\functionB\epsilon)_y}]{} & \setB_\elty & & \setB_\elty & \xrightarrow[\smash{\textstyle (\functionB\eta)_y}]{} & \int_\eltx \hom \elty \setY {\eltx\functionf} \power \functionB_{\eltx\functionf} \\ &&&&&&& \text{$\elty$-component of transformations $\functionB\epsilon$ and $\functionB\eta$} \\ (\functionB\functionf^\star\functionf_! = \functionB_\functionf\Lanl\functionf) & \xRightarrow[\textstyle \boxed{\functionB\epsilon}]{} & \functionB & & \functionB & \xRightarrow[\textstyle \boxed{\functionB\eta}]{} & (\functionB\functionf^\star\functionf_\star = \functionB_\functionf\Ranl\functionf) \\ \\ &&& {} \rlap{\mkern-106mu \boxed { \mkern1ex \begin{array}{} \setX & \xlongequal{} & \setX & \xlongequal{} & \setX \\ \llap\functionf \Big\downarrow && \Big\downarrow \rlap{\mkern-14mu\functionf} && \Big\downarrow \rlap\functionf \\ \setY & \xRightarrow{ \smash { \textstyle 1_{\functionf\functionB} } } & \setY & \xRightarrow{ \smash { \textstyle 1_{\functionf\functionB} } } & \setY \\ \llap\functionB \Big\downarrow && \Big\downarrow\rlap{\mkern-15mu\functionB} && \Big\downarrow \rlap\functionB \\ \calV & \xlongequal{} & \calV & \xlongequal{} & \calV \\ \end{array} \mkern1ex } } && \subset & \CAT \\ &&& \Bigg\vert \mkern-1mu \Bigg\vert \mkern-1mu \Bigg\vert \\ &&& {} \rlap{\mkern-230mu \boxed { \mkern1ex \begin{array}{} \setX && \xlongequal{\phantom{\Longrightarrow}} && \setX && \xlongequal{\phantom{\Longrightarrow}} && \setX \\ \llap\functionf \Big\downarrow &&&& \Big\downarrow \rlap{\mkern-14mu\functionf} &&&& \Big\downarrow \rlap\functionf \\ \setY & \xRightarrow{ \smash { \textstyle\mkern1ex (\functionf\functionB)\eta \mkern1ex} } & \setY & \xlongequal{} & \setY & \xlongequal{} & \setY & \xRightarrow{ \smash { \textstyle\mkern1ex (\functionf\functionB)\epsilon \mkern1ex } } & \setY \\ \llap\functionB \Bigg\downarrow && \Bigg\downarrow\rlap{\mkern-20mu (\functionf\functionB)_!} & \xRightarrow[ \smash { \textstyle \boxed{\functionB\epsilon} } ]{} & \Bigg\downarrow\rlap{\mkern-15mu\functionB} & \xRightarrow[ \smash { \textstyle \boxed{\functionB\eta} } ]{} & \Bigg\downarrow\rlap{\mkern-20mu(\functionf\functionB)_\star} && \Bigg\downarrow \rlap\functionB \\ \calV & \xlongequal{} & \calV & \xlongequal{} & \calV & \xlongequal{} & \calV & \xlongequal{} & \calV \\ \end{array} \mkern1ex } } && \subset & \CAT \\ \end{array}$$

Duplicate of part of the computation for (the counit $\functionA\epsilon$ of $\functionf^\star \dashv (\functionf_\star = \Ran_\functionf)$, evaluated at an element $\eltx_0\in\setX$):: $$\begin{array}{cccccl} (\functionA\functionf_\star\functionf^\star)_{\eltx_0} = (\functionA\Ranl\functionf)_{\eltx_0\functionf} & \xlongequal{} & \int_\eltx \hom {\eltx_0\functionf} \setY {\eltx\functionf} \power \functionA_\eltx & \xrightarrow {\textstyle (\functionA\epsilon)_{\eltx_0}} & \setA_{\eltx_0} \\ &&&&& \text{“name of” bijection (ECT (1.25))} \\ I & \xrightarrow{\textstyle 1_{\eltx_0\functionf} } & \hom {\eltx_0\functionf} \setY {\eltx_0\functionf} & \xrightarrow{\textstyle \overline{\hom {\eltx_0\functionf} \pi {\eltx_0} } } & \left[ \int_\eltx \hom {\eltx_0\functionf} \setY {\eltx\functionf} \power \functionA_\eltx , \setA_{\eltx_0} \right] \\ &&&&& \text{Yoneda bijection} \\ && \hom \elty \setY {\eltx_0\functionf} & \xrightarrow{\textstyle \overline{\hom \elty \pi {\eltx_0} } } & \left[ \int_\eltx \hom \elty \setY {\eltx\functionf} \power \functionA_\eltx , \setA_{\eltx_0} \right] \\ &&&&& \text{transpose under the definition of power ($\power$)} \\ (\functionA\functionf_\star)_\elty = (\functionA\Ranl\functionf)_\elty & \xlongequal{} & \int_\eltx \hom \elty \setY {\eltx\functionf} \power \functionA_\eltx & \xrightarrow{\textstyle \hom \elty \pi {\eltx_0} } & \hom \elty \setY {\eltx_0\functionf} \power \functionA_{\eltx_0} \\ &&&&& \text{($\eltx_0$-component) of (universal map $\hom \elty \pi {}$) for (the end for $(\functionA\Ranl\functionf)_\elty$) } \\ \end{array}$$ There are equivalent forms of components (again evaluated at an element $\eltx_0\in\setX$) of the resulting transformations: $$\begin{array}{} (\functionA\eta)_{\eltx_0} & : & \functionA_{\eltx_0} \buildrel {\text{(1.4)}} \over \cong I \copower \functionA_{\eltx_0} \xrightarrow{\textstyle 1_{\eltx_0\functionf}\copower\functionA_{\eltx_0}} \hom {\eltx_0\functionf} \setY {\eltx_0\functionf} \copower \functionA_{\eltx_0} \xrightarrow{\textstyle \hom {\eltx_0\functionf\,} \iota {\,\eltx_0}} \displaystyle\int^{\eltx\in\setX} \hom {\eltx\functionf} \setY {\eltx_0\functionf} \copower \functionA_\eltx = (\functionA\Lanl\functionf)_{\eltx_0\functionf} \\ (\functionA\epsilon)_{\eltx_0} & : & (\functionA\Ranl\functionf)_{\eltx_0\functionf} = \displaystyle\int_{\eltx\in\setX} \hom {\eltx_0\functionf} \setY {\eltx\functionf} \power \functionA_\eltx \xrightarrow{\textstyle \hom {\eltx_0\functionf} \pi {\eltx_0}} \hom {\eltx_0\functionf} \setY {\eltx_0\functionf} \power \functionA_{\eltx_0} \xrightarrow{\textstyle 1_{\eltx_0\functionf} \power \functionA_{\eltx_0}} I \power \functionA_{\eltx_0} \buildrel {\text{(1.26)}} \over \cong \functionA_{\eltx_0} \\ \end{array}$$ Here are those versions (for a general $\calV$) again, followed by their translations for $\calV=\bftwo$ and $\calV=\Set$: $$\begin{array}{} (\functionA\eta)_{\eltx_0} & : & \functionA_{\eltx_0} & \buildrel {\text{(1.4)}} \over \cong & I \copower \functionA_{\eltx_0} & \xrightarrow{\textstyle 1_{\eltx_0\functionf}\copower\functionA_{\eltx_0}} & \hom {\eltx_0\functionf} \setY {\eltx_0\functionf} \copower \functionA_{\eltx_0} & \xrightarrow{\textstyle \hom {\eltx_0\functionf\,} \iota {\,\eltx_0}} & \displaystyle\int^{\eltx\in\setX} \hom {\eltx\functionf} \setY {\eltx_0\functionf} \copower \functionA_\eltx & = & (\functionA\Lanl\functionf)_{\eltx_0\functionf} &&&& \calV \\ (\functionA\eta)_{\eltx_0} & : & \functionA_{\eltx_0} & \buildrel {\text{(1.4)}} \over \cong & \top \wedge \functionA_{\eltx_0} & \xrightarrow{\textstyle 1_{\eltx_0\functionf}\wedge\functionA_{\eltx_0}} & \hom {\eltx_0\functionf} \setY {\eltx_0\functionf} \wedge \functionA_{\eltx_0} & \xrightarrow{\textstyle \hom {\eltx_0\functionf\,} \iota {\,\eltx_0}} & (\exists\eltx\in\setX) \hom {\eltx\functionf} \setY {\eltx_0\functionf} \wedge \functionA_\eltx & = & (\functionA\Lanl\functionf)_{\eltx_0\functionf} & = & (\exists_\functionf\functionA)_{\eltx_0\functionf} && \bftwo \\ (\functionA\eta)_{\eltx_0} & : & \functionA_{\eltx_0} & \buildrel {\text{(1.4)}} \over \cong & 1 \times \functionA_{\eltx_0} & \xrightarrow{\textstyle 1_{\eltx_0\functionf}\times\functionA_{\eltx_0}} & \hom {\eltx_0\functionf} \setY {\eltx_0\functionf} \times \functionA_{\eltx_0} & \xrightarrow{\textstyle \hom {\eltx_0\functionf\,} \iota {\,\eltx_0}} & \displaystyle\sum_{\eltx\in\setX} \hom {\eltx\functionf} \setY {\eltx_0\functionf} \times \functionA_\eltx & = & (\functionA\Lanl\functionf)_{\eltx_0\functionf} & = & (\textstyle\sum_\functionf\functionA)_{\eltx_0\functionf} && \Set \\ \end{array}$$ $$\begin{array}{} (\functionA\epsilon)_{\eltx_0} & : & & & (\functionA\Ranl\functionf)_{\eltx_0\functionf} & = & \displaystyle\int_{\eltx\in\setX} \hom {\eltx_0\functionf} \setY {\eltx\functionf} \power \functionA_\eltx & \xrightarrow{\textstyle \hom {\eltx_0\functionf} \pi {\eltx_0}} & \hom {\eltx_0\functionf} \setY {\eltx_0\functionf} \power \functionA_{\eltx_0} & \xrightarrow{\textstyle 1_{\eltx_0\functionf} \power \functionA_{\eltx_0}} & I \power \functionA_{\eltx_0} & \buildrel {\text{(1.26)}} \over \cong & \functionA_{\eltx_0} && \calV \\ (\functionA\epsilon)_{\eltx_0} & : & (\forall_\functionf\functionA)_{\eltx_0\functionf} & = & (\functionA\Ranl\functionf)_{\eltx_0\functionf} & = & (\forall\eltx\in\setX) [ \hom {\eltx_0\functionf} \setY {\eltx\functionf} \Rightarrow \functionA_\eltx] & \xrightarrow{\textstyle \hom {\eltx_0\functionf} \pi {\eltx_0}} & [ \hom {\eltx_0\functionf} \setY {\eltx_0\functionf} \Rightarrow \functionA_{\eltx_0}] & \xrightarrow{\textstyle [ 1_{\eltx_0\functionf} \Rightarrow \functionA_{\eltx_0} ] } & [ \top \Rightarrow \functionA_{\eltx_0} ] & \buildrel {\text{(1.26)}} \over \cong & \functionA_{\eltx_0} && \bftwo \\ (\functionA\epsilon)_{\eltx_0} & : & (\prod_\functionf\functionA)_{\eltx_0\functionf} & = & (\functionA\Ranl\functionf)_{\eltx_0\functionf} & = & \displaystyle\prod_{\eltx\in\setX} [ \hom {\eltx_0\functionf} \setY {\eltx\functionf}, \functionA_\eltx ] & \xrightarrow{\textstyle \hom {\eltx_0\functionf} \pi {\eltx_0}} & [ \hom {\eltx_0\functionf} \setY {\eltx_0\functionf}, \functionA_{\eltx_0} ] & \xrightarrow{\textstyle [ 1_{\eltx_0\functionf}, \functionA_{\eltx_0} ] } & [ 1, \functionA_{\eltx_0} ] & \buildrel {\text{(1.26)}} \over \cong & \functionA_{\eltx_0} && \Set \\ \end{array}$$