有向コンテナと多項式コモナド - 檜山正幸のキマイラ飼育記 (はてなBlog)

コンテナ〈container〉は、アーボット／アルテンキルヒ／ガニ〈Michael Abbott, Thorsten Altenkirch, Neil Ghani〉等によって導入された、型理論と圏論に関わる概念です（「圏論的コンテナ」参照）。有向コンテナ〈directed container〉は、コンテナにモノイド類似構造を追加した代数系で、アーマン／チャップマン／ウウスタル〈Danel Ahman, James Chapman, Tarmo Uustalu〉が提案したものです。

アーマン／チャップマン／ウウスタルによる有向コンテナの説明はAgda構文で記述されているので、初見では困惑します。普通の構文で書いてあれば、ずっとアクセスしやすかったろうに、と残念な気がします。この記事では、有向コンテナを普通の構文で定義します（Agda構文には触れません）。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\hyp}{\text{－} }
\newcommand{\id}{\mathrm{id}}
\newcommand{\In}{\text{ in } }
\newcommand{\Dwn}{\downarrow }
\newcommand{\Comp}{\mathop{;} }
\newcommand{\o}[1]{\overline{#1}}
\newcommand{\twoto}{\Rightarrow }
`$

内容：

有向コンテナ
圏から見る有向コンテナ
有向コンテナの法則
有向コンテナの再定義
パスとカローラ
付値カローラ
多項式関手
(n)-多項式関手
多項式コモナドに向けて

有向コンテナ

有向コンテナのホームページがあります。

https://cs.ioc.ee/~danel/dcont.html

有向コンテナに関する論文はこのWebページからたどれます。ひとつだけ論文を挙げると*1：

[AU16-]
Title: Directed Containers as Categories
Authors: Danel Ahman, Tarmo Uustalu
Submitted: 5 Apr 2016
Pages: 10p
URL: https://arxiv.org/abs/1604.01187

冒頭に述べたように、独特な記法（Agda構文）で書かれているので難読です。独特な記法を解説しようかとも思いましたが、実りがない作業なのでやめます。[AU16-] で使われている記号と、この記事で（一時的に）使う記号の対応だけ示しておきます。

$`\text{[AU16-]}`$	$`\text{この記事}`$
$`s, p, p'`$	$`a, f, g`$
$`s\Dwn p`$	$`\Dwn_a f`$
$`\mrm{o}\{s\}`$	$`\mrm{i}_a`$
$`p \oplus\{s\}\, p'`$	$`f \Comp_a g`$

圏から見る有向コンテナ

有向コンテナ〈directed container〉は、結論を先取りしてしまえば、小さな圏〈small category〉の別な表現です。有向コンテナの構成素は次です。

対象達の集合（小さい集合）： $`X \in |{\bf Set}|`$
$`X`$ の要素〈対象〉は $`a, b, x`$ などで表す。
対象でインデックス付けられた集合族〈ファミリー〉： $`A : X \to |{\bf Set}| \In {\bf SET}`$
諸般の事情により、$`A(a)`$ ではなくて $`A[a]`$ と書く。$`A[a]`$ の要素は $`a`$ から“出る射〈emanating morphism | morphism emanating {from | out of}〉”。
射の余域を与える単項演算子（の族）： $`\Dwn_a \hyp : A[a] \to X \In {\bf Set}`$
恒等射を与える定数（の族）： $`\mrm{i}_a \in A[a]`$
射の結合を与える依存二項演算子（の族）： $`(\hyp_1 \Comp_a \hyp_2): A[a] \times A[\Dwn_a \hyp_1] \to A[a] \In {\bf Set}`$ すぐ下に説明あり。

法則は後で述べるとして、幾つか補足をしておきます。

$`A`$ は集合族〈ファミリー〉なので、シグマ型やパイ型を作ることができます（「依存型と総称型の圏論的解釈」参照）。シグマ型は次のように略記します（この略記は [AU16-] でも使われています）。

$`\quad \o{A} := \sum_{x\in X} A[x]`$

シグマ型の標準射影を $`\mrm{dom}`$ と書きます（実際、圏の域そのものです）。

$`\quad \mrm{dom} : \o{A} = \sum_{x\in X} A[x] \to X`$

$`\o{A}`$ の要素は依存ペアなので、次の形に書きます。

$`\quad (a, f) \;\text{ where } a\in X,\,f \in A[a]`$

この形で書くと、$`\mrm{dom}`$ は次のように書けます。

$`\quad \o{A} \ni (a, f) \overset{\mrm{dom}}{\mapsto} a \in X`$

$`(\Dwn)`$ と $`\mrm{i}`$ のプロファイル（仕様）はパイ型を使って次のように書けます。

$`\quad (\Dwn) \in \prod_{x\in X} \mrm{Map}(A[x], X)\\
\quad \mrm{i} \in \prod_{x\in X} A[x]
`$

次の同型があります。

$`\quad \prod_{x\in X} \mrm{Map}(A[x], X) = \prod_{x\in X} X^{A[x]}\\
\quad \cong X^{(\sum_{x\in X} A[x])} = X^{\o{A}} = \mrm{Map}(\o{A}, X)
`$

この同型を使って $`(\Dwn)`$ を $`\mrm{Map}(\o{A}, X)`$ に移す〈写す〉と $`\mrm{cod}`$ が得られます。

$`\quad \mrm{cod} \in \mrm{Map}(\o{A}, X)\\
\text{i.e.}\\
\quad \mrm{cod} : \o{A} = \sum_{x\in X} A[x] \to X`$

$`(\Comp)`$ がややこしいですね。$`a\in X`$ ごとに二項演算子 $`(\Comp_a)`$ が決まるのですが、第一引数を決めないと第ニ引数の型〈値の集合〉が決まりません。第一引数の値に依存して第二引数の型が決まるというたぐいの依存二項演算子です。

$`(\Comp)`$ のプロファイルは次のようになります。

$`\quad (\Comp) \in \prod_{x\in X} \prod_{u\in A[x]} \mrm{Map}(A[\Dwn_x u], A[x])`$

$`(\Comp)`$ がどのように計算されるか順番に見ていきましょう。$`a \in X`$ を決めると、次の値が決まります。

$`\quad (\Comp_a) \in \prod_{u\in A[a]} \mrm{Map}(A[\Dwn_a u], A[a])`$

$`f \in A[a]`$ を決めると、次の値が決まります。

$`\quad (\Comp_a)(f) \in \mrm{Map}(A[\Dwn_a f], A[a])`$

$`g \in A[\Dwn_a f]`$ を決めると、次の値が決まります。

$`\quad (\Comp_a)(f)(g) \in A[a]`$

$`(\Comp_a)(f)(g)`$ を $`f \Comp_a g`$ と書くので、

$`\quad f \Comp_a g \in A[a]`$

$`f`$ を選べば $`\mrm{dom}`$ を使って $`a`$ が決まるので、$`A[\Dwn_a f] = A[\mrm{cod}(f)]`$ から $`g`$ を選べば、 $`f, g`$ に対して演算 $`(\Comp_a)`$ を適用できます。

ここまでの話で、有向コンテナ $`(X, A, \Dwn, \mrm{i}, \Comp)`$ は、圏の定義を別な形にしたものだと見当がつくでしょう。

両端（域と余域）を指定したホムセットの代わりに、域だけ指定した片方向ホムセット $`A[\hyp]`$ を使う。
すべての射達の集合は、ファミリー $`A`$ のシグマ型を使って定義できる。シグマ型の標準射影が域（$`\mrm{dom}`$）となる。
余域（$`\mrm{cod}`$）は単項演算子の族 $`(\Dwn_a)_{a\in X}`$ から構成できる。
依存二項演算子の族 $`(\Comp_a)_{a\in X}`$ が圏の結合〈composition〉を与える。
対象の集合 $`X`$ と、恒等射の族 $`(\mrm{i}_a)_{a\in X}`$ はそのまま使う。

有向コンテナの法則

有向コンテナ $`(X, A, \Dwn, \mrm{i}, \Comp)`$ が満たすべき法則〈公理〉は次のものです。

$`\forall a \in X.\, \Dwn_a \mrm{i}_a = a`$
$`\forall a \in X. \forall f \in A[a]. \forall g \in A[\Dwn_a f].\\ \quad \Dwn_a (f \Comp_a g) = \,\Dwn_{\Dwn_a f} g`$
$`\forall a \in X. \forall f \in A[a].\, f \Comp_a \mrm{i}_{\Dwn_a f} = f`$
$`\forall a \in X. \forall f \in A[a].\, \mrm{i}_a \Comp_a f = f`$
$`\forall a \in X. \forall f \in A[a]. \forall g \in A[\Dwn_a f].\forall h \in A[\Dwn_{\Dwn_a f} g].\\ \quad (f \Comp_a g) \Comp_a h = f \Comp_a (g \Comp_{\Dwn_a f} h)`$

通常の圏 $`\cat{C}`$ における、対応する法則は次のようになります。

$`\forall a \in |\cat{C}|.\, \mrm{cod}(\id_a) = a`$
$`\forall a \in |\cat{C}|. \forall f \in \cat{C}(a, \hyp). \forall g \in \cat{C}(\mrm{cod}(f), \hyp).\\ \quad \mrm{cod}(f ; g) = \mrm{cod}(g)`$
$`\forall a \in |\cat{C}|. \forall f \in \cat{C}(a, \hyp).\, f ; \id_{\mrm{cod}(f)} = f`$
$`\forall a \in |\cat{C}|. \forall f \in \cat{C}(a, \hyp).\, \id_a ; f = f`$
$`\forall a \in |\cat{C}|. \forall f \in \cat{C}(a, \hyp). \forall g \in \cat{C}(\mrm{cod}(f), \hyp).\forall h \in \cat{C}(\mrm{cod}(g), \hyp).\\ \quad (f ; g) ; h = f ; (g ; h)`$

通常の圏 $`\cat{C}`$ における以下の法則は、$`\mrm{dom}`$ の作り方から出ます。

$`\forall a \in |\cat{C}|.\, \mrm{dom}(\id_a) = a`$
$`\forall a \in |\cat{C}|. \forall f \in \cat{C}(a, \hyp). \forall g \in \cat{C}(\mrm{cod}(f), \hyp).\\ \quad \mrm{dom}(f ; g) = \mrm{dom}(f)`$

圏を定義するのに、なんでわざわざ奇妙な形式をつかうのか？ いくつかの理由がありますが、有向コンテナは、台（下部構造）がコンテナであることが大きな理由です。コンテナは集合圏上の多項式自己関手に対応します。よって、コンテナに構造を載せたものは、多項式自己関手に構造を載せたものに対応すると期待できます。

実際、有向コンテナは、集合圏上の多項式コモナドに対応します。コンテナ $`(X, A)`$ に対応する多項式関手上に、$`(\Dwn, \mrm{i}, \Comp)`$ を使ってコモナド構造（コモナド余乗法とコモナド余単位）を構成できます。多項式コモナドのあいだのコモナド準同型射は、有向コンテナのあいだの準同型射と一対一に対応します。また、有向コンテナのあいだの準同型射は、圏のあいだの関手とは違うものになります。

このような観点や事実は、通常の圏の定義からはなかなか出てこないでしょう。

有向コンテナの再定義

コンテナの典型的〈プロトタイプ的〉なイメージは、ツリー（形状）の集合があり、各ツリーごとにノードの集合が決まっている、といったものです。ノードは値を入れる場所・位置として機能します。一方で圏は、対象と対象のあいだに射と呼ばれる矢印がある、といったイメージでしょう。ニ種類のイメージはかなりかけ離れています。

ここでは、二種類のイメージの中間的なメンタルモデルに基づいた用語と記法を決めます。

圏	有向コンテナ	折衷案
対象	形状〈シェイプ〉	ポイント〈point〉
射	位置〈ポジション〉	アロー〈arrow〉
射の域	位置の親の形状	アローのソース〈source〉
射の余域	位置の部分形状の大域形状	アローのターゲット〈target〉
恒等射	ルート位置	ポイントアロー〈point arrow〉
射の結合	位置の演算（記号は $`\oplus`$）	アローの結合〈composition〉

有向コンテナに関するオリジナルの（例えば [AU16-]の）用語法は、上記のごとくでだいぶ使い勝手が悪いので使いません。折衷案の記法は次のように決めます。

圏＝有向コンテナ： $`\cat{D}`$
対象の集合＝ポイントの集合： $`X = \mrm{Pt}(\cat{D}) = |\cat{D}|`$
射の集合＝アローの集合： $`\o{A} = \mrm{Arr}(\cat{D}) = \sum_{x\in X} A[x]`$
片方向ホムセット＝ カローラ〈corolla〉（後述）： $`A[a] = \cat{D}_1[a]`$
域＝ソース： $`\mrm{src}: \o{A} = \mrm{Arr}(\cat{D}) \to X = |\cat{D}| \In {\bf Set}`$
余域＝ターゲット： $`\mrm{trg}: \o{A} = \mrm{Arr}(\cat{D}) \to X = |\cat{D}| \In {\bf Set}`$
対象指定の余域＝ポイント指定のターゲット： $`\mrm{trg}_a: A[a] = \cat{D}_1[a] \to X = |\cat{D}| \In {\bf Set}`$
恒等＝ポイントアロー： $`\mrm{i} \in \prod_{x \in X} A[x]`$
対象ごとの恒等＝ポイントごとのポイントアロー： $`\mrm{i}_a \in A[a]`$
結合： $`\mrm{comp} = (;) \;\in \prod_{x\in X} \prod_{f\in A[x]} \mrm{Map}(A[\mrm{trg}_x(f)], A[x] )`$
対象ごとの結合＝ポイントごとの結合： $`\mrm{comp}_a = (;_a) \;\in \prod_{f\in A[a]} \mrm{Map}(A[\mrm{trg}_a(f)], A[a] )`$

アローは、そのソースポイントも明示して $`(a, f)`$ のように書くことにします。これは、依存ペアの書き方です。アローのプロファイル（ソースとターゲットの仕様）は、圏と同じように書きます。

$`\quad (a, f): a \to \mrm{trg}_a(f) \In \cat{D}`$

有向コンテナの用語・記法を以上のように決めれば、圏に関する言葉をわずかに変えたものだと思えます。圏の言葉と有向コンテナの言葉が混ざってしまっても特に違和感はないでしょう。例えば、「恒等アロー」、「射のターゲット」「ポイントから出る射」と言っても何の問題もありません。

アーマン／チャップマン／ウウスタルの用語・記法は、圏論の用語・記法と混ぜて使うことがまったく出来ないことがおおきな問題です。概念的に同じことを周知の用語・記法に翻訳する負担がバカになりません。

パスとカローラ

$`\cat{D}`$ を有向コンテナ〈圏〉だとして、結合可能〈composable〉なn本のアロー〈射〉の列を、長さnのパス〈path of length n〉、あるいはより短くn-パス〈n-path〉と呼びます。0-パスは単一のポイント〈対象〉のことだとします。

0-パスの例： $`a`$
1-パスの例： $`(a, f)`$
2-パスの例： $`(a, f, g) = ( (a, f), (\mrm{trg}_a(f), g) )`$
3-パスの例： $`(a, f, g, h) = ( (a, f), (\mrm{trg}_a(f), g), (\mrm{trg}_{\mrm{trg}_a(f)}(g), h) )`$

有向コンテナ $`\cat{D}`$ のポイント $`a`$ から出るn-パスの集合を次のように書きます。

$`\quad \cat{D}_n[a]\;\in |{\bf Set}|`$

$`n = 0, 1, 2`$ なら次のようになります。$`X, A`$ は前節と同じ意味です。

$`\cat{D}_0[a] = \{a\} \subseteq X = \mrm{Pt}(\cat{D})`$
$`\cat{D}_1[a] = A[a] \subseteq \mrm{Arr}(\cat{D})`$
$`\cat{D}_2[a] = \{ ( (a, f), (b, g) )\in \mrm{Arr}(\cat{D})^2 \mid \mrm{trg}_a(f) = b \}`$

有向コンテナ $`\cat{D}`$ のn-パスの集合を次のように書きます。

$`\quad \mrm{Path}_n(\cat{D})\;\in |{\bf Set}|`$

$`n = 0, 1`$ なら次のようになります。

$`\mrm{Path}_0(\cat{D}) = X = \mrm{Pt}(\cat{D}) = |\cat{D}|\;\in |{\bf Set}|`$
$`\mrm{Path}_1(\cat{D}) = \o{A} = \mrm{Arr}(\cat{D}) = \sum_{x\in X}A[x]\;\in |{\bf Set}|`$

集合 $`\cat{D}_n[a]`$ を一本のツリーと考えることがあります。集合の要素であるパスは、ツリーのリーフと一対一対応します。パスの長さは、リーフまでの分岐の回数＋１なので、ツリーの高さとみなせます。

ポイント $`a`$ からすべての方向に広がるイメージから、集合 $`\cat{D}_n[a]`$ をカローラ〈corolla〉と呼ぶこともあります*2。「カローラ」とは、花輪／花冠、あるいは植物の花びらの意味です。

$`n= 4`$ の“イメージ”は、例えば次のようでしょうか。

集合 $`\cat{D}_n[a]`$ をカローラと呼んだ場合は、$`a`$ は（ルートではなくて）中心〈center〉、$`n`$ は（高さではなくて）半径〈radius〉とします。中心 $`a`$ 半径 $`0`$ のカローラは一点だけの集合 $`\{a\}`$ です。

付値カローラ

$`\cat{D}`$ は有向コンテナとします。$`S`$ を何でもいいから集合とします。

ポイント $`a \in |\cat{D}|`$ と自然数 $`n\in {\bf N}`$ を決めると、$`\cat{D}`$ のカローラ $`\cat{D}_n[a]`$ がひとつ確定します。これは、中心 $`a`$ 、半径 $`n`$ のカローラです。カローラはひとつの集合です。その要素は、中心 $`a`$ から出る長さ $`n`$ のパスです。

ひとつのカローラ上で定義された $`S`$ に値を取る関数〈写像〉 $`v:\cat{D}_n[a] \to S`$ を、$`S`$-付値カローラ〈$`S`$-valued corolla | corolla with $`S`$-valuation〉と呼びます。関数の域も添えて $`v = (\cat{D}_n[a], v)`$ と書くことにします*5。

$`S`$-付値カローラを、$`S`$で色付けされたカローラ〈$`S`$-colored corolla〉とか$`S`$で修飾されたカローラ〈$`S`$-decorated corolla〉とか呼んでもかまいません。（下はカローラ〈花輪〉でデコレートされたカローラ〈トヨタ・カローラ〉）

呼び名は別に何だっていいんです。「Diag構成：圏論的構成法の包括的フレームワークとして」から引用すると：

ちなみに、「付値〈valuation〉／値〈value〉」という言葉を使いましたが、同義語はたくさんあり、概念的には同じでも状況により違う言葉を使います。

ラベリング／ラベル

色付け／色（色＝一般的な値）

修飾

重み付け／重さ（主に実数値）

ランク付け／ランク（主に整数値）

階付け／階数（主に整数値）

値がモノの種類のときは：

型付け／型〈タイプ〉

ソート付け／ソート

色付け／色（色＝種類）

値が二値のときは：

極性付け〈偏極〉／極性

符号付け／符号

パリティ付け／パリティ

荷電

有向コンテナの$`S`$-付値カローラ $`(\cat{D}_n[a], v)`$ は、形状であるカローラ（パスの集合）に関数 $`v`$ で$`S`$-値割り当て〈$`S`$-色付け | $`S`$-修飾〉したものです。同一形状 $`\cat{D}_n[a]`$ に対するすべての値割り当ての集合は、次の関数集合になります。

$`\quad \mrm{Map}(\cat{D}_n[a], S)\;\in |{\bf Set}|`$

ここで、$`a\in X,\,n\in {\bf N}`$ を動かして寄せ集めれば、考え得るすべての$`S`$-付値カローラ（形状と値割り当て）達の集合が得られます。

$`\quad \sum_{n\in {\bf N}}\sum_{a\in X} \mrm{Map}(\cat{D}_n[a], S)\;\in |{\bf Set}|`$

特に重要なのは、$`n = 1`$ の場合です。

$`\quad \sum_{a\in X} \mrm{Map}(\cat{D}_1[a], S)\;\in |{\bf Set}|`$

これは、$`\cat{D}`$ における半径 $`1`$ （ツリーとみれば高さ $`1`$）のすべての$`S`$-付値カローラを集めた集合です。

多項式関手

前節の“半径 $`1`$ のすべての$`S`$-付値カローラ”は、値の集合 $`S`$ を決めれば確定します。もちろん、有向コンテナ $`\cat{D}`$ あっての話です。$`\cat{D}`$ と $`S`$ から決まる集合を次のように書きます。

$`\quad \widehat{\cat{D}}(S) \;\in |{\bf Set}|`$

集合 $`S\in |{\bf Set}|`$ は何でもよかったので、$`\widehat{\cat{D}}`$ は次のような写像となります。

$`\quad |{\bf Set}|\ni S \mapsto \widehat{\cat{D}}(S) \in |{\bf Set}|`$

$`\widehat{\cat{D}}(S)`$ の具体的な定義を再掲すれば：

$`\quad \widehat{\cat{D}}(S) = \sum_{x \in X}\mrm{Map}(\cat{D}_1[x], S)\;\in |{\bf Set}|`$

関数集合をベキ〈累乗〉形式で書くと：

$`\quad \widehat{\cat{D}}(S) = \sum_{x \in X} S^{\cat{D}_1[x]}\;\in |{\bf Set}|`$

あるいは、$`A[\hyp] = \cat{D}_1[\hyp]`$ という記法ならば：

$`\quad \widehat{\cat{D}}(S) = \sum_{x \in X} S^{A[x]} \;\in |{\bf Set}|`$

つまり、任意の集合 $`S`$ に、“半径 $`1`$ のすべての$`S`$-付値カローラ”の集合を対応させる写像 $`\widehat{D}`$ は、多項式形式で書けるわけです。

集合〈集合圏の対象〉 $`S`$ が入る場所に、関数〈集合圏の射〉 $`f:S \to T`$ を入れることができます。

$`\quad \widehat{\cat{D}}(f) = \sum_{x \in X} f^{A[x]} \;: \widehat{\cat{D}}(S) \to \widehat{\cat{D}}(T) \In {\bf Set}`$

関数のベキ〈累乗〉はサンドイッチ結合で計算できます。それについては：

以上で $`\widehat{\cat{D}}(\hyp)`$ は、引数に集合だけでなくて関数も取れるようになりました。さらに、次を示すことができます。

$`\text{For } f:S \to T, g: T \to U \In {\bf Set}\\
\quad \widehat{\cat{D}}(f;g) = \widehat{\cat{D}}(f);\widehat{\cat{D}}(g)\\
\quad \widehat{\cat{D}}(\id_S) = \id_{\widehat{\cat{D}}(S)}
`$

集合圏上の多項式自己関手 $`\widehat{\cat{D}}`$ を定義するには、有向コンテナの構造は不要で、コンテナ部分 $`(\mrm{Pt}(\cat{D}), \cat{D}_1[\hyp]) = (X, A[\hyp])`$ だけで十分です。コンテナは集合圏上の多項式自己関手を定義します；そうして定義された関手を多項式自己関手〈polynomial endofunctor〉、あるいは単に多項式関手〈polynomial functor〉と呼びます。

(n)-多項式関手

コンテナがあれば、集合圏上の多項式関手が定義できます。有向コンテナからは、標準的な多項式関手 $`\widehat{\cat{D}}`$ 以上のナニカが定義できるはずです。そのひとつが、$`\widehat{\cat{D}}^{(n)}`$ という関手です。

$`\quad \widehat{\cat{D}}^{(n)}(y) = \sum_{x \in X} y^{\cat{D}_n[x]}`$

ここで、小文字の $`y`$ は米田不定元で、集合〈対象〉も関数〈射〉も代入できる形式的変数です（「スピヴァックの指数記法（米田不定元）」参照）。$`y`$ を含んだ多項式形式は関手を定義します。

$`\widehat{\cat{D}}^{(n)}`$ は $`n`$ ごとに定義されます； $`\widehat{\cat{D}}^{(0)}`$、$`\widehat{\cat{D}}^{(1)}`$、$`\widehat{\cat{D}}^{(2)}`$ などです。実際に重要なのはこの3つです。

$`\quad \widehat{\cat{D}}^{(0)}(y) = \sum_{x \in X} y^{\cat{D}_0[x]}\\
\quad = \sum_{x \in X} y^{ \{x\} } \cong \sum_{x \in X} y \cong X\times y\\
\quad \widehat{\cat{D}}^{(1)}(y) = \sum_{x \in X} y^{\cat{D}_1[x]}\\
\quad = \widehat{\cat{D}}(y)\\
\quad \widehat{\cat{D}}^{(2)}(y) = \sum_{x \in X} y^{\cat{D}_2[x]}
`$

$`\widehat{\cat{D}}^{(2)}(S)`$ は、半径 $`2`$ のすべての（すべてのポイントの）$`S`$-付値カローラからなる集合になります。$`\widehat{\cat{D}}^{(2)}`$ は関手を結合した $`\widehat{\cat{D}}^2`$ とは（関係はあるが）別物なので注意してください。$`\widehat{\cat{D}}^{(0)}`$ と $`\widehat{\cat{D}}^{0} = \mrm{Id}_{\bf Set}`$ も違う関手です。

$`\widehat{\cat{D}}^{(2)}`$ と $`\widehat{\cat{D}}^{2}`$ のあいだの関係とは、次のような自然変換があることです。

$`\quad \iota :: \widehat{\cat{D}}^{(2)} \twoto \widehat{\cat{D}}^{2}
: {\bf Set} \to {\bf Set}\In {\bf CAT}
`$

自然変換 $`\iota`$ は成分ごとに包含写像になります（詳細は省略）。

多項式コモナドに向けて

集合圏上の多項式コモナド〈polynomial comonad〉とは、多項式自己関手 $`P : {\bf Set}\to{\bf Set}`$ と、以下のような2つの自然変換 $`\delta, \varepsilon`$ （コモナド余乗法とコモナド余単位）の組 $`(P, \delta, \varepsilon)`$ で、コモナド法則を満たすものです。

$`\quad \delta :: P \twoto P^2 = P*P : {\bf Set} \to {\bf Set} \In {\bf CAT}\\
\quad \varepsilon :: P \twoto P^0 = \mrm{Id}_{\bf Set} : {\bf Set} \to {\bf Set} \In {\bf CAT}
`$

コモナド法則はモナド法則に双対的なもので、自己関手の結合積〈composition product〉に関するコモノイド構造（「図式思考の例として、コモノイドについて考えてみる」参照）を定義する法則〈公理〉です。

有向コンテナから定義された多項式関手には、有向コンテナの圏構造 $`(\mrm{trg}, \mrm{i}, \mrm{;})`$ から誘導されるコモナド構造が載ることが知られています。これは、アーマン／ウウスタルの発見で、圏に対する新しい見方を提供しました。

有向コンテナ $`\cat{D}`$ からの多項式コモナド構造を完全に記述するのは手間がかかるので、ここでは、自然変換 $`\delta, \varepsilon`$ の具体的な定義だけを紹介します。

コモナド余単位 $`\varepsilon`$ は簡単です。自然変換の$`S`$-成分は次のようです。

$`\quad \varepsilon_S : \widehat{D}(S) \to \mrm{Id}_{\bf Set}(S) \In {\bf Set}`$

より具体的に書けば：

$`\quad \varepsilon_S : \sum_{x \in X} S^{\cat{D}_1[x]} \to S \In {\bf Set}`$

パイ型 $`\sum_{x \in X} S^{\cat{D}_1[x]}`$ の要素は依存ペアの形で次のように書けます。

$`\quad (a, v) \text{ where }a\in X,\, v \in S^{\cat{D}_1[a]}`$

この要素に対する値を決めればいいわけです。次のように決めます。

$`\text{For } (a, v) \in \sum_{x \in X} S^{\cat{D}_1[x]}\\
\quad \varepsilon_S( (a, v) ) := v(\mrm{i}_a) \;\in S
`$

ここで、$`\mrm{i}_a`$ は、有向コンテナ〈圏〉のポイントアロー〈恒等射〉です。カローラへの値割り当てである $`v`$ に、ポイントアローでの値を対応させています。

次に、コモナド余乗法 $`\delta`$ の$`S`$-成分を次の形で定義します。

$`\quad \delta_S : \widehat{D}(S) \to \widehat{D}^{(2)}(S) \In {\bf Set}`$

本来、写像の行き先は $`\widehat{D}^{2}(S) = \widehat{D}(\widehat{D}(S))`$ ですが、前節で注意した包含関係があるので大丈夫です。

$`\quad \widehat{D}^{(2)}(S) \subseteq \widehat{D}^{2}(S) \In {\bf Set}`$

$`\delta_S`$ をより具体的に書けば：

$`\quad \delta_S : \sum_{x \in X} S^{\cat{D}_1[x]} \to \sum_{x \in X} S^{\cat{D}_2[x]} \In {\bf Set}`$

$`\sum_{x \in X} S^{\cat{D}_1[x]}`$ の要素が依存ペアで書けるのは同じです。依存ペアに対する値を次のように決めます。

$`\text{For } (a, v) \in \sum_{x \in X} S^{\cat{D}_1[x]}\\
\quad \delta_S( (a, v) ) := (a, \lambda\, (a, f, g) \in \cat{D}_2.(\, v(f;g) \;\in S\,) )
\in \sum_{x \in X} S^{\cat{D}_2[x]}
`$

$`\delta_S`$ の値もまた依存ペアです。依存ペアの第二成分は半径 2 のカローラへの値割り当て関数なので、ラムダ記法で関数を書いています。長さ 2 のパス $`(a, f, g)`$ に対する$`S`$-値割り当てを $`v(f;g)`$ と定義しています。有向コンテナ〈圏〉の結合 $`(;)`$ を利用しています。

以上の定義だけからも次のことは読み取れるでしょう。