https://m-hiyama.hatenablog.com/entry/2025/04/21/203809

2年ほど前（2023年の春）、二重圏ベースでハイパードクトリンを定義できないかとジタバタしていました。

結局、ハッキリとした定式化は得られず、締りのないままに放置。ですが、アイディアと方向性は正しかったように思います。道具・手段が足りてなかった、と。

ディスプレイクラスやC-システムを知った2024年の秋に、次の過去記事でもう一度“二重圏ベースのハイパードクトリン”に触れています。

コンテキストの圏と指標の圏と限量子 // エス関手とハイパードクトリン

2023年に「シード射」「シード四角形」と呼んでいた曖昧な概念が、C-システムの「標準射影」と「標準プルバック四角形」として定義できる、と指摘していますが、その先には進んでいません。

今（2025年春）みたび考え直してみると、クラン（「クラン、ファイブレーション、スパン」参照）と包括クラン（「テレスコープと包括クラン // 包括クラン」参照）を使えば、2023年当時の発想と方針を先に進めることが出来そうです。その発想・方針とは：

ハイパードクトリンは二重圏のあいだの二重関手であり、ハイパードクトリンの条件であるベック／シュバレー条件は、二重関手に関する条件になるはずだ。

この発想・方針は、「随伴系の二重圏」で述べた、パルムクイスト〈Paul H. Palmquist〉の二重圏とうまく繋がります。二重圏的視点〈double categorical perspective〉で見ると、新しいモノ・コトが見つかったりするかも知れません（期待）。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
\newcommand{\msc}[1]{\mathscr{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
%\newcommand{\o}[1]{\overline{#1}}
%\newcommand{\id}{\mathrm{id}}
\newcommand{\op}{\mathrm{op}}
\newcommand{\In}{\text{ in }}
\newcommand{\hyp}{ \text{－} }
\newcommand{\twoto}{\Rightarrow }
\newcommand{\dimU}[2]{ {{#1}\!\updownarrow^{#2}} }
%
%
\newcommand{\SWArrow}{\style{display: inline-block; transform: rotate(-45deg)}{\Leftarrow} }
\newcommand{\SEArrow}{\style{display: inline-block; transform: rotate(45deg)}{\Rightarrow} }
\newcommand{\NEArrow}{\style{display: inline-block; transform: rotate(-45deg)}{\Rightarrow} }
`$

内容：

ハブ記事：

圏論的述語論理とお絵描き

ハイパードクトリンとは

ハイパードクトリンとは、述語論理の圏論的な定式化です。論理には命題論理と述語論理がありますが、この二種の区別は人により違います。ここでは、限量子〈quantifier〉を扱うのが述語論理、限量子が出てこないなら命題論理としましょう。この定義では、命題論理でも述語を扱います。「述語を扱うのが述語論理」ではありません！

カリー／ハワード／ランベック対応によれば、論理と型理論に本質的な違いはありません。よって、述語論理の圏論的な定式化とは、型理論の圏論的な定式化と同じことです。型理論で限量子に相当するものはシグマ型とパイ型です。シグマ型が存在限量子に相当し、パイ型が全称限量子に相当します。

そういう事情でハイパードクトリンは、シグマ型とパイ型を持つような型理論の圏論的な定式化でもあります。論理の用語とメンタルモデルで語るときは“ハイパードクトリン”と呼ぶ、ということです。呼び名だけの問題で論理のメンタリティや解釈法が無意味なのか？というと、そうでもなくて、型理論的な態度では見過ごしがちな所に注意が向いたりします。

ベック／シュバレー条件は、論理的な観点からは注目され、型理論的な観点ではあまり話題にされない性質です。ベック／シュバレー条件を強調した型理論の方言がハイパードクトリン（の理論）だとも言えます。

述語論理では、存在限量子と全称限量子をセットにして扱います。が、型理論ではパイ型だけを考えるなんてこともあります。ここでは、存在限量子だけを持つハイパードクトリンを存在的ハイパードクトリン〈existential hyperdoctrine〉、全称限量子だけを持つハイパードクトリンを全称的ハイパードクトリン〈universal hyperdoctrine〉と呼びます。ただし、universal は他の意味でよく使われているので誤解されそうだから、右ハイパードクトリン〈right hyperdoctrine〉という言葉も使います（定義は後述）。となると、存在的ハイパードクトリンは左ハイパードクトリン〈left hyperdoctrine〉とも呼ぶことになります。ここでの「左右」は、随伴ペアの「左右」と関係します。

エス関手

エス関手は「コンテキストの圏と指標の圏と限量子 // エス関手」で導入しています。過去記事でエス関手の由来は説明していますが、形式的な記述はしていません。ここでもう少しハッキリさせます。

エス関手は包括構造（「大きい包括クランの3つの例 // 包括構造の定義」参照）の一部です。以下のような、圏 $`\cat{C}`$ 上の包括構造があったとします。

$`\quad \xymatrix{
\cat{E} \ar[d]_{\pi} \ar[r]^-{\gamma}
&{\mrm{Arr}(\cat{C})} \ar[d]^{\mrm{Cod}}
\\
\cat{C} \ar@{=}[r]
&\cat{C}
}\\
\quad \text{commutative }\In \mbf{CAT}
`$

ファイブレーション〈ファイバー付き圏〉 $`\pi: \cat{E}\to \cat{C}`$ に対応するインデックス付き圏が、包括構造〈包括圏〉のエス関手〈ess functor〉です。ファイブレーションとインデックス付き圏は、グロタンディーク構成／逆グロタンディーク構成（「グロタンディーク構成・逆構成と同値対応」参照）で対応します。

別な言い方をすると、圏 $`\cat{C}`$ 上のインデックス付き圏 $`S : \cat{C}^\op \to \mrm{CAT}`$ があり、それから次の包括構造を作ったとき、関手〈インデックス付き圏〉 $`S`$ は、当該包括構造〈包括圏〉のエス関手です。

$`\quad \xymatrix{
{\int_\cat{C} S} \ar[d]_{\pi} \ar[r]^-{\gamma}
&{\mrm{Arr}(\cat{C})} \ar[d]^{\mrm{Cod}}
\\
\cat{C} \ar@{=}[r]
&\cat{C}
}\\
\quad \text{commutative }\In \mbf{CAT}
`$

「エス関手」という言葉は、包括圏という構造の構成素役割り名〈constituent role name〉ですが、いったんグロタンディーク構成を通すので間接的な構成素といえます。

エス関手の余域は $`\mbf{CAT}`$ としましたが、一般化しておきます。$`\cat{K}`$ は2-圏だとします。エス関手は $`S:(\dimU{\cat{C}}{2})^\op \to \cat{K} \In \mathbb{2CAT}`$ の形のスード反変2-関手でもよいとします。ここで $`\dimU{\cat{C}}{2}`$ は、1-圏を“射の等式”を2-射とみなして2-圏としたものです。

ただし、$`\cat{K}`$ が単なる2-圏だとグロタンディーク構成によりファイブレーションを作れないので、具象化関手〈concretization functor〉$`U: \cat{K} \to \mbf{CAT}`$ を持つとします。抽象的な2-圏の対象 $`a\in |\cat{K}|`$ に対して、$`U(a)`$ は具体的な圏です。具象化関手（2-関手）を備えた2-圏を具象2-圏〈concrete 2-category〉と呼びます。

具象化関手（2-関手） $`U`$ の条件は、ホム圏 $`\cat{K}(a, b)`$ に制限した1-関手
$`\quad U_{a, b} : \cat{K}(a, b) \to \mbf{CAT}(U(a), U(b)) \In \mbf{CAT}`$
がすべて埋め込み関手（「方向とオリエンテーション、圏論の絵図 // 埋め込み関手」参照）であることです。

エス関手からファイブレーションを作るときは、インデックス付き圏（圏達の2-圏へのスード反変2-関手） $`S*U`$ からグロタンディーク構成をします。

包括クラン

基本となる圏は単なる圏ではなくてクラン〈clan〉（「クラン、ファイブレーション、スパン」参照）です。記号の乱用により、クランを次のように書きます。

$`\quad \cat{C} = (\cat{C}, \mbf{1}, \cat{P})`$

$`\cat{P}`$ はファイブレーションクラスです。ファイブレーションクラスに属する射を射影〈projection〉とも呼びます。

$`\cat{C}`$ 上にエス関手 $`\msc{S}`$ （目立つように筆記体の S）があり、それによる包括構造があるとします。つまり、$`\cat{C}`$ は包括クラン〈comprehension clan〉（「テレスコープと包括クラン // 包括クラン」「大きい包括クランの3つの例」参照）になっているとします。この状況で、次の概念が意味を持ちます。

コンテキスト〈context〉： $`\cat{C}`$ の対象のこと。習慣により、$`\Gamma, \Delta`$ などと書く。
拡張ステップ〈extension step〉： $`\msc{S}(\Gamma)`$ の対象のこと。型理論では型、またはソート、論理では命題、インスティチューション理論では文と呼ばれているもの（「コンテキストの圏と指標の圏と限量子 // エス関手」参照）。
射影〈projection〉：クランのファイブレーションクラスの要素である射。ファイブレーション、ディスプレイ射とも呼ぶ。
コンテキスト拡張〈context extension〉：コンテキスト $`\Gamma`$ と拡張ステップ $`A\in |\msc{S}(\Gamma)|`$ から新しいコンテキスト $`\Gamma\cdot A`$ を作る操作、またはその結果。
標準射影〈canonical projection〉：コンテキスト $`\Gamma`$ と拡張ステップ $`A\in |\msc{S}(\Gamma)|`$ から決まる射 $`\rho^{\Gamma, A} : \Gamma\cdot A \to \Gamma\In \cat{C}`$ 。標準射影は射影である。
標準プルバック四角形〈canonical pullback square〉：任意の射 $`f:\Delta \to \Gamma \In \cat{C}`$ と拡張ステップ $`A\in |\msc{S}(\Gamma)|`$ から決まる $`\cat{C}`$ 内のプルバック四角形。$`f`$ と $`\rho^{\Gamma, A}`$ からなるコスパンを含む四角形。

プルバック四角形達の二重圏

二重圏的ハイパードクトリンのアイディアは、ハイパードクトリンをとある二重圏 $`\cat{D}`$ からの二重関手だとみなすことです。2023年時点では「とある二重圏 $`\cat{D}`$」の定義がイマイチ曖昧でした。包括クランを使えば、「とある二重圏 $`\cat{D}`$」をハッキリと定義できます。

包括クランの標準プルバック四角形は次の形でした。

$`\quad \xymatrix{
\cdot \ar[r] \ar[d]
\ar@{}[dr]|{\text{p.b.}}
&{\Gamma\cdot A} \ar[d]^{\rho^{\Gamma, A}}
\\
\cdot \ar[r]_f
&\Gamma
}\\
\quad \In\cat{C}
`$

この四角形は、アロー圏〈バンドル達の圏 | 可換四角形達の圏〉$`\mrm{Arr}(\cat{C})`$ 内の、コドメイン関手 $`\mrm{Cod}`$ に関するデカルト射（「関手のデカルト射とファイバー付き圏」参照）だとみなせます。

さて、標準プルバック四角形を基本二重射として生成される二重圏を定義します。コンテキスト達の圏 $`\cat{C}`$ の任意の射をタイト射として、標準射影を基本プロ射（プロ射の生成元）だとします。基本二重射（二重射の生成元）は標準プルバック四角形です。

僕は（個人的に）プロ射を横方向に描いたほうが心が落ち着くので、基本二重射は次のレイアウトで描きます。上の図を、時計回りに90度回転してから左右反転〈鏡映〉しています（「方向とオリエンテーション、圏論の絵図 // 圏論における絵図：描画方向と射の方向」参照）。スラッシュはプロ射であることの目印です。

$`\quad \xymatrix{
\cdot \ar[r]|{/} \ar[d]
\ar@{}[dr]|{\text{p.b.}}
&\cdot \ar[d]^f
\\
{\Gamma\cdot A} \ar[r]|{/}_{\rho^{\Gamma, A}}
&\Gamma
}
`$

タイト射の結合と、二重射のタイト方向への結合は容易に定義できます。基本プロ射（＝標準射影）の結合で得られる射を（一般の）プロ射とします。こう定義すると、プロ射の結合はプロ射になります。一般の二重射のプロ方向への結合も、プルバック四角形の結合として定義できます。こうして構成される構造が二重圏になることの確認は、面倒ですがやれば出来ます。

この二重圏のプロ射は標準射影達の結合ですが、プロ射の標準射影達への分解が一意にできることは保証できません。が、もし、$`\cat{C}`$ にカートメルツリー構造（「C-システム、分裂ディスプレイクラス、カートメルツリー構造」「クランからC-システム」参照）が載っていれば、プロ射の標準射影達への分解は一意的になります。

包括クラン $`\cat{C}`$ の標準プルバック四角形達から生成される二重圏を $`\mrm{CBPSqDC}(\cat{C})`$ とします。一時的に $`\cat{D} := \mrm{CBPSqDC}(\cat{C})`$ と置きます。

二重圏 $`\cat{D}`$ では、フレーム（二重射の境界となる四辺形）に対して二重射が高々1つしかないので、やせた二重圏〈thin double category〉です。より強く、フレーム全体ではなくて、フレーム内のコスパンが決まれば、二重射が一意に決まります。フレームから二重射の対応は、包括構造のファイブレーションの分裂子〈splitting〉（「ファイブレーションの亀裂と分裂」参照）を使って構成できます。

二重圏 $`\cat{D}`$ のプロ射は、標準射影の結合により2つのコンテキストを繋ぐものです。これは、コンテキスト達の圏 $`\cat{C}`$ 内部のファイブレーションだと言えます。もともと、クランのファイブレーションクラスに所属するので「ファイブレーション」なのですが、より内容的に考えても“ファイブレーション〈fibered context〉”だということです。そして、二重圏 $`\cat{D}`$ の二重射は、（タイト方向にみて）ファイブレーション〈fibered context〉のあいだの準同型射だとみなせます。

パルムクイスト二重圏

パルムクイスト二重圏〈Palmquist double category〉とは、過去記事「随伴系の二重圏」で導入した、随伴系をプロ射とする二重圏のことだとします。この二重圏は、1969年にポール・パルムクイスト〈Paul H. Palmquist〉が学位論文で定義しています。

パルムクイスト二重圏の二重射を図示すると次のようになります。

パルムクイスト二重圏のタイト射は関手です。プロ射は、随伴関手ペア〈随伴系〉です。上の図の上下が2つのプロ射です。上下のプロ射（随伴関手ペア）に注目してペースティング図にすると：

$`\quad \xymatrix@R+0.5pc {
\cat{C} \ar@/^/[r]^{R} \ar[d]_F
\ar@{}[r]|{\top}
&\cat{D} \ar@/^/[l]^{L} \ar[d]^G
\\
\cat{C'} \ar@/^/[r]^{R'}
\ar@{}[r]|{\top}
&\cat{D'} \ar@/^/[l]^{L'}
}
`$

パルムクイスト二重圏の二重射は、上の図のピンク色の面と青色の面のペアになります。ピンク色の面〈四角形〉を抜き出して、ペースティング図で表すと次のようです。

$`\quad \xymatrix{
\cat{C} \ar[r]^{L} \ar[d]_F
\ar@{.}[dr]|{\NEArrow}
&\cat{D} \ar[d]^G
\\
\cat{C'}\ar[r]_{L'}
&\cat{D'}
}
`$

青色の面〈四角形〉を抜き出して、ペースティング図で表すと次のようです。

$`\quad \xymatrix{
\cat{C} \ar[d]_F
&\cat{D} \ar[l]_{R}\ar[d]^G
\ar@{.}[dl]|{\SEArrow}
\\
\cat{C'}
&\cat{D'} \ar[l]^{R'}
}
`$

点線の対角線については「n角形の対角線とペースティング図」を参照してください。

二重射を $`\alpha`$ としたとき、左関手のあいだを繋ぐピンク色の面を $`\alpha_\mrm{left}`$ 、右関手のあいだを繋ぐ青色の面を $`\alpha_\mrm{right}`$ とします。次のように書けます。

$`\quad \alpha = (\alpha_\mrm{left}, \alpha_\mrm{right})`$

ペースティング図で描けば、$`\alpha_\mrm{left}, \alpha_\mrm{right}`$ はそれぞれ四角形ですが、ストリング図で描くと4脚の（4本のワイヤーを持つ）ノードになります。

$`\alpha_\mrm{left}`$ と $`\alpha_\mrm{right}`$ は無関係ではなくて、互いにメイト〈mate〉になっています。メイトについては、「随伴系の二重圏 // メイト」に書いてあります。

パルムクイスト二重圏のプロ射は随伴関手ペアですが、プロ射の方向の決め方が、「左関手にあわせる／右関手にあわせる」の二通りあります。どちらを選ぶかによって別な二重圏ができます。

一般に、随伴系〈adjunction | adjoint pair | adjoint system〉は、2-圏 $`\cat{K}`$ のなかで定義できます。$`\cat{K}`$ 内の随伴系をプロ射とするパルムクイスト二重圏を $`\mrm{AdjDC}_\mrm{L}(\cat{K})`$ とします。下付きの $`{_\mrm{L}}`$ は、プロ射の方向が左関手方向であることを示します。右関手方向に選べば $`\mrm{AdjDC}_\mrm{R}(\cat{K})`$ です。$`\cat{K} = \mbf{CAT}`$ のときは、$`\mbf{AdjDC}_\mrm{L}, \mbf{AdjDC}_\mrm{R}`$ と書くことにします。

パルムクイスト二重圏の二重射は2枚の四角形から構成されますが、それぞれは2-圏のクインテット（「2-圏からのクインテット構成で二重圏」参照）です。また、どちらか一枚の四角形（クインテット）が決まれば、もう一方はメイトとして作れます。したがって、一枚のクインテットでも二重射を指定するには十分です。必要に応じて、二重射 $`\alpha`$ をクインテット $`\alpha_\mrm{left}`$ で、またはクインテット $`\alpha_\mrm{right}`$ で代表させることができます。

なお、以下の過去記事で、二重圏だけでなく1-圏や0-圏としての“随伴系達が作る構造”を扱っています。

すべての随伴系達が作る構造は？

左可指数／右可指数な包括クラン

$`\cat{C}`$ を包括クランとします。記号の乱用で、包括クランの台クランや台クランの台圏も同じ $`\cat{C}`$ で表します。包括クラン $`\cat{C}`$ のエス関手は次のようだとします。

$`\quad \msc{S} : (\dimU{\cat{C}}{2})^\op \to \cat{K}\In \mathbb{2CAT}`$

ここで、$`\cat{K}`$ は具象2-圏です。$`\cat{K}`$ の具体例としては、$`\mbf{Set}`$ や $`\mbf{Cat}`$ を想定してください。

コンテキストのあいだの射 $`f:\Delta \to \Gamma \In \cat{C}`$ が、エス関手 $`\msc{S}`$ に関して右可指数〈right exponentiable〉であるとは、$`\msc{S}(f)`$ が $`\cat{K}`$ において右随伴を持つことです。

この定義は、エス関手が特別なケースにおいて、単に可指数〈exponentiable〉と呼ばれる性質を一般化したものです。exponentiable morphism については、nLab項目 "exponential object // Related notions" を参照してください。

同様に、$`f`$ が左可指数〈right exponentiable〉であるとは、$`\msc{S}(f)`$ が $`\cat{K}`$ において左随伴を持つことです。

包括クランが左可指数／右可指数であるとは、すべての射影〈ファイブレーション〉がエス関手に関して左可指数／右可指数であることです。標準射影は射影なので、包括クランが左可指数／右可指数ならば、標準射影は左可指数／右可指数です。

論理の文脈で解釈すれば、射影 $`p`$ に対する $`\msc{S}(p)`$ は、述語の変数水増しで、$`\msc{S}(p)`$ の右随伴は全称限量子、$`\msc{S}(p)`$ の左随伴は存在限量子です。この状況から用語を借用して：

包括クランの射影 $`p`$ に対して、$`\msc{S}(p)`$ を、$`p`$ による水増し〈thinnig〉と呼ぶ。
水増し $`\msc{S}(p)`$ の左随伴を、$`p`$ による存在限量子〈existential quantifier〉と呼ぶ。
水増し $`\msc{S}(p)`$ の右随伴を、$`p`$ による全称限量子〈universal quantifier〉と呼ぶ。

以上の用語法は、論理にちなんだ名付けであり、他の名付けもあります。

二重圏的ハイパードクトリン

最初の節でも触れたように、ハイパードクトリンを左ハイパードクトリン〈存在的ハイパードクトリン〉と右ハイパードクトリン〈全称的ハイパードクトリン〉に分けます。左右両方の構造を備えていれば、単にハイパードクトリンと呼びます。

以下、左ハイパードクトリン〈left hyperdoctrine〉を定義します。

$`\cat{C}`$ を左可指数な包括クランとします。射影〈ファイブレーション〉$`p`$ に対する $`\msc{S}(p)`$〈水増し〉を、$`p^*`$ と略記します。左可指数性から、$`p^*`$ は左随伴〈存在限量子〉を持ちます。それを $`\exists_p`$ と書きます。クランのファイブレーションクラスを $`\cat{P}`$ として、以下の状況です。

$`\text{For }p: \Delta \to \Gamma \In \cat{C} \text{ where }p\in \cat{P}\\
\quad \xymatrix@C+1pc{
{\msc{S}(\Gamma) } \ar@/_1pc/[r]_{\exists_p}
\ar@{}[r]|{\top}
&{\msc{S}(\Delta) } \ar@/_1pc/[l]_{p^*}
}\\
\quad \In \cat{K}
`$

ところで、包括クラン $`\cat{C}`$ のエス関手は次の形でした。

$`\quad \msc{S} :(\dimU{\cat{C}}{2})^\op \to \cat{K} \In \mathbb{2CAT}`$

$`\cat{C}`$ が左可指数であることを利用すると、エス関手から次の形の二重関手 $`\widetilde{\msc{S}}`$ を構成できます。

$`\quad \widetilde{\msc{S}} : \mrm{CPBSqDC}(\cat{C}) \to \mrm{AdjDC}_\mrm{L}(\cat{K}) \In \mbf{DblCAT}`$

二重関手 $`\widetilde{\msc{S}}`$ の具体的な構成法は次節に回すとして、二重関手 $`\widetilde{\msc{S}}`$ が左ハイパードクトリンと呼べるための要件であるベック／シュバレー条件〈Beck-Chevalley condition〉について述べます。

以下は二重圏 $`\mrm{CPBSqDC}(\cat{C})`$ の二重射だとします。

$`\quad \xymatrix{
\circ \ar[r]|{/} \ar[d]
\ar@{}[dr]|{\text{p.b.}}
&\cdot \ar[d]
\\
\cdot \ar[r]|{/}
&\bullet
}\\
\quad \In \mrm{CPBSqDC}(\cat{C})
`$

これは、$`\cat{C}`$ 内の図式と解釈できます。その図式を、$`\msc{S}`$（$`\widetilde{\msc{S} }`$ ではない）で $`\cat{K}`$ に移すと次の図式ができます（詳細は次節）。

$`\quad \xymatrix{
\circ \ar@/_/[r]|{\exists}
&\cdot \ar@/_/[l]|{*}
\\
\cdot \ar[u] \ar@/_/[r]|{\exists}
&\bullet \ar[u] \ar@/_/[l]|{*}
}\\
\quad \In \cat{K}
`$

星印が付いた矢印は水増しで、存在記号（$`\exists`$）が付いた矢印は左随伴である存在限量子です。随伴系の左関手〈左1-射〉を上下に持つ面を取り出すと次のようです。

$`\quad \xymatrix{
\circ \ar@/_/[r]|{\exists}
&\cdot
\ar@{.}[dl]|{\SEArrow}
\\
\cdot \ar[u] \ar@/_/[r]|{\exists}
&\bullet \ar[u]
}\\
\quad \In \cat{K}
`$

これは、随伴系の右関手〈右1-射〉を上下に持つ“裏側の面”からメイトとして作られた、2-圏 $`\cat{K}`$ 内のクインテットです。クインテットの実体は2-射（通常は自然変換）なので、可逆性を云々できます。可逆になっているとき、左ベック／シュバレー条件を満たす、といいます。

左ベック／シュバレー条件は、エス関手 $`\msc{S}`$ に対する条件ですが、二重関手 $`\widetilde{\msc{S}}`$ に関する条件だとも言えます。なぜなら、$`\widetilde{\msc{S}}`$ の行き先（値、像）に条件を付けているからです。

$`\widetilde{\msc{S}}`$ が（もとを正せば $`\msc{S}`$ が）左ベック／シュバレー条件を満たすとき、二重関手 $`\widetilde{\msc{S}}`$ を左ハイパードクトリン〈left hyperdoctrine〉と呼びます。右ハイパードクトリンも同様に定義できます。左ハイパードクトリンを存在的ハイパードクトリン〈exisitential hyperdoctrine〉、右ハイパードクトリンを全称的ハイパードクトリン〈universal hyperdoctrine〉とも呼びます。左ハイパードクトリンかつ右ハイパードクトリンなら、単にハイパードクトリン〈hyperdoctrine〉と呼びます。ハイパードクトリンは、2つの限量子を備えた述語論理の定式化です。

二重関手の構成

$`\msc{S}`$ から $`\widetilde{\msc{S}}`$ を構成する方法を述べます。

前節と同じ図式を考えます。

$`\quad \xymatrix{
\circ \ar[r]|{/} \ar[d]
\ar@{}[dr]|{\text{p.b.}}
&\cdot \ar[d]
\\
\cdot \ar[r]|{/}
&\bullet
}
`$

これは $`\mrm{CPBSqDC}(\cat{C})`$ の二重射ですが、同じ図式を $`\cat{C}`$ 内で解釈すればプルバック図式です。プルバック図式の内部は等式で埋められて（2-射が張られて）います。これを $`\msc{S}`$ で $`\cat{K}`$ 内に移すと、先の図の“裏側の面”（奥のほうの面）が生じます。

$`\quad \xymatrix{
\circ
\ar@{.}[dr]|{\SWArrow}
&\cdot \ar@/_/[l]|{*}
\\
\cdot \ar[u]
&\bullet \ar[u] \ar@/_/[l]|{*}
}\\
\quad \In \cat{K}
`$

これは $`\cat{K}`$ 内のクインテットですが、上下の水増しは左随伴を持つので、メイトにより“表側の面”（手前のほうの面）を作れます。表裏二枚でパルムクイスト二重圏の二重射になります。こうして、$`\mrm{CPBSqDC}(\cat{C})`$ の二重射から、$`\mrm{AdjDC}_\mrm{L}(\cat{K})`$ の二重射への対応を作れました。

対象、タイト射、プロ射、二重射の対応が決まっても、二重関手となるのは幾つかの条件をクリアしなくてはなりません。長く退屈になるので省略します。

おわりに

包括クランの上にハイパードクトリンを定義すると、一般性もありながらハッキリとした描像を持てます。二重関手としてのハイパードクトリンを定義するために使った、プルバック四角形の二重圏とパルムクイスト二重圏は、それ自体としても面白く役に立ちます。包括クランを調べる場合も、プルバック四角形の二重圏を一緒に考えるのは有効でしょう。

ハイパードクトリンを二重圏と二重関手として定義できたので、二重圏的視点〈double categorical perspective〉からハイパードクトリンを観察できる準備が整いました。

述語論理：ハイパードクトリンとパルムクイスト二重圏