デカルト圏上のコンウェイ不動点オペレーターは、関数のパラメータ付き不動点の振る舞いを抽象化して圏論的に定式化したものです。2つの成分変数（インデックス）を持つオペレーターで、ひとつの成分変数に関しては自然性を持ち、もうひとつの成分変数に関しては対角自然性を持ちます。
圏論的に好都合なオペレーターなのですが、圏論的な扱いは割と複雑です。できるだけ簡単で憶えやすい計算公式の形も一緒に提示します。
記事内で使う文字の色については「文字の色の約束（再確認）」を参照してください。
[追記 date="翌々日"]$`\star^A`$ と書くべき所を $`\star^{\mathbf{1}}`$ と間違っていました。修正しました。修正箇所にも追記を入れてます。[/追記]$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\u}[1]{\underline{#1} }
\newcommand{\o}[1]{\overline{#1} }
\newcommand{\In}{\text{ in } }
\newcommand{\hyp}{\text{－} }
%\newcommand{\Imp}{\Rightarrow }
%\newcommand{\Iff}{\Leftrightarrow}
\newcommand{\T}[1]{ \text{#1} }
\newcommand{\op}{\mathrm{op} }
\newcommand{\id}{\mathrm{id} }
%\newcommand{\pto}{\nrightarrow} % proarrow to
%\newcommand{\dto}{\looparrowright} % dependent to
%\newcommand{\hto}{\rightsquigarrow} % hetero to
%\newcommand{\parto}{\supset\!\to}
\newcommand{\twoto}{\Rightarrow}
\newcommand{\conc}{\mathop{\#}} % concatnation
\newcommand{\C}{\mathop{;}} % Composition
`$
内容：
- デカルト圏とパラメータ付き射の圏
- 不動点オペレーター
- コンウェイ不動点オペレーター
- 自然性（パラメータ変換公式）
- 対角自然性（結合順入れ替え公式）
- 対角自然性（結合順入れ替え公式） 続き
- 対角性（ダブルスター公式）
- まとめ
デカルト圏とパラメータ付き射の圏
まず、後で必要となる概念と記法の準備をします。
$`\cat{C} = (\cat{C}, \times, \mbf{1})`$ をデカルト・モノイド圏〈Cartesian monoidal category〉とします。以下、デカルト・モノイド圏（モノイド圏として定義されたデカルト圏）を単にデカルト圏〈Cartesian category〉と呼びます。$`\cat{C}`$ の結合〈composition〉は、図式順中置演算子記号 $`;`$（セミコロン）を使って書きます。
対象 $`A\in |\cat{C}|`$ に対して、新しい圏 $`\cat{C}^A`$ を定義します。$`\cat{C}^A`$ という記法を使いますがベキ〈冪 | 指数〉とは何の関係もありません。
- $`|\cat{C}^A| := |\cat{C}|`$
- $`X, Y \in |\cat{C}^A|`$ に対して、ホムセットは $`\cat{C}^A(X, Y) := \cat{C}(A\times X, Y)`$
$`\cat{C}^A`$ における結合〈composition〉と恒等〈identity〉については、過去記事「環境付き計算と依存アクテゴリー 1/n」において、ストリング図で説明しています。過去記事では、$`\cat{C}^A`$ ではなくて $`\cat{C}_{(A \times)}`$ という記法を使っています（要注意）。
また、別な過去記事「不動点理論と対角自然性（dinaturality）」でも同様な話題を扱っています。こっちの過去記事では、記法 $`\cat{C}^A`$ を使っています（今回の記事と同じ記法）。インデックス付き圏〈indexed category〉であることを強調したいときは $`\cat{C}^A = \cat{C}[A]`$ とも書いています（今回も同じ記法を使います）。$`\cat{C}^A`$ における結合は $`\conc`$ を使っていました（今回は使いません）。
今回は、$`\cat{C}^A`$ における結合は $`\star^A`$ 、恒等は $`\id^A`$ とします。しかし、ほとんどの場合、上付きの $`A`$ を省略して単に $`\star, \id`$ とします。
$`f:A\times X \to Y \In \cat{C}`$ は、$`\cat{C}^A`$ の射とみなせば、$`f:X \to Y \In \cat{C}^A`$ です。同じ射でも、どの圏の射とみなすかによりプロファイル（域と余域）が変わります。この点（実体が同じでも区別すること）については過去記事「エラーを起こす不純な関数を純化してあげる // 静かなるドン」で説明しています。
$`\cat{C}^A`$ の射を$`A`$-パラメータ付き射〈$`A`$-parameterized morphism〉と呼びます。したがって、$`\cat{C}^A`$ は$`A`$-パラメータ付き射の圏〈category of $`A`$-parameterized morphisms〉です。$`\cat{C}`$ の対象 $`A`$ はパラメータ対象〈parameter object〉またはパラメータ空間〈parameter space〉と呼ぶことにします。それ自体がパラメータ対象という種類の対象があるわけではなくて、ある状況において対象が果たす役割りの名前が「パラメータ対象〈パラメータ空間〉」です。「環境付き計算と依存アクテゴリー 1/n」では、パラメータ対象を環境〈environment〉と呼んでいました。
$`f:A \times T\times X \to Y \In \cat{C}`$ を
$`\quad f:T\times X \to Y \In \cat{C}^A`$
とみなせば、$`f`$ のパラメータ対象は $`A`$ です。しかし、
$`\quad f:X \to Y \In \cat{C}^{A\times T}`$
とみなせば、$`f`$ のパラメータ対象は $`A\times T`$ です。また、
$`\quad f: \mbf{1} \to Y \In \cat{C}^{A\times T\times X}`$
とみなすこともできます。この場合、$`f`$ のパラメータ対象は $`A\times T\times X`$ です。
$`u:A \to B\In \cat{C}`$ があると、$`\cat{C}[u] : \cat{C}[B] \to \cat{C}[A]`$ という再インデキシング関手〈reindexing functor〉が定義できます。これは、$`g:B\times X\to Y\In \cat{C}`$ の第一引数側に $`u`$ を結合することなので、次のように書きます。
$`\quad u\C_1 g := (u \times \id_X)\C g`$
$`\quad \cat{C}[u](g) := u\C_1 g`$
$`w: T \to X\In \cat{C}`$ があるとき、$`f:A\times X\to Y\In \cat{C}`$ の第二引数側に $`w`$ を結合することは：
$`\quad w\C_2 f := (\id_A \times w)\C f`$
$`\C_1`$ と $`\C_2`$ は二変数関数の片一方の変数への結合を表す記号です*1。
書き方が $`\cat{C}_{A\times}`$ でも $`\cat{C}^A`$ でもその他でも何でもいいですが、大事なことは $`\cat{C}[A] := \cat{C}_{(A\times)} = \cat{C}^A`$ と置いたとき、$`\cat{C}[\hyp]`$ がインデックス付き圏になることです。例えば、射影 $`\pi^{A, B}_2: A\times B \to B`$ からは
$`\quad \cat{C}[\pi^{A, B}_2] : \cat{C}[B] \to \cat{C}[A\times B] \In \mbf{CAT}`$
が誘導されます。$`\cat{C}[\hyp]`$ は次の性質を持ちます。
- 任意の $`A\in |\cat{C}|`$ に関して、$`|\cat{C}[A]| = |\cat{C}|`$
- 任意の $`u: A \to B \In \cat{C}`$ に対して $`\cat{C}[u]`$ はid.o.関手〈identity-on-objects functor〉（「充満忠実関手の疑似的逆関手 // 関手の性質」参照）
- $`\cat{C}[\mbf{1}] \cong \cat{C}`$ （圏同型）
$`\cat{C}[\hyp] = \cat{C}^\hyp`$ なので、$`u: A \to B \In \cat{C}`$ に対して、$`\cat{C}^u`$ も意味を持ちます。これは再インデキシング関手です。
$`\quad \cat{C}^u : \cat{C}^B \to \cat{C}^A \In \mbf{CAT}`$
$`X, Y\in |\cat{C}|`$ に対して、$`\cat{C}^u(X, Y)`$ は、再インデキシング関手のホムパート〈hom part〉です。
$`\quad \cat{C}^u(X, Y) : \cat{C}^B(X, Y) \to \cat{C}^A(X, Y) \In \mbf{Set}`$
$`\T{For }g : X \to Y \In \cat{C}^B\\
\T{i.e. }g : B\times X \to Y \In \cat{C}\\
\quad \cat{C}^u(X, Y)(g) := u \C_1 g := (u\times \id_X)\C g
`$
不動点オペレーター
集合圏で考えましょう。$`f: X \to X \In \mbf{Set}`$ の不動点〈fixed point〉とは、
$`\quad f(s) = s`$
を満たす $`s\in X`$ です。自己写像 $`f`$ によって動かされない点が不動点です。
単一の写像〈関数〉ではなくて、$`a\in A`$ でパラメータ付けられた自己写像の族 $`(f_a : X \to X)_{a\in A}`$ があったとします。どの自己写像 $`f_a : X \to X`$ にも不動点があるとします。各 $`a\in A`$ ごとに不動点を選んでそれを $`s(a) \in X`$ とすると、$`s(a)`$ は次を満たします。
$`\quad \forall a \in A. f_a(s(a)) = s(a)`$
写像の族〈高階関数〉$`a\mapsto f_a`$ を反カリー化〈uncurrying〉して、それを同じ記号 $`f`$ で表せば、次のように書いても同じことです。
$`\quad \forall a \in A. f(a, s(a)) = s(a)`$
これを次のように書けば、集合圏以外でも使えます。
$`\quad \langle \id_A, s\rangle \C f = s \; : A \to X`$
ここで、$`\langle \hyp, \hyp\rangle`$ はデカルト・ペアリング〈Cartesian pairing〉です*2。
不動点の族 $`s`$ が満たすべき条件を、集合圏とは限らないデカルト圏内の可換図式で書けば次のようになります。
$`\quad \xymatrix{
A \ar[d]_{\langle \id_A, s\rangle} \ar[dr]^s
\\
{A\times X} \ar[r]_f
& X
}\\
\quad \T{commutative}\In \cat{C}
`$
$`s`$ を（$`f`$ に対する）パラメータ付き不動点〈parameterized fixed points〉と呼びます。パラメータがないケースは、$`A = \mbf{1}`$ と考えます。
$`\quad \xymatrix{
\mbf{1} \ar[d]_{\langle \id_{\mbf{1}}, s\rangle} \ar[dr]^s
\\
{\mbf{1}\times X} \ar[r]_f
& X
}\\
\quad \T{commutative}\In \cat{C}
`$
$`\mbf{1}\times X \cong X`$ を使って簡略化すれば：
$`\quad \xymatrix{
\mbf{1} \ar[d]_s \ar[dr]^s
\\
X \ar[r]_f
& X
}\\
\quad \T{commutative}\In \cat{C}
`$
この可換図式を集合圏で考えたものが、最初に挙げた不動点方程式 $`f(s) = s`$ です。
ここから先この記事で扱う不動点／不動点オペレーターは、圏論的に抽象化・公理化したもので具体性は乏しいかも知れません。具体的な不動点／不動点オペレーターの話は、以下の過去記事達でしています。適宜参照してください。
- letrecと不動点方程式とトレース付き圏 (2012年)
- 不動点理論と対角自然性（dinaturality） (2013年)
- ωCPO（可算完備順序集合）で考える形式言語理論 (2013年)
- 単調作用素と閉包作用素のプレ不動点 (2021年)
- 不動点方程式／不動点不等式と不動点オペレーター (2022年)
- タルスキーの最小プレ不動点定理（訂正） (2022年)
- タルスキーの定理の実例と応用 (2022年)
- 再帰的関数定義と不動点 (2022年)
コンウェイ不動点オペレーター
不動点オペレーターの代数的公理化は、コンウェイ〈John Horton Conway〉により始まりました。そのときの不動点オペレーターは半環〈semiring〉上のオペレーターでした。その後、ブルーム／エーシク〈Stephen L. Bloom, Zoltán Ésik〉によりローヴェア・セオリー〈Lawvere theory〉（と呼ばれる特別なデカルト圏）上のオペレーターとして公理化され、さらにシンプソン／プロトキン*3〈Alex Simpson, Gordon Plotkin〉*4により任意のデカルト圏上のオペレーターにまで拡張されました*5。
デカルト圏上の不動点オペレーターは、次の形をしています。
$`\T{For }A, X \in |\cat{C}|\\
\quad \mrm{Fix}^A_X : \cat{C}(A\times X, X) \to \cat{C}(A, X) \In \mbf{Set}
`$
つまり、$`\cat{C}`$ の2つの対象でインデックス付けられたホムセット間の写像の族です。
$`\cat{C}(A, X) \cong \cat{C}(A \times \mbf{1}, X) = \cat{C}^A(\mbf{1}, X)`$ であるので、次のようにも書けます。
$`\T{For }A, X \in |\cat{C}|\\
\quad \mrm{Fix}^A_X : \cat{C}^A(X, X) \to \cat{C}^A(\mbf{1}, X) \In \mbf{Set}
`$
等式的公理によって特徴付けられた不動点オペレーターはコンウェイ不動点オペレーター〈Conway fixed-point operator〉と呼ばれます。コンウェイ不動点オペレーターの公理は次の4つです。
- パラメータ付き不動点性〈parameterized fixed-point property〉
- 自然性〈naturality〉
- 対角自然性〈dinaturality〉
- 対角性〈diagonal property〉
実は、パラメータ付き不動点性は対角自然性の特別な場合なので、なくてもかまいません。しかし、一番重要な性質であるパラメータ付き不動点性を落としてしまうのは（論理的には正当でも）気持ち悪いので冗長でも4つの公理にしておきます。
パラメータ付き不動点性は、前節で述べたパラメータ付き不動点が満たす性質である等式、または可換図式のことです。次のように書けます。
$`\T{For } f:A\times X \to X \In \cat{C}\\
\quad \langle \id_A, \mrm{Fix}^A_X(f)\rangle \C f = \mrm{Fix}^A_X(f) \;
: A \to X \In \cat{C}
`$
$`\mrm{Fix}^A_X(f)`$ という書き方はちょっと煩雑なので、通常はダガーを使って $`f^\dagger`$ と書かれます。しかし、ダガーを手書きするのが大変*6なので、この記事ではアスタリスクを使って $`f^*`$ とします。上付きアスタリスクは多用されるので、紛らわしいのがデメリットです。そのデメリットを幾分でも緩和するために $`[\cdots]^*`$ という書き方も使います。
パラメータ付き不動点性は、アスタリスクを使って次のように書けます。
$`\quad \langle \id_A, f^*\rangle \C f = f^*`$
$`\id_A`$ を単に $`A`$ と書く流儀を採用するとさらに簡潔に書けます。
$`\quad \langle A, f^*\rangle \C f = f^*`$
自然性（パラメータ変換公式）
$`(\mrm{Fix}^A_X)_{A, X\in |\cat{C}|}`$ をコンウェイ不動点オペレーター（写像の族）とします。2つのインデックス〈成分変数〉 $`A, X`$ がありますが、$`A`$（ここでは上付き）に関しては自然変換、$`X`$（ここでは下付き）に関しては対角自然変換〈dinatural transformation〉になっています。不動点オペレーターは、圏論的に良い特徴付け／定式化を持っていることになります。
$`\mrm{Fix}^A_X`$ の $`X`$ を固定して $`A`$ を動かした $`\mrm{Fix}^{\hyp}_X`$ は自然変換になります。この性質が、コンウェイ不動点オペレーターの自然性〈naturality〉です。
通常、自然変換の成分〈インデックス | 成分変数〉は下付きで書きますが、上付きに変更して、前層（集合圏への反変関手）のあいだの自然変換 $`\alpha :: F \twoto G`$ （2個のコロンは2-射である目印）の自然性四角形〈naturality square〉を描くと：
$`\T{For } u: A \to B \In \cat{C}\\
\quad \xymatrix{
F(B) \ar[r]^{\alpha^B} \ar[d]_{F(u)}
&G(B) \ar[d]^{G(u)}
\\
F(A) \ar[r]_{\alpha^A}
&G(A)
}\\
\quad \T{commutative}\In \mbf{Set}
`$
$`F, G`$ は反変関手なので、反対圏の射をオーバーライン記法（「反対圏とホム関手： オーバーライン、ブラケット、上付きop」参照））で書くなら：
$`\T{For } \o{u}: B \to A \In \cat{C}^\op\\
\quad \xymatrix{
F(B) \ar[r]^{\alpha^B} \ar[d]_{F(\o{u})}
&G(B) \ar[d]^{G(\o{u})}
\\
F(A) \ar[r]_{\alpha^A}
&G(A)
}\\
\quad \T{commutative}\In \mbf{Set}
`$
不動点オペレーターの場合は、$`\alpha^A = \mrm{Fix}^A_X`$ と置くのですが、$`F, G`$ に相当する前層がなにか？ 意外と分かりにくいです。答は：
- $`F(A) = \cat{C}(A\times X, X)`$
- $`G(A) = \cat{C}(A, X)`$
$`F`$ も $`G`$ もホム双関手〈hom bifunctor〉に含まれる変数 $`X`$ を固定したものです。変数 $`A`$ は関手の変数として生き残ります。
不動点オペレーターの場合の自然性四角形は：
$`\T{For } \o{u}: B \to A \In \cat{C}^\op\\
\quad \xymatrix{
{\cat{C}(B\times X, X)} \ar[r]^{\mrm{Fix}^B_X} \ar[d]_{\cat{C}(\o{u}\times\o{\id_X}, \id_X)}
&{\cat{C}(B, X)} \ar[d]^{\cat{C}(\o{u}, \id_X)}
\\
{\cat{C}(A\times X, X)} \ar[r]_{\mrm{Fix}^A_X}
&{\cat{C}(A, X)}
}\\
\quad \T{commutative}\In \mbf{Set}
`$
次のようにも書けます。
$`\T{For } \o{u}: B \to A \In \cat{C}^\op\\
\quad \xymatrix{
{\cat{C}^B(X, X)} \ar[r]^{\mrm{Fix}^B_X} \ar[d]_{\cat{C}^{\o{u}}(X, X) }
&{\cat{C}^B(\mbf{1}, X)} \ar[d]^{\cat{C}^{\o{u}} (\mbf{1}, X)}
\\
{\cat{C}^A(X, X)} \ar[r]_{\mrm{Fix}^A_X}
&{\cat{C}^A(\mbf{1}, X)}
}\\
\quad \T{commutative}\In \mbf{Set}
`$
上記の可換四角形の右側の辺は、$`u:A \to B`$ によるプレ結合引き戻し〈pre-composition pullback〉$`t \mapsto u\C t`$ とみなせます。
さて、コンウェイ不動点オペレーターの自然性を簡単な等式で表してみましょう。次のようになります。
$`\T{For }u: A \to B \In \cat{C}\\
\T{For }g: B\times X \to X \In \cat{C}\\
\quad [u\C_1 g]^* = u\C g^* \; : A \to X \In \cat{C}
`$
$`g \mapsto u\C_1 g`$ は、$`u`$ によるパラメータ変換とみなせます。よって、コンウェイ不動点オペレーターの自然性は、パラメータ変換した後の $`u\C_1 g`$ の不動点を“$`g`$ の不動点からどう計算するか”の公式を与えます。$`g`$ の不動点 $`g^*`$ を、パラメータ変換 $`u`$ によるプレ結合引き戻し〈pre-composition pullback〉で移送〈transfer〉するだけです。
対角自然性（結合順入れ替え公式）
コンウェイ不動点オペレーター $`(\mrm{Fix}^A_X)_{A, X\in |\cat{C}|}`$ は、下付きの成分変数 $`X`$ に関しては対角自然変換〈dinatural transformation〉になっています。
対角自然変換について少し復習します。$`P, Q : \cat{D}^\op\times \cat{D} \to \mbf{Set}`$ をプロ関手〈profunctor〉とします（この場合、自己プロ関手〈endo profunctor〉です）。対角自然変換は2つのプロ関手のあいだを結ぶ変換です。$`\beta`$ が対角自然変換であることを次のように書きます（二重矢印上のドットに注意）。
$`\quad \beta:: P \overset{\cdot}{\twoto} Q : \cat{D}^\op\times \cat{D} \to \mbf{Set}`$
$`\beta`$ の実体は、$`P`$ の対角成分から $`Q`$ の対角成分への写像の族です。
$`\T{For }X \in |\cat{D}|\\
\quad \beta_X : P(X, X) \to Q(X, X) \In \mbf{Set}
`$
この族 $`(\beta_X)_{X \in |\cat{D}|}`$ が対角自然変換であるための条件が対角自然性〈dinaturality〉です。対角自然性は、次の六角形図式の可換性として記述されます。以下、 $`\id_X`$ や $`\o{\id_X}`$ を単に $`X`$ で代用します。
$`\T{For }X, Y \in |\cat{D}|\\
\T{For } g: Y \to X \In \cat{D}\\
\T{i.e. } \o{g} : X \to Y \In \cat{D}^\op \\
\quad \xymatrix{
{}
&{P(Y, Y)} \ar[r]^{\beta_Y}
&{Q(Y, Y)} \ar[dr]^{Q(Y, g)}
&{}
\\
{P(X, Y)} \ar[ur]^{P(\o{g}, Y)} \ar[dr]_{P(X, g)}
&{}
&{}
&{Q(Y, X)}
\\
{}
&{P(X, X)} \ar[r]_{\beta_X}
&{Q(X, X)} \ar[ur]_{Q(\o{g}, X)}
&{}
}\\
\quad \T{commutative}\In \mbf{Set}
`$
ここで、いきなり不動点オペレーターにはいかないで、対角自然変換の特別なケースを見ておきます。$`\cat{D}`$ をデカルト圏だとして、プロ関手 $`P, Q`$ を次のように置きます。
- $`P(X, Y) := \cat{D}(X, Y)`$ （$`\cat{D}`$ のホム双関手 ＝ 恒等プロ関手）
- $`Q(X, Y) := \cat{D}_\mbf{1}(X, Y) := \cat{D}(\mbf{1}, Y)`$ （$`X`$ に無関係に、$`Y`$ の“ポイント”の集合）
この2つのプロ関手のあいだの対角自然変換を考えます。$`P`$ は単にホム双関手ですが、$`Q`$ は要注意です。共変の変数（第二引数） $`Y`$ は生きてますが、反変の変数（第一引数） $`X`$ はダミーです。ダミーの変数（何の影響もない）があると事情が見えにくくなります。
$`P, Q`$ を上記のように置いた状況で、対角自然変換 $`\beta`$ の対角自然性六角形〈dinaturality hexagon〉を描いてみます。
$`\T{For }X, Y \in |\cat{D}|\\
\T{For } g: Y \to X \In \cat{D}\\
\T{i.e. } \o{g} : X \to Y \In \cat{D}^\op \\
\quad \xymatrix{
{}
&{\cat{D}(Y, Y)} \ar[r]^{\beta_Y}
&{\cat{D}_\mbf{1}(Y, Y)} \ar[dr]^{\cat{D}_\mbf{1}(Y, g)}
&{}
\\
{\cat{D}(X, Y)} \ar[ur]^{\cat{D}(\o{g}, Y)} \ar[dr]_{\cat{D}(X, g)}
&{}
&{}
&{\cat{D}_\mbf{1}(Y, X)}
\\
{}
&{\cat{D}(X, X)} \ar[r]_{\beta_X}
&{\cat{D}_\mbf{1}(X, X)} \ar[ur]_{\cat{D}_\mbf{1}(\o{g}, X)}
&{}
}\\
\quad \T{commutative}\In \mbf{Set}
`$
ここで、右下の辺 $`\cat{D}_\mbf{1}(\o{g}, X): \cat{D}_\mbf{1}(X, X) \to \cat{D}_\mbf{1}(Y, X)`$ に注目します。定義により、第一引数（反変側の引数）は、$`\o{g}: X\to Y \In \cat{D}^\op`$ が何であっても、値は $`\id_\mbf{1} : \mbf{1}\to \mbf{1} \In \cat{D}`$ に潰れます。生き残るのは第二引数（共変側の引数）の効果ですが、第二引数は $`X = \id_X`$ なので実質的効果はありません。
したがって、右下の辺は恒等となり、六角形は五角形に退化します。
$`\T{For }X, Y \in |\cat{D}|\\
\T{For } g: Y \to X \In \cat{D}\\
\T{i.e. } \o{g} : X \to Y \In \cat{D}^\op \\
\quad \xymatrix{
{}
&{\cat{D}(Y, Y)} \ar[r]^{\beta_Y}
&{\cat{D}_\mbf{1}(Y, Y)} \ar[dd]^{\cat{D}_\mbf{1}(Y, g)}
&{}
\\
{\cat{D}(X, Y)} \ar[ur]^{\cat{D}(\o{g}, Y)} \ar[dr]_{\cat{D}(X, g)}
&{}
&{}
&{}
\\
{}
&{\cat{D}(X, X)} \ar[r]_{\beta_X}
&{\cat{D}_\mbf{1}(X, X)}
&{}
}\\
\quad \T{commutative}\In \mbf{Set}
`$
このままだと、右の辺 $`\cat{D}_\mbf{1}(Y, g) : \cat{D}_\mbf{1}(Y, Y) \to \cat{D}_\mbf{1}(X, X)`$ が奇妙な感じです。$`\id_Y : Y \to X`$ じゃオカシイ。でも、$`\cat{D}_\mbf{1}(\hyp, \hyp)`$ の定義に基づいて展開すれば奇妙ではなくなります。
$`\T{For }X, Y \in |\cat{D}|\\
\T{For } g: Y \to X \In \cat{D}\\
\T{i.e. } \o{g} : X \to Y \In \cat{D}^\op \\
\quad \xymatrix{
{}
&{\cat{D}(Y, Y)} \ar[r]^{\beta_Y}
&{\cat{D}(\mbf{1}, Y)} \ar[dd]^{\cat{D}(\mbf{1}, g)}
&{}
\\
{\cat{D}(X, Y)} \ar[ur]^{\cat{D}(\o{g}, Y)} \ar[dr]_{\cat{D}(X, g)}
&{}
&{}
&{}
\\
{}
&{\cat{D}(X, X)} \ar[r]_{\beta_X}
&{\cat{D}(\mbf{1}, X)}
&{}
}\\
\quad \T{commutative}\In \mbf{Set}
`$
過去記事「不動点理論と対角自然性（dinaturality）」や「不動点の対角自然性（dinaturality）はやっぱり五角形可換らしい」において、「なんで六角形じゃなくて五角形なんだろう？」と悩んでいましたが、こういう事情だったのです。
対角自然性（結合順入れ替え公式） 続き
前節で、対角自然性六角形が五角形に退化するケースがあることを説明しました。コンウェイ不動点オペレーターの対角自然性〈dinaturality〉はまさにそのケースなのです。対象 $`A\in |\cat{C}|`$ を固定して、$`\cat{D} = \cat{C}^A`$ と置きます。すると、前節の対角自然性五角形は次のようになります。
$`\T{For }X, Y \in |\cat{D}|\\
\T{For } g: Y \to X \In \cat{D}\\
\T{i.e. } \o{g} : X \to Y \In \cat{D}^\op \\
\quad \xymatrix{
{}
&{\cat{C}^A(Y, Y)} \ar[r]^{\mrm{Fix}^A_Y}
&{\cat{C}^A(\mbf{1}, Y)} \ar[dd]^{\cat{C}^A(\mbf{1}, g)}
&{}
\\
{\cat{C}^A(X, Y)} \ar[ur]^{\cat{C}^A(\o{g}, Y)} \ar[dr]_{\cat{C}^A(X, g)}
&{}
&{}
&{}
\\
{}
&{\cat{C}^A(X, X)} \ar[r]_{\mrm{Fix}^A_X}
&{\cat{C}^A(\mbf{1}, X)}
&{}
}\\
\quad \T{commutative}\In \mbf{Set}
`$
この可換図式を等式で表現すれば：
$`\quad \cat{C}^A(X, g) \C \mrm{Fix}^A_X = \cat{C}^A(\o{g}, Y) \C \mrm{Fix}^A_Y \C \cat{C}^A(\mbf{1}, g) \In \mbf{Set}`$
[追記 date="翌々日"]以下に、$`\star^{\mbf{1}}`$ と書いてあったのですが、$`\star^A`$ の間違いでした（僕の勘違い）。数式内では直接修正し、本文は取り消し線で消します。[/追記]
引数 $`f \in \cat{C}^A(X, Y)`$ を渡すには反図式順のほうが便利なので*7、反図式順の結合記号 $`\circ`$ で書くと：
$`\T{For }f \in \cat{C}^A(X, Y) \\
\quad (\mrm{Fix}^A_X \circ \cat{C}^A(X, g) )(f) = (\cat{C}^A(\mbf{1}, g) \circ \mrm{Fix}^A_Y \circ \cat{C}^A(\o{g}, Y) )(f)\\
\T{i.e.}\\
\quad [f \star^A g]^* = [g \star^A f]^* \star^A g
`$
$`\star^{\mbf{1}}`$ は $`\cat{C}`$ の結合とみなせるので $`\C`$ でもかまいません。簡潔な形式
$`\quad [f \star^A g]^* = [g \star^A f]^* \star^A g`$
を導出するには、定義に基づいた展開を律儀に行ってください。良い練習問題だと思います。
過去記事「不動点理論と対角自然性（dinaturality）」では、同じ事を次の記法で書いていました。
$`\quad (f\conc g)^\dagger = (g\conc f)^\dagger \conc g`$
この公式は、圏 $`\cat{C}^A`$ における2つの射 $`f:X \to Y`$ と $`g: Y \to X`$ に関して、順番を入れ替えた結合 $`f\star g`$ と $`g\star f`$ の不動点の関係を述べています。自己射 $`f\star g : X \to X`$ の不動点 $`[f\star g]^*`$ は、結合順を入れ替えた $`g\star f : Y \to Y`$ の不動点を、$`g`$ によるポスト結合前送り〈post-composition pushforward〉で移送〈transfer〉するだけです。
対角性（ダブルスター公式）
コンウェイ不動点オペレーターの対角性は、$`h:A\times X \times X \to X \In \cat{C}`$ のような、$`\cat{C}`$ の射（いわば、3変数の射）に不動点オペレーターを作用させたときに成立する等式です。簡潔な形式を先に出すと：
$`\quad h^{**} = [\Delta \C_2 h]^*`$
不動点オペレーターを2回続けて作用させることは、実は1回の作用で計算できるのです。
対角性〈diagonal property〉の公理をちゃんと書くと：
$`\T{For }h : A\times X\times X \to X \In \cat{C}\\
\quad \mrm{Fix}^A_X( \mrm{Fix}^{A\times X}_{X}(h) ) = \mrm{Fix}^A_X( (\id_A \times \Delta_X)\C h) \; : A \to X \In \cat{C}
`$
対角性の「対角」は $`\Delta_X`$ にちなむもので、前節の対角自然性とは関係ないです。
対角性を可換図式として描けば次のようになります。
$`\T{For }A, X \in |\cat{C}|\\
\quad \xymatrix@C+1pc{
{\cat{C}^A(X\times X, X)} \ar[r]^{(\Delta_X \C_2 \hyp)} \ar[d]_{\cong}
&{\cat{C}^A(X, X)} \ar[ddd]^{\mrm{Fix}^A_X}
\\
{\cat{C}^{A\times X}(X, X)} \ar[d]_{\mrm{Fix}^{A\times X}_X}
&{}
\\
{\cat{C}^{A\times X}(\mbf{1}, X)} \ar[d]_{\cong}
&{}
\\
{\cat{C}^A(X, X) } \ar[r]_{\mrm{Fix}^A_X}
&{\cat{C}^A(\mbf{1}, X)}
}\\
\quad \T{commutative}\In \mbf{Set}
`$
$`\cong`$ とマークされている射（写像）は、定義から自明に誘導される同型です。左上端から反時計回りが「不動点オペレーターの2回適用」、時計回りが「対角をプレ部分結合してから不動点オペレーター1回適用」です。
まとめ
コンウェイ不動点オペレーターの公理を、簡潔な計算公式の形で書くなら次のようです。
- パラメータ付き不動点性： $`\langle A, f^* \rangle\C f = f^*`$
- パラメータ変換公式（自然性）： $`[u \C_1 f]^* = u\C f^*`$
- 結合順入れ替え公式（対角自然性）： $`[f\star g]^* = [g\star f]^* \star g`$
- ダブルスター公式（対角性）： $`h^{**} = [\Delta \C_2 h]^*`$
結合順入れ替え公式（対角自然性）からパラメータ付き不動点性は出る*8ので、ほんとに必要な公式は3つしかありません。圏論的背景はちょっと複雑なんですが、パラメータ変換、結合順入れ替え、2回繰り返し適用の場合に不動点を計算するための基本公式です。
これらの公式を使った計算を実際に行う場合は、ストリング図とオペレーター・ボックスを使うと楽ちんです。例えば、結合順入れ替え公式からパラメータ付き不動点性を出すのはほぼ自明になります。ストリング図とオペレーター・ボックスの技法は、相対モナドやカン拡張などでも使えるものなので、いずれまとめて説明するかも知れません。
*1:圏論的概念なので、実際の変数が出てくるわけではないです。言葉の綾です。
*2:デカルト・ペアリングは、対角 $`\Delta`$ とデカルト積 $`\times`$ を使って、$`\langle f, g\rangle := \Delta\C (f\times g)`$ と書けます。
*3:t はほとんど発音しないようで、「プロキン」のほうが近いかも知れないです。
*4:"Complete Axioms for Categorical Fixed-point Operators" by Alex Simpson, Gordon Plotkin https://www.pure.ed.ac.uk/ws/portalfiles/portal/12418060/fixpoints.pdf
*5:シンプソン／プロトキンの公理は完全です。公理系が標準モデル達に対して健全〈sound〉なだけでなく十全〈adequate〉です。
*6:プラス記号に見えないように、∞ に縦棒とかで書いてます。が、あまり書きたくない。
*7:引数渡しが、右から渡すライプニッツ／オイラー記法が主流だからで、左から引数を渡せば図式順記法でもかまいません。
*8:$`[f\star g]^* = [g\star f]^* \C g`$ の $`f`$ を第二射影に取ります。
