カプチ／マイヤース〈Matteo Capucci, David Jaz Myers〉のコンテキスタッドは、最近の記事「コンテキスタッドかぁ、ウーム‥‥」で紹介しました。依存アクテゴリーと呼ばれていた頃（2023年末）から注目はしていましたが（「依存アクテゴリーが面白い」参照）。
僕にとってのコンテキスタッドのご利益・ありがたみは、ジェイコブス〈Bart Jacobs〉の包括圏とローヴェア〈William Lawvere〉のハイパードクトリンに対して適切な“議論の枠組み”を提供してくれることです。包括圏／ハイパードクトリンをコンテキスタッドの枠組みにフィットさせるためには若干の細工が必要です。その細工が従来から知られていた構成法になるところもまた面白いです。$`\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\twoto}{\Rightarrow }
\newcommand{\lto}{\sqsubseteq }
\newcommand{\ot}{\leftarrow }
%\newcommand{\parto}{ \supset\!\to }
\newcommand{\In}{\text{ in }}
\newcommand{\op}{\mathrm{op}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\u}[1]{\underline{#1}}
\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{ \text{－} }
%\newcommand{\H}{ \text{-} }
%\newcommand{\Iff}{ \Leftrightarrow }
%\newcommand{\Imp}{ \Rightarrow }
%\newcommand{\SEArrow}{\style{display: inline-block; transform: rotate(45deg)} {\Rightarrow} }
%\newcommand{\NEArrow}{\style{display: inline-block; transform: rotate(-45deg)} {\Rightarrow} }
%\newcommand{\Models}{ \mathrel{|\!\!\models} }
`$
内容：
- コンテキスタッドと特殊ケース達
- 包括圏とテレスコープ構成
- C-システムの特徴付け
- ハイパードクトリンのテレスコープ閉包
- テレスコープ閉包の作り方
- グロタンディーク構成とデカルト圏に関する準備
- ハイパードクトリンのグロタンディーク構成への持ち上げ
- 依存演算の代数系としてのコンテキスタッド
関連記事：
- 依存アクテゴリーが面白い
- 環境付き計算と依存アクテゴリー 1/n
- コンテキスタッドかぁ、ウーム‥‥
- コンテキスタッド、包括圏、ハイパードクトリン （この記事）
- 型理論とコンテキスタッド： コンテキストフル射
- 包括コンテキスタッドに向けて
- 型理論周辺、何で混乱するのか？
- 型理論／論理／インスティチューション理論の引っ越し
コンテキスタッドと特殊ケース達
コンテキスタッド〈contextad〉はある種のモナド（正確にはスード高次モナド）です。モナドなので、台の上に単位と乗法が載った代数構造（モノイド構造）になります。コンテキスタッドの台はスパンです。次の形に書きます。
$`\quad \cat{C}\overset{\pi}{\ot}\cat{E} \overset{\odot}{\to}\cat{C}`$
このスパンは、一般的にはパラダイスと呼ばれる種別の2-圏内に居ますが、ここではパラダイスを $`\mbf{CAT}`$ に固定します。つまり、スパンは圏と関手から構成されるとします。スパンの左脚〈left leg〉には条件が付きますが、ここでの左脚条件は「ファイバー付き圏〈グロタンディーク・ファイブレーション〉だ」という条件にします。右脚は特に条件を付けません。
コンテキスタッドの起源となったスパンの典型事例〈プロトタイプ〉はアクテゴリー〈actegory〉です。右アクテゴリーなら次のようなスパンになります。
$`\quad \cat{C}\overset{\pi_1}{\ot}\cat{C}\times \cat{M} \overset{\odot}{\to}\cat{C} \In \mbf{CAT}`$
ここで、$`\cat{M}`$ は右作用域〈右刺激域〉であるモノイド圏です。$`\pi_1`$ は直積の第一射影関手、$`\odot`$ は右作用双関手です。
$`\cat{C}`$ と $`\cat{M}`$ が一致して、右作用がモノイド積で与えられる場合は、次のスパンになります。モノイド圏の自分自身による右作用です。
$`\quad \cat{C}\overset{\pi_1}{\ot}\cat{C}\times \cat{C} \overset{\otimes}{\to}\cat{C} \In \mbf{CAT}`$
特にモノイド積がデカルト積である場合は：
$`\quad \cat{C}\overset{\pi_1}{\ot}\cat{C}\times \cat{C} \overset{\times}{\to}\cat{C} \In \mbf{CAT}`$
矢印の上に載っている $`\times`$ は双関手〈二項関手〉としてのデカルト積です。$`\cat{C}\times \cat{C}`$ の $`\times`$ は別物で、デカルト圏としての $`\mbf{CAT}`$ が備えるデカルト積です。
「コンテキスタッド → アクテゴリー → モノイド圏 → デカルト圏」という、一般から特殊への系列、逆向きに見れば特殊から一般への系列で物事を考えられるようになったことは、コンテキスタッドのご利益のひとつです。
包括圏とテレスコープ構成
包括圏の構造を図式で描くと次のようになります（「大きい包括クランの3つの例 // 包括構造の定義」参照）。
$`\quad \xymatrix@C+1pc{
{}
&{\cat{C} }
\\
{\cat{E}} \ar[ur]^{\cdot} \ar[dr]_{\pi} \ar[r]^-{\gamma}
&{\mrm{Arr}(\cat{C}) } \ar[u]_{\mrm{Dom}}\ar[d]^{\mrm{Cod}}
\\
{}
&{\cat{C}}
}\\
\quad \text{commutative }\In \mbf{CAT}
`$
2つの三角形は厳密に可換です。
- $`\pi`$ は、ファイバー付き圏〈グロタンディーク・ファイブレーション〉の射影
- $`\cdot`$ （ナカグロ）は、コンテキスト拡張〈context extension〉と呼ばれる演算（双関手）
- $`\mrm{Arr}(\cat{C})`$ は、$`\cat{C}`$ のアロー圏
- $`\mrm{Dom}, \mrm{Cod}`$ は、アロー圏の域関手と余域関手
- $`\gamma`$ は包括関手（包括関手の条件はデカルト関手であること）
ファイバー付き圏のトータル圏 $`\cat{E}`$ の対象は、型理論では依存型と呼びますが、コンテキスト拡張の拡張ステップ〈extension step〉です。コンテキスト拡張演算は、コンテキスト（$`\cat{C}`$ の対象） $`\Gamma`$ と、$`\Gamma`$ 上の拡張ステップ（ファイバー内に居る対象） $`A`$ を受け取って新しいコンテキスト $`\Gamma\cdot A`$ を返します。演算 $`\cdot`$ は、第一引数値に依存して第二引数に許されるモノが決まるという意味で依存二項演算です。
包括圏の構造の一部を取り出すと次のスパンになります。
$`\quad \cat{C} \overset{\pi}{\ot} \cat{E} \overset{\cdot}{\to} \cat{C} \In \mbf{CAT}`$
このスパンを台としてただちにコンテキスタッドが作れるか？ というと、そうはいきません。
コンテキスト $`\Gamma`$ 上のファイバー（局所圏）を拡張する（コンテキスト拡張のことではなくて、日常日本語の「より大きくする」）必要があります。単一の拡張ステップではなくて、拡張ステップを並べたリストを考えるのです。そのようなリストはテレスコープ〈telescope〉と呼びます。テレスコープの作り方は「テレスコープと包括クラン // 包括クランのテレスコープ圏」を見てください。
コンテキスト $`\Gamma`$ 上のテレスコープ $`(A_1, \cdots, A_n)`$ をパルムグレン〈Erik Palmgren〉はブラケットで囲んで $`[A_1, \cdots, A_n]`$ と書いています（「パルムグレンによる、型理論の複前層モデル」参照）。テレスコープは次のように書くことにします。
$`\quad \vec{A} = {_\Gamma}[A_1, \cdots, A_n]`$
単一のステップから、ステップ達のベクトル〈リスト | 並び〉に変更しているので、テレスコープ構成（テレスコープによるファイバーの拡張）をしたスパンを、次のようなベクトル記法（上に矢印乗せる）で書きます。$`\pi`$ も最初と変わってますが同じ文字で書きます（オーバーロード）。
$`\quad \cat{C} \overset{\pi}{\ot} \vec{\cat{E}} \overset{\odot}{\to} \cat{C}`$
$`\odot`$ はテレスコープによるコンテキスト拡張演算であり、次のように定義します。
$`\quad \Gamma\odot [A_1, \cdots, A_n] := (\cdots (\Gamma\cdot A_1)\cdot \cdots)\cdot A_n `$
空テレスコープ $`[ ]`$ によるコンテキスト拡張は何もしません。
$`\quad \Gamma\odot [ ] := \Gamma`$
包括圏にテレスコープ構成を施せば、それからスムーズにコンテキスタッドが作れます。コンテキスタッドの枠組みにより、テレスコープ構成の必要性・必然性が非常に明確になりました。これは素晴らしい。
C-システムの特徴付け
型理論で出てくる様々な圏を、包括圏とテレスコープ構成のなかに埋め込んで考えると、なにかと事情がハッキリします。一例として、ヴォエヴォドスキー〈Vladimir Voevodsky〉のC-システム（カートメル〈John Cartmell〉のコンテキスト圏と同じ、「C-システム、分裂ディスプレイクラス、カートメルツリー構造」参照）を特徴付けてみましょう。
C-システムの定義から、包括圏としてのファイブレーションは離散〈discrete〉かつ分裂的〈split〉です。それだけでなく、C-システムには長さ関数とカートメルツリー構造があります。コンテキストに長さが定義できて、コンテキスト達がツリー構造を持つことを（歴史的経緯から）文脈的〈contextual〉といいます。分かりにくい言葉ですが、こんな呼び名が付いたのは偶発的事情です*1。
テレスコープ構成された包括圏が文脈的であるためには幾つかの条件が必要です。まず、コンテキスト達の圏 $`\cat{C}`$ に終対象が必要です。習慣により、終対象であるコンテキストを空コンテキスト〈empty context〉と呼びます。空コンテキストは $`\diamond`$ と書くことにします（山形括弧の空リスト $`\langle\rangle`$ と似てるから）。
すべてのコンテキストが、空コンテキスト $`\diamond`$ 上のテレスコープから生成されるという条件は、次の写像が全射であることです。
$`\quad \odot_{\diamond} : \vec{\cat{E}}_{\diamond} \to |\cat{C}|`$
ここで、$`\vec{\cat{E}}_{\diamond}`$ は、空コンテキスト $`\diamond`$ 上のファイバー〈局所圏〉です。C-システムは離散ファイブレーションなので、ファイバーは集合〈離散圏〉です。$`\odot_{\diamond}`$ は、コンテキスト拡張演算 $`\odot`$ を $`\diamond`$ 上のファイバーに制限したものです。
上記条件だけだと、コンテキストの長さが定義できません。長さの導入のためには、「クランからC-システム」と同様な議論が必要になります。
コンテキスト $`\Gamma`$ 上のステップ $`A`$ に対して、テレスコープ $`[B, C]`$ があって、
$`\quad \Gamma\odot [A] \cong \Gamma\odot [B, C]`$
ならば、ステップ $`A`$ は $`B`$ と $`C`$ に因子分解されたことになります。このような分解が、それ以上分解できないステップ達の並びとして、本質的に〈up-to-iso で〉一意に出来るなら、コンテキストの長さを定義できます。
拡張ステップと拡張に伴う標準射影は一対一対応するので、標準射影達のクラスが一意分解性を持つことが、長さとツリー構造の定義可能性、つまり文脈性〈contextuality〉の条件となります。
こうしてみると、C-システムの条件が相当に強い条件であることが分かります。応用上は、一部の条件は外したほうがよい場合があるでしょう。例えば、コンテキストの長さが定義できなくても、テレスコープの長さは定義できるので、テレスコープの長さに沿った帰納法は使えます*2 -- それで十分なこともあります。
ハイパードクトリンのテレスコープ閉包
$`\cat{L}`$ は2-圏（1-圏も特殊な2-圏）であり、圏達の2-圏 $`\mbf{CAT}`$ への忠実関手を持つとします。
$`\quad K: \cat{L} \to \mbf{CAT} \In 2\mathbb{CAT}`$
$`K`$ の例として、$`\mbf{Set}`$ の対象を離散圏とみなす関手、$`\mbf{Ord}`$ の対象をやせた圏とみなす関手、$`\mbf{MonCat}`$ の対象（小さなモノイド圏）を単なる圏とみなす関手などがあります。
ハイパードクトリン〈hyperdoctrine〉は、忠実関手 $`K`$ を持つ2-圏 $`\cat{L}`$ を余域〈ターゲット2-圏〉とするインデックス付き圏〈indexed category〉$`P`$ です。ハイパードクトリンのキモは限量子なのですが、今回は限量子には注目しないで、インデックス付き圏 $`P`$ だけに注目します。（限量子の話は「述語論理： ハイパードクトリンとパルムクイスト二重圏」に書いています。）
$`\quad P: \cat{C}^\op \to \cat{L} \In 2\mathbb{CAT}`$
2-圏 $`\cat{L}`$ が1-圏に退化していて、サイズもあまり大きくないなら、次のようにみなすことが出来ます。
$`\quad P: \cat{C}^\op \to \cat{L} \In \mbf{CAT}`$
$`P`$ が反変関手であることは次のようにも書けます。
$`\quad P: \cat{C} \to \cat{L}^\op \In \mbf{CAT}`$
$`X\in |\cat{C}|`$ に対する $`P(X)`$ は、論域〈domain of discourse〉$`X`$ 上の述語達が形成する論理的代数構造だとみなします。典型的具体例は：
$`\text{For }X\in |\mbf{Set}|\\
\quad P(X) := \mrm{Map}(X, \{0, 1\})
`$
ここで、$`\{0, 1\}`$ は、ブール代数構造を備えた古典二値ブール代数とみなします。$`\mrm{Map}(X, \{0, 1\})`$ のブール代数構造は、ベキ集合 $`\mrm{Pow}(X)`$ のブール代数構造と同じです。
論理的代数構造（典型例はブール代数）達の圏である $`\cat{L}`$ の選び方は色々ありますが、ここでは小さいデカルト圏*3（デカルト・モノイド圏）達の1-圏だとします（2-圏だと話が面倒になるので）。$`\cat{L}`$ が1-圏であっても、その対象が圏であることには注意してください。
ここで扱うハイパードクトリンの構成素を確認すると：
- $`\cat{L}`$ は、小さいデカルト圏達の1-圏（自然変換は考えない）
- $`K:\cat{L}\to \mbf{CAT}`$ は、デカルト・モノイド構造を忘れる忘却関手
- $`\cat{C}`$ は、任意の圏でよい（特に具体化はしない）。具体的に考えたいなら、$`\cat{C} = \mbf{Set}`$ としてもよい。
- $`P:\cat{C}^\op \to \cat{L}`$ は反変関手。ハイパードクトリンの条件から任意ではあり得ないが、ハイパードクトリンの条件は今は気にしなくてよい。単なる反変関手だと思ってよい。
- $`\cat{C}`$ の対象は、型理論の言葉では「コンテキスト」、述語論理の言葉では「論域〈domain of discourse〉」。
- デカルト圏 $`P(X)`$ の対象は、述語論理の言葉では「命題」、意味論的に考えれば「述語」。
- デカルト圏 $`P(X)`$ の射は、述語論理の言葉では「証明」。
ハイパードクトリンをコンテキスタッドの枠組みに載せるには、事前に、テレスコープ構成と類似の加工を施します。述語（$`\cat{L}`$ の対象であるデカルト圏の対象）のリスト $`(p_1, \cdots, p_n)`$ に意味を持たせ、論域を述語のリストで拡張することを可能とします。新しい言葉を作るのは避けて、述語のリストのこともテレスコープ〈telescope〉と呼ぶことにします。
もとの圏 $`\cat{C}`$ の対象だけではなくて、すべてのテレスコープ達も対象として組み入れた圏を構成します。そのようにして作った圏を（ハイパードクトリン $`(\cat{C}, P)`$ の）テレスコープ閉包〈telescope closure〉と呼ぶことにします。テレスコープ閉包の作り方の全体像を次節で述べます。
テレスコープ閉包の作り方
ハイパードクトリンのテレスコープ閉包は、よく知られている手法を組み合わせれば構成できます。とはいえ、相当にめんどくさい。動機がなければ、こんなことしようとは思わないでしょう。「コンテキスタッドにフィットさせよう」、「テレスコープ構成の類似物を作ろう」としたからやってみたわけで、動機を提供してくれた事はコンテキスタッドの恩恵です。
さて、テレスコープ閉包を作るにはまず、$`C_0 := \cat{C}`$、$`P_0 := P`$ と置いて、以下のような梯子状の系列を構成します。可換図式ではないので注意してください。$`\cat{L}`$ 側に $`{}^\op`$ を付けているのは気分だけの問題で特に意味はないです。
$`\quad \xymatrix{
{\cat{C}_0} \ar[d]^{P_0}
& {\cat{C}_1} \ar[l]_{\rho_1} \ar[d]^{P_1}
& {\cat{C}_2} \ar[l]_{\rho_2} \ar[d]^{P_2}
& {\cdots} \ar[l]_{\rho_3}
\\
{\cat{L}^\op}
& {\cat{L}^\op} \ar@{=}[l]
& {\cat{L}^\op} \ar@{=}[l]
& {\cdots} \ar@{=}[l]
}\\
\quad \In \mbf{CAT}
`$
圏 $`C_1`$ は、$`C_1 := \int(C_0 \mid P_0)`$ というグロタンディーク構成で、$`\rho_1`$ はグロタンディーク構成の標準射影です。他の部分も同じで、次の関係があります。
$`\quad C_{k + 1} = \int(C_k \mid P_k)`$
$`\quad \rho_{k + 1} : \int(C_k \mid P_k) \to \cat{C}_k\In \mbf{CAT}`$
$`P_0`$ を $`P_1`$ に持ち上げるのが面倒です。ただし、まったく同じ方法で $`P_k`$ を $`P_{k +1}`$ に持ち上げることができます。つまり、$`P_0`$ を $`P_1`$ に持ち上げる手順が全体の要〈かなめ〉です。
上記の梯子状の図式の極限を取ると、それがハイパードクトリン $`P:\cat{C}\to\cat{L}^\op`$ のテレスコープ閉包 $`\widetilde{\cat{C}}`$ を与えます。極限対象（極限錐の頂点） $`\widetilde{\cat{C}}`$ から $`\cat{L}^\op`$ への射影（極限錐の成分射）が、$`\widetilde{\cat{C}}`$ 上のハイパードクトリン構造を与えます。
$`P_0`$ を $`P_1`$ に持ち上げるとき、デカルト圏特有のコモノイド構造を使うので、ハイパードクトリンが値を取る圏（または2-圏）はデカルト圏達の圏であることが必要なことが分かります。テレスコープ閉包を述語論理の文脈で考えてみると、公理系の拡張（コンテキスト拡張と同じ）や、公理系を前提（あるいは環境）とした推論・証明を記述していることになり、論理としてオーガニックな*4意味論を持つことが分かります。
$`P_0`$ から $`P_1`$ への持ち上げは次々節で定義します。そのための準備を次節で行います。
グロタンディーク構成とデカルト圏に関する準備
$`P : \cat{C}\to \cat{L}^\op`$ として、インデックス付き圏 $`P`$ のグロタンディーク構成を $`\cat{D}`$ とします。
$`\quad \cat{D} := \int(\cat{C} \mid P)`$
$`P`$ の $`\cat{D}`$ への持ち上げを $`Q`$ と置いて、次節で $`Q`$ を定義します。
$`\quad Q : \cat{D} \to \cat{L}^\op \In \mbf{CAT}`$
$`Q`$ を $`P`$ に基づいて定義するので、$`P \mapsto Q`$ という対応（構成法）を記述することになります。
構成はちょっとややこしくなるので、簡略な記法の準備をしましょう。関手 $`F`$ の対象パートと射パートを以下のように書くことにします。
$`\text{For }F :\cat{A} \to \cat{B} \In \mbf{CAT}\\
\quad |F| := F_\mrm{obj} : |\cat{A}| \to |\cat{B}| \In \mbf{SET}\\
\quad \o{F} := F_\mrm{mor} : \o{\cat{A}} \to \o{\cat{B}} \In \mbf{SET}\\
\text{Where}\\
\quad \o{\cat{A}} := \mrm{Mor}(\cat{A})\\
\quad \o{\cat{B}} := \mrm{Mor}(\cat{B})
`$
圏も関手も一律の記法でパートを取り出します。最初は違和感があるかも知れませんが、慣れると便利な記法です。絶対値記号（縦棒囲み）と上線は関手になります。
$`\quad |\hyp| : \mbf{CAT} \to \mbf{SET} \In 2\mathbb{CAT}\\
\quad \o{\hyp} : \mbf{CAT} \to \mbf{SET} \In 2\mathbb{CAT}
`$
対象パートと射パートに同じ名前を使う（オーバーロード）記法を禁止しているわけではありません。対象パート／射パートを区別したほうがよいときに絶対値記号と上線を使います。
出てくる概念的事物の種類を区別するために、使用するフォントや略記に関して次の約束をします。
- $`\cat{L}`$ の対象であるデカルト圏は $`A, B`$ など。カリグラフィー体ではなくてイタリック体なので注意。
- $`\cat{L}`$ の対象（$`A, B`$ など）は圏なので、その対象（述語相当）を $`p, q, r, s`$ など。
- $`\cat{L}`$ の対象（$`A, B`$ など）は圏なので、その射（証明相当）を $`\phi, \psi`$ など。
- $`\cat{L}`$ の対象（$`A, B`$ など）であるデカルト圏のデカルト積は $`\land`$ と書く。連言〈論理AND〉を想定している。
- $`\cat{L}`$ の対象（$`A, B`$ など）であるデカルト圏の終対象兼モノイド単位対象は $`\mbf{t}`$ と書く。論理的真〈True〉を想定している。
- $`\cat{L}`$ の対象（$`A, B`$ など）であるデカルト圏の射は、$`\phi: p \lto q \In A`$ と書く。射は論理的証明を想定しているので不等号っぽい $`\lto`$ を使う。ターンスタイル記号 $`\vdash`$ は型理論と激しくコンフリクト〈かち合い〉するので使わない*5。
- 圏 $`\cat{C}`$ の対象と射は $`f:X \to Y \In \cat{C}`$ のように書く。
- インデックス付き圏 $`P`$ による $`f`$ の値である関手〈リダクト関手 | 水増し〉$`P(f)`$ を $`f^*`$ と略記する。反変関手の値を上付きアスタリスクは比較的よく使われる略記。
- グロタンディーク構成（の結果） $`\cat{D} = \int(\cat{C}\mid P)`$ の対象は $`(X, p)`$ のように書く。$`X\in |\cat{C}|, p\in |P(X)|`$ である依存ペアである。
- グロタンディーク構成（の結果） $`\cat{D} = \int(\cat{C}\mid P)`$ の射は $`F = (\u{F}, F^\#)`$ のように書く。$`\u{F}`$ は $`F`$ のベースパート、$`F^\#`$ は $`F`$ のファイバーパート。グロタンディーク構成した圏〈平坦化圏〉の射は、必ずベースパートとファイバーパートを持つ。
- さらに、ベースパート $`\u{F}`$ を $`f`$ （対応する小文字）と略記して、$`F = (f,F^\#)`$ とする。
$`\cat{L}`$ の対象であるデカルト圏 $`A`$ とその対象 $`p\in |A|`$ に対して、新しいデカルト圏 $`A_{(p\land)}`$ を構成できます。これについては、「環境付き計算と依存アクテゴリー 1/n // 環境付き計算のインデックス付き圏」を読んでください。ごく簡単に定義を復習すると：
- 対象： $`|A_{(p\land)}| := |A|`$ （対象達の集合は同じ）
- ホムセット： $`\text{For }r, s\in |A|`$
$`A_{(p\land)}(r, s) := A(p\land r, s)`$
圏 $`A_{p\land}`$ は、$`p`$ を前提（あるいは環境）とする証明を射とする圏です。
ハイパードクトリンのグロタンディーク構成への持ち上げ
では、$`Q:\cat{D} \to \cat{L}`$ を構成します。
Q の対象パート
まずは、対象パートからです。
$`\quad |Q| : |\cat{D}| \to |\cat{L}| \In \mbf{Set}`$
定義は以下のとおり。
$`\text{For }(X, p) \in |\cat{D}|\\
\quad |Q| ( (X, p) ) := {|P|(X)}_{(p\land)}
`$
$`|P|(X)`$ はデカルト圏（$`\cat{L}`$ の対象）なので、$`{|P|(X)}_{(p\land)}`$ は前節で述べたような意味（「環境付き計算と依存アクテゴリー 1/n // 環境付き計算のインデックス付き圏」参照）を持ちます。事前に $`P`$ が与えられていれば、$`|Q|`$ は構成可能です。このとき、デカルト圏の一般論は（圏 $`\cat{L}`$ 内での作業のために）使います。
Q の射パート
次に、$`Q`$ の射パートです。
$`\quad \o{Q} : \o{\cat{D}} \to \o{\cat{L}} \In \mbf{Set}`$
$`\o{\cat{D}}`$ の要素、つまり射 $`F:(X, p) \to (Y, q)\In \cat{D}`$ に対して、$`\o{Q}(F)`$ は次のように宣言（定義ではない）できます。
$`\text{For }F: (X, p)\to (Y, q) \In \cat{D} = \int(\cat{C} \mid P)\\
\quad \o{Q}(F) : |Q|( (Y, q) ) \to |Q|( (X, p)) \In \cat{L}
`$
$`|Q|`$ の定義から、この宣言は以下のように書けます。
$`\quad \o{Q}(F) : |P|(Y)_{(q\land) } \to |P|(X)_{(p\land)} \In \cat{L}
`$
$`\cat{L}`$ の射 $`\o{Q}(F)`$ が、圏 $`|P|(Y)_{(q\land) }`$ から圏 $`|P|(X)_{(p\land)}`$ への関手なので、さらに対象パートと射パートに分ける必要があります。
Q の射パートの対象パート
関手 $`\o{Q}(F)`$ の対象パートは次のように宣言できます。
$`\quad |\o{Q}(F)| : | |P|(Y)_{(q\land) }| \to | |P|(X)_{(p\land)}| \In \mbf{Set}
`$
$`Q`$ の射パート（の値）の対象パート $`|\o{Q}(F)|`$ の定義は以下のとおり。
$`\text{For }r \in | |P|(Y)_{(q\land) }|\\
\quad |\o{Q}(F)|(r) := f^*(r)
`$
ここで、$`f^*`$ はリダクト関手 $`P(f)`$ の略記でした。$`f`$ は $`\cat{D} = \int(\cat{C} | P)`$ の射 $`F`$ のベースパート $`\u{F}`$ の略記でした。よって、略記を用いずに定義を書けば：
$`\quad |\o{Q}(F)|(r) := P(\u{F})(r)`$
これは、$`P`$ が与えられていれば、任意の $`F`$ に対して構成可能です。$`|\o{Q}(F)| := P(\u{F})`$ とも書けます。
Q の射パートの射パート
関手 $`\o{Q}(F)`$ の射パートは次のように宣言できます。
$`\quad \o{\o{Q}(F)} : \o{|P|(Y)_{(q\land) }} \to \o{ |P|(X)_{(p\land})} \In \mbf{Set}
`$
$`\phi \in \o{|P|(Y)_{(q\land) }}`$ に対して、$`\o{\o{Q}(F)}(\phi)`$ を定義すればよいことになります。$`\phi`$ は次の形です。
$`\quad \phi : r \to s \In {|P|(Y)}_{(q\land)}`$
これは、$`{|P|(Y)}_{(q\land)}`$ の定義から、次のようになります。
$`\quad \phi : q\land r \to s \In {|P|(Y)}`$
したがって、$`\phi\in {|P|(Y)}(q\land r, s)`$ に対して $`\o{\o{Q}(F)}(\phi)`$ を定義すればいいのです。
$`F`$ から誘導されるリダクト関手 $`f^* = P(\u{F}) = |\o{Q}(F)|`$ を $`\phi`$ に適用すると：
$`\quad f^*(\phi) : f^*(q\land r ) \to f^*(s) \In |P|(X)`$
デカルト圏のあいだのリダクト関手 $`f^*`$ は、デカルト構造を厳密に保存するとして、次が得られます。
$`\quad f^*(\phi) : f^*(q)\land f^*(r ) \to f^*(s) \In |P|(X)`$
一方、$`\cat{D}`$ の射 $`F:(X, p) \to (Y, q)\In \cat{D}`$ のファイバーパートは次のようです。
$`\quad F^\# : p \to f^*(q) \In \cat{D}_X`$
ここで、$`\cat{D}_X`$ は、$`X\in \cat{C}`$ 上のファイバー〈局所圏〉です。
これらを使って、$`\o{\o{Q}(F)}(\phi)`$ を以下のように定義します。
$`\quad \o{\o{Q}(F)}(\phi) := (F^\# \land \id_{f^*(r)}); f^*(\phi) \;:p\land f^*(r) \to f^*(s) \In |P|(X)`$
これは、$`P`$ が与えられていれば、任意の $`F`$ と $`\phi`$ に対して構成可能です。
残っている作業
$`Q`$ の射パートの値 $`\o{Q}(F)`$ は、$`\cat{L}`$ の射、つまり関手です。任意の $`\cat{D}`$ の射 $`F`$ に対して、$`\o{Q}(F)`$ の関手性を示す必要があります。
$`Q`$ の射パート $`\o{Q}`$ と対象パート $`|Q|`$ を一緒にした $`Q`$ は、圏 $`\cat{D}`$ から圏 $`\cat{L}`$ の反変関手である必要があります。$`Q`$ の反変関手性を示す必要があります。
これらを示すと、$`Q : \cat{D} \to \cat{L}^\op\In \mbf{CAT}`$ であることがわかり、$`P`$ を与えられて、グロタンディーク構成 $`\cat{D} = \int(\cat{C}\mid P)`$ への持ち上げ手順が完成します。
持ち上げ手順には、グロタンディーク構成とデカルト圏の一般論しか使ってないので、$`\cat{C}, P`$ が何であっても汎用的に使えます。したがって、梯子状の無限な持ち上げ系列を作れます。無限な持ち上げ系列の極限がテレスコープ閉包でした。
与えられたハイパードクトリン $`(\cat{C}, P)`$ から、そのテレスコープ閉包が構成できれば、包括圏とコンテキスタッドの枠組みにフィットさせるのは（比較的に）容易です。
コンテキスタッドから離れて、ハイパードクトリンのテレスコープ閉包だけを考えてみても、これは述語論理の構成として素直に解釈できます。ハイパードクトリンのベース圏（型理論の言葉ではコンテキストの圏）に対してもテレスコープを考えることができて、これも、型理論的／述語論理的、そしてデータベース的に自然な解釈が出来ます。
依存演算の代数系としてのコンテキスタッド
包括圏をコンテキスタッドの枠組みにフィットさせるときも、ハイパードクトリンをコンテキスタッドの枠組みにフィットさせるときも、テレスコープを使いました。テレスコープとは、型理論や論理の文脈で使われる依存リストのことです。依存リストの連接（依存連接）がコンテキスタッドの乗法を与え、依存空リストがコンテキスタッドの単位になります。
コンテキスタッドの出自が依存アクテゴリーであったことを思い起こせば、コンテキスタッドが依存性を持つ二項演算の定式化であることは推察できます。依存性を持たない二項演算の定式化はモノイドでした。コンテキスタッドは、モノイド構造に依存性を入れて、極度に一般化・抽象化した代数系と捉えられます。
モノイドの典型例は、(リスト, 連接, 空リスト) からなる自由モノイドです。おそらく、コンテキスタッドの典型例は、(依存リスト, 依存連接, 依存空リスト) からなる自由コンテキスタッドなのでしょう。自由リストは集合から生成されました。自由コンテキスタッドの生成系はずっと複雑な構造のはずです。
包括圏やハイパードクトリンにテレスコープ構成をしたらコンテキスタッドになった、ということは、包括圏やハイパードクトリンはコンテキスタッドの生成系の事例なのでしょう。一般的に、コンテキスタッドの生成系とは何であるか？ 今のところサッパリ分かりません。が、何らかの生成系が与えられたとき、テレスコープ構成により依存リストを飽和するまで付け足せば、それが自由コンテキスタッドになるだろう、とは予測できます。
コンテキスタッドは抽象的で複雑な構造ですが、依存演算を持つモノイド類似代数系を定式化するには、こういう形にならざるを得なかった、という気もします。依存性とはそれほどに難しい概念なのです。
