コンテキスタッドかぁ、ウーム‥‥

2024年の春に、依存アクテゴリー〈dependent actegory〉に関する一連の記事を書きました。

• ハブ記事： 環境付き計算と依存アクテゴリー 1/n

依存アクテゴリーは、マッテーオ・カプチとディビッド・ジャズ・マイヤースの発案による圏論的構造です。2023年時点では、oplax dependent actegory〈反ラックス依存アクテゴリー〉と呼んでました。その後、fibered actegory, fibered action などの名前も使われましたが、結局 contextad〈コンテキスタッド〉に落ち着いたようです。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\In}{\text{ in }}
\newcommand{\op}{\mathrm{op}}
\newcommand{\id}{\mathrm{id}}
`$

2023年の最初のアナウンスでは3ページの資料しかありませんでしたが、2024年後半に以下の論文が出ました。

• [CM24-]
• Title: Contextads as Wreaths; Kleisli, Para, and Span Constructions as Wreath Products
• Authors: Matteo Capucci, David Jaz Myers
• Submitted: 29 Oct 2024
• Pages: 84p
• URL: https://arxiv.org/abs/2410.21889

コンテキスタッド

コンテキスタッドは、依存アクテゴリーをさらに一般化・抽象化した概念です。圏達の2-圏 $`\mbf{Cat}`$（あるいは $`\mbf{CAT}`$）だけではなくて、良い構造と性質を持つ2-圏 $`\cat{K}`$（パラダイスと呼ぶ）をベースに理論を展開します。2-圏 $`\cat{K}`$ 内のスパンの圏 $`x\mrm{Span}(\cat{K})`$ を作ります。$`x`$ は、スパンに付ける条件を象徴する文字です。スパンの圏 $`x\mrm{Span}(\cat{K})`$ は 3-圏になります。この3-圏内のモナド（正確にはスードモナド）がコンテキスタッド〈contextad〉です。

コンテキスタッドの台となるスパンを次のように書きます。

$`\quad \cat{C} \overset{\pi}{\twoheadleftarrow} \cat{E} \overset{\odot}{\to} \cat{C}
\In \cat{K}
`$

コンテキスタッドの台スパンは、左右の足〈foot〉が同じ対象 $`\cat{C}`$ です。左脚〈left leg〉が特殊な矢印 $`\twoheadleftarrow`$ なのは、何らかの条件が付いていることを示します。「何の条件も付けない」ことも何らかの条件の一種です。

よくある記号の乱用により、コンテキスタッドの台によりコンテキスタッドを代表させます。しかし、コンテキスタッド全体は複雑で大規模な構造です。上記論文 [CM24-] の Definition3.17. がコンテキスタッドの定義ですが、形式的定義だけで3ページを費やしています。

カプチ／マイヤースはさらに略記を進めて、スパンの右脚 $`\odot`$ だけでコンテキスタッド全体を代表させています。とあるコンテキスタッドを「コンテキスタッド $`\odot`$」と表現します。

コンテキスタッドの出発点（起源）はアクテゴリーです。$`\cat{M}`$ をモノイド圏として、圏 $`\cat{C}`$ に右から作用しているとします。そのとき、アクテゴリーの基本部分は次のように書けます。

$`\quad \cat{C} \overset{\pi}{\twoheadleftarrow} \cat{C}\times\cat{M} \overset{\odot}{\to} \cat{C}
\In \mbf{Cat}
`$

ここで、$`\pi`$ は直積の第一射影で、双関手〈二項関手〉 $`\odot`$ は $`\cat{M}`$ による右作用です。アクテゴリーの中核は右作用 $`\odot`$ なので、「アクテゴリー $`\odot`$」と言ってもいいでしょう。

と、そんなわけで、アクテゴリーで使っていた記法や言い回しをコンテキスタッドでも踏襲しているのです。

型理論から作られるコンテキスタッド

カプチ／マイヤースは、どこかで（どこだったかは忘れた）「依存アクテゴリーが型理論と関係するだろう」と言ったか書いたかしていました。僕はそれを真に受けて、依存アクテゴリーを型理論に使う気でいました（今でもその気）。コンテキスタッドはより抽象化されているので、型理論への適用はむしろ容易になったと思います。

バート・ジェイコブス〈Bart Jacobs〉の包括圏にエリック・パルムグレン〈Erik Palmgren〉のテレスコープのアイディアを入れた構造からコンテキスタッドを作れます。この型理論的コンテキスタッドに、カプチ／マイヤースのコンテキスト構成（$`\mathfrak{Ctx}`$ 構成）*1を施すと二重圏が作れます。型理論的コンテキスタッドから作られた二重圏は型理論的二重圏と呼ぶことにします。

　　型理論的コンテキスタッド --(コンテキスト構成)-→ 型理論的二重圏

型理論的二重圏のプロ射〈ルーズ射〉を見ると、それは「型理論へのファイブレーション的アプローチ： インスタンスとは // ハープーン」で述べたインスタンス〈ハープーン〉の双対になります。ここでの双対は矢印を反対向きにする（反対圏で考える）だけのことなので、プロ射はインスタンスと言っていいでしょう。

型理論的二重圏の対象は“型理論の意味でのコンテキスト”で、タイト射は“型理論の意味でのコンテキスト射”です。“型理論の意味での型”は、型理論的コンテキスタッドの台スパンのボディの対象です。

一方で、カプチ／マイヤースはアクテゴリーの流れから考えているので、コンテキスタッドの台スパンのボディの対象がコンテキストなのです。

型理論用語とカプチ／マイヤースの用語を対比してみると：

型理論	カプチ／マイヤース
コンテキスト	型 (注1)
型	コンテキスト
インスタンス (注2)	コンテキストフル射

• 注1： カプチ／マイヤースが用語「型」を使っているわけではないのですが、射（関数相当）の入力と出力の仕様を与える、という意味で型です。
• 注2： 型理論ではインスタンスを「項〈term〉」と呼ぶ習慣（悪習）があります。「型理論へのファイブレーション的アプローチ： インスタンスとは // 「インスタンス」を「項」と呼ぶのはやめよう」参照。

カプチ／マイヤースのテーマは、コンテキストフルな計算です。ここでのコンテキストは、明示的な入力と出力以外で計算に影響を与える要因のことです -- この意味で用語「コンテキスト」を使う時点で嫌な予感はしましたが、案の定、型理論とはひどく食い違った（真逆とも言える）用語法になってしまいました。

コンテキスタッドと型理論は相性が良さそうなんですが、用語的には、混乱をまねくトテモヤヤコシイ事態となってしまいました。ウーム‥‥