またダジャレです。
「それでもカン拡張の左右を忘れてしまう」において、左右を憶えるために次のような随伴トリプルを出しました。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\hyp}{\text{－} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\In}{\text{ in } }
\newcommand{\Imp}{ \Rightarrow }
`$
$`\quad \mrm{Lan}_K \dashv \mrm{Can}_K \dashv \mrm{Ran}_K`$
$`\mrm{Can}_K`$ は、$`K`$ を関手プレ結合することによる引き戻しです。記法の簡略化のために、「それでもカン拡張の左右を忘れてしまう」で出した $`?(\hyp , \hyp)`$ を使うことにすると、随伴トリプルのホムセット同型は次のように書けます。
$`\quad ?(K* X , F) \cong \,?(X, \mrm{Ran}_K F)\\
\quad ?(F , K* Y) \cong \,?(\mrm{Lan}_K F, Y)
`$
「カン拡張における上下左右： 入門の前に整理すべきこと」で出した $`{^K F}, {^\cap \alpha}, {_K F}, {_\cup \beta}`$ も使うと：
$`\quad ?(K* X , F) \ni \alpha \longleftrightarrow {^\cap \alpha} \in \,?(X, {^K F})\\
\quad ?(F , K* Y) \ni \beta \longleftrightarrow {_\cup \beta} \in \,?( {_K F}, Y)
`$
上の右カン拡張における同型を図示した「それでもカン拡張の左右を忘れてしまう」の絵を再掲すると：
ラムダ抽象に相当する $`{^\cap \alpha}`$ から $`\alpha`$ を再現するときは、ラムダ計算における評価射〈eval〉と類似の役割りを持った自然変換 $`K* {^K F} \twoto F`$ を使います。この eval 類似の自然変換には特に名前はないようです。eval はインタプリタの実行に相当します。実行、そう、run ですね。
run を使って $`\alpha`$ を再現する過程は次のように描けます。左の $`K`$ のワイヤーを引っ張り上げてワイヤーストレッチングすると、run は壊れて右の状態になります。
右カン拡張の eval 相当物が run ならば、左拡張における相当物は -- そりゃ lun ですよ。
