…旧） 環境付き計算のインデックス付き圏 グロタンディーク構成とファイブレーション 依存アクテゴリー モノイド法則 環境付き計算ペアのミックス操作 ベース射の自明持ち上げ 自明持ち上げの法則 2-圏内のスパンのあいだの射 関連記事： 環境付き計算と依存アクテゴリー 1/n （この記事） 環境付き計算と依存アクテゴリー 2/n 環境付き計算と依存アクテゴリー 3/n 環境付き計算（懐旧）入力の型 $`A`$ と出力の型 $`B`$ 以外に、状態の型 $`S`$ を持った計算は、次…

…： 随伴系の圏の上のインデックス付き圏として (2022年) 「最近のモナド論の概観と注意事項 1/2」で紹介した文献をひとつだけ再掲しておきます。バスケス-マルケスの次の論文です。 [Vaz15-17] Title: Monad and Comonad Objects through 2-adjunctions of the type Adj-Mnd Submitted: 15 Oct 2015 (v1), 8 Jun 2017 (v3) Author: Adrian Va…

…拡張包括構造を持ったインデックス付き圏」で概要を述べた包括圏〈comprehension category〉が、依存アクテゴリーの事例になりそうです。 「最近の型理論： 拡張包括構造を持ったインデックス付き圏」は、バート・ジェイコブス〈Bart Jacobs〉の包括圏〈comprehension category〉というより、ファミリー付き圏と局所デカルト閉圏を若干抽象化した圏を想定して書いていたようです。 型理論では、型の意味論としてファミリー付き圏〈CwF | categ…

…スについては、「2階インデックス付き圏と反ラックス余錐」で述べたように： この呼び名は、どちらかの方向をラックスと決めたら、もう一方を反ラックス（あるいは余ラックス）と呼ぶだけで、逆の呼び名もありえます。また、ラックスと反ラックスを区別しないこともあります。 要はお約束の問題です。一般的・統一的ルールは無理なので、その場その場でどっちがラックスかを決めることにします。アナロジー集合〈0-圏〉上の構造と圏〈1-圏〉上の構造では、文字通り“次元が違います”。0次元ベースの構造と1…

…題があります。「2階インデックス付き圏と反ラックス余錐」から： この呼び名は、どちらかの方向をラックスと決めたら、もう一方を反ラックス（あるいは余ラックス）と呼ぶだけで、逆の呼び名もありえます。また、ラックスと反ラックスを区別しないこともあります。 形容詞「反ラックス」は取り去って、ここでは単に依存アクテゴリー〈dependent actegory〉と呼びます。カプチ／マイヤースは、依存アクテゴリーと一般化Para構成〈generalized Para constructio…

…^\hyp)`$ はインデックス付き圏〈indexed category〉となります。これは、単純ファミリー構成を $`|\cat{S}|`$ に制限しただけではなくて、$`\cat{S}`$ の（恒等射以外の）射に対応するファミリー射まで定義しています。さらに、インデックス付き圏 $`(\cat{S}^\hyp)`$ に対するグロタンディーク構成を施します。これが $`\cat{S}`$ の（大域的な）ファミリー構成です。$`\quad \mrm{Fam}^\cat{S}(…

…要素の圏 同語反復余インデックス付き圏のグロタンディーク構成 スライシング関手 スライス圏$`\cat{C}`$ は小さい圏とします。$`\cat{C}`$ の対象は、ラテン文字小文字の最初のほう $`a, b, \cdots`$ で表します。$`\cat{C}`$ の射は、ラテン文字小文字の中間あたりの $`f, g, \cdots`$ で表します。$`\cat{C}`$ の対象 $`c\in |\cat{C}|`$ に対して、スライス圏〈slice category | …

…密〈strict〉なインデックス付き圏〈indexed category〉達の圏を表します。それに対して弱い〈weak〉インデックス付き圏達の2-圏は次のように書けます。$`\quad [\cat{C}^\mrm{op}, {\bf CAT}]_2 := 2{\bf CAT}(\dimU{\cat{C}^\mrm{op}}{2}, \dimU{\bf CAT}{2}) = 2{\bf CAT}(\mrm{Disc2}(\cat{C}^\mrm{op}), \bf CAT)`$…

14年近く前の記事「インデックス付き圏のインデックス付き圏」において、インデックス付き圏達が形成する圏が再びインデックス付き圏の構造を持つことを書いています。しかし、インデックス付き圏達のインデックス付き圏へのインデックス付き圏をハッキリと定義することは出来ませんでした。最近、反ラックス余錐を使うと、インデックス付き圏達のインデックス付き圏へのインデックス付き圏の明瞭な定式化が得られることが分かりました。$`\newcommand{\mrm}[1]{ \mathrm{#1} …

…に説明があります。 インデックス付き圏のグロタンディーク構成 グロタンディーク構成と積分記号 プロ関手 $`P`$ の場合は、状態空間であるインデックス付き集合のインデキシング集合は次の形になります。$`\quad |\cat{C}^\op\times \cat{D}| = |\cat{C}^\op| \times |\cat{D}|`$もう、気分を出す必要はないでしょうから、$`|\cat{C}^\op| \times |\cat{D}|`$ のまま使います。インデックスは…

…u{S}}`$ 上のインデックス付き圏（実体は反変関手）です。インデックス付き圏にグロタンディーク構成をほどこすと平坦化圏ができます。それがDiag構成の結果〈成果物〉です。$`\quad \doct{D}\text{-}\mrm{Diag}^\cat{S}(\cat{D}) := \Int{\u{\cat{S}}} \doct{D}\text{-}\mrm{Diag}^\cat{S}[\hyp](\cat{D}) \;\in |{\bf CAT}| `$グロタンディーク構成…

…ct{S}`$ 上のインデックス付き圏〈indexed category〉になります。Diag構成ときに関手のことを図式と呼び、関手圏を図式の圏と呼びます。この節での「図式〈diagram〉」は関手の意味です。$`\doct{D}, \doct{S}`$ は前節と同じで、ドクトリンとその部分1-圏だとします。ドクトリン $`\doct{D}`$ は了解されている（文脈で前提している）として明示しないこともあります。2-圏 $`\doct{D}, {\bf CAT}`$ の2-…

…ン拡張とラムダ計算 インデックス付き圏として 関連する関手・自然変換の名前 右カン拡張とラムダ計算まず、さすがに次は忘れない。 $`\mrm{Left}`$ $`\mrm{Center}`$ $`\mrm{Right}`$ KanのKを L, C, R に置き換えて、取り除いたKを下付きにすると： $`\mrm{Lan}_K`$ $`\mrm{Can}_K`$ $`\mrm{Ran}_K`$ Kは形状関手（後述）の「ケ」とも憶えられます。$`\mrm{Can}_K`$ は、関…

…。前層の要素の圏は、インデックス付き圏のグロタンディーク構成〈Grothendieck construction for indexed category〉の特殊ケースです。前層 $`F`$ の要素の圏を $`\mrm{El}(F)`$ と書きます。圏 $`\mrm{El}(F)`$ の対象の集合は、次の集合論的シグマ型で与えます。$`\quad |\mrm{El}(F)| := \sum_{X\in |\cat{C}|} F(X)`$要するに、$`F(X)`$ 達をすべて寄…

…m〉ですが、これは余インデックス付き圏／インデックス付き圏のトータル圏（「最近の型理論： 拡張包括構造を持ったインデックス付き圏」の最初の節参照）の対象・射・等式の描画に有効です。この記事で描画法をもう少し説明します。一般的な余インデックス付き圏／インデックス付き圏を相手にするのは複雑なので、ベース圏〈インデキシング圏〉が順序集合の場合に限ります（ロブスキ／ザンサイ〈Leo Lobski, Fabio Zanasi〉論文もそのようなケースを扱っています）。また、局所圏〈ファイ…

…側だけを切り出すと、インデックス付き圏〈indexed category〉です。ただし、最初に余インデックス付き圏（共変関手）を出して、後からインデックス付き圏〈反変関手〉を追加する構成になっています。反変・共変の別で混乱しがちなので、そこを先に片付けておきましょう。明示的に次の反変関手を使います。$`\quad \mrm{Rev}_\cat{C} : \cat{C} \to \cat{C}^\mrm{op}`$ （反変関手）任意の反変関手 $`G`$ は、この反変関手（裏返…

…圏に共通する構造を、インデックス付き圏として定式化できます。ファミリー付き圏は拡張包括構造〈extension-comprehension structure〉を持ちますから、インデックス付き圏に対しても拡張包括構造を考えることにします。$`\newcommand{\dimU}[2]{{#1}\!\updownarrow^{#2}} \newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \ne…

…を見ると、2-前層はインデックス付き圏〈indexed category〉の別名のようです。インデックス付き圏の定義 https://ncatlab.org/nlab/show/indexed+category を参照すると、2-圏である $`{\bf Cat}`$ を余域とする反変2-関手を2-前層と呼んでいます。ということは、単なる前層は1-前層ということになります。1-前層と2-前層の定義に倣って、n-前層は、n-圏である $`(n - 1){\bf Cat}`$ を余…

…もよい）、次のようなインデックス付き圏 $`\cat{P}`$ を作ります。$`\quad \cat{P}[\hyp] := {\bf CAT}(\J(\hyp), \cat{C})\;\in |{\bf CAT}|`$$`\cat{P}`$ は $`\cat{C}, \cat{D}`$ から決まるので、必要があれば次のように書きます。$`\quad \cat{P} = \cat{P}_\cat{C}^\cat{D}`$$`\cat{P}`$ を定義するために出てきた $`\…

…ング構成 デカルト・インデックス付き圏の変形 1 デカルト・インデックス付き圏の変形 2 意味的シーケントの意味 シリーズ・ハブ記事： 最近の型理論： 宇宙と世界、そして銀河 基本概念「依存型理論で述語論理が出来てしまう理由」で導入した概念を手短に復習します。記号 $`U, \cat{C}, \cat{D}, \cat{P}`$ は、次のような意味だとします。 $`U`$ ： グロタンディーク宇宙。$`{\bf Set}, {\bf SET}, {\bf Cat}, {\bf…

…完備性 ファミリーのインデックス付き圏 射影と随伴トリプル系 おわりに シリーズ・ハブ記事： 最近の型理論： 宇宙と世界、そして銀河 はじめに「階層化された宇宙達を備えた型理論」のヨーガ〈基本教義〉は、 型は宇宙の要素である です。が、「宇宙より銀河」（「最近の型理論： 型理論の構文論と意味論」参照）というキャッチフレーズにより、我々は以下の解釈を採用します。 型は銀河（という圏）の対象である 銀河はデカルト閉圏だとすれば、単純型理論〈simple type theory〉や…

…合圏をベース圏とするインデックス付き圏〈indexed category〉になります。インデックス付き圏はグロタンディーク構成ができます。インデックス付き圏のグロタンディーク構成については過去にだいぶ書いています。 「グロタンディーク構成」のブログ内検索 2つだけ記事を挙げるならば： インデックス付き圏のグロタンディーク構成 グロタンディーク構成と積分記号 インデックス付き圏 $`{\bf Fam}[\hyp](\cat{D})`$ の標準的なグロタンディーク構成は次のように…

…拡張包括構造を持ったインデックス付き圏 関連記事： 射ファミリーと圏論的コンビネータ 圏の束構造と包含的圏 一般化されたファミリーの圏 自然言語混じり形式証明の意味論と最近の型理論 宇宙と世界語感としては、世界より宇宙のほうが広い感じがしますが、ここでは、世界は宇宙（と後述の銀河）の集まりだとします。$`\mathscr{W}`$ がひとつの世界〈a world〉だとすると、世界 $`\mathscr{W}`$ のなかにはたくさんの宇宙が入っています。宇宙のなかでも特に重要な…

…論理代数を対応させるインデックス付き圏 $`\cat{P}:\cat{C} \to {\bf Cat}`$ からなります。その他の構成素もありますし、色々な条件が付きますが、主役は $`\cat{P}:\cat{C} \to {\bf Cat}`$ です。二重圏的ハイパードクトリン〈double categorical hyperdoctrine〉とは、ハイパードクトリンにおける主役を置き換える試みです。二重圏 $`\cat{D}`$ を構成し、二重圏からの2つの二重関手$`…

…のです。 述語論理とインデックス付き圏と限量随伴性 順序集合のカン拡張と特徴述語論理 $`\cat{C}`$ をハイパードクトリンのベース圏とします。通常、$`\cat{C}`$ はデカルト圏であると仮定します。つまり、$`\cat{C}`$ は直積と始対象を持ちます。直積の第一射影 $`\pi_1`$ を単に $`\pi`$ と書くことにします。$`\quad \pi_{X, Y}: X\times Y \to X \In \cat{C}`$この射影ごとに述語論理のモデルが…

…合の総和）の代わりにインデックス付き圏のグロタンディーク構成を使います。2-コンテナ〈2-container〉とは次の形の2-関手だとします。$`\quad \cat{A} :\cat{I}\!\uparrow_2 \to {\bf CAT} \In \mathbb{2CAT}`$ここで、$`\cat{I}\!\uparrow_2`$ は、圏 $`\cat{I}`$ を2-離散2-圏（すべての2-射は恒等射）とみなした2-圏です。$`\cat{A}`$ は、とても大きい2-圏…

…category〉とインデックス付き圏〈indexed category〉のあいだのグロタンディーク同型になります。「依存集合←→ファミリー」の対応は、グロタンディーク同型の0次元バージョンと言えます。依存カリー同型依存カリー同型の主張を先に書いてしまうと：$`\quad {\bf DepSet}[I](X \rtimes I, \sum_I F) \cong {\bf Set}(X, \prod_I F)`$$`\sum_I, \prod_I`$ は、シグマ型構成とパイ型構…

…f Cat}`$ はインデックス付き圏〈indexed category〉になります。必要があれば、インデックス付き圏に関する技法、例えばグロタンディーク構成（「 インデックス付き圏のグロタンディーク構成 」参照）を使うことが出来ます。グロタンディーク構成を通じて、ハイパードクトリンをファイバー付き圏〈{fibred | fibered} category〉とみなすと、ベースの対象 $`X`$ 上の論理代数 $`\mrm{Pred}[X]`$ はファイバーになります。なので、…

…圏を対応させる関手＝インデックス付き圏の話をします。これは、10年近く前2012年4月の記事「またインデックス付き圏が出てきたけど、これはどうなっている？」のコメント欄でksさんに教えていただいたことをまとめたレポートです。とても遅れたレポートです。ksさん、その節はありがとうございました。内容： 概要 セットアップ 随伴系の圏 随伴系の圏上のEnd関手 厳密モノイド圏の内部モノイドとMon関手 モノイド／モナドの保存 モナドのインデックス付き圏の構成 概要10年前の過去記事…

…ory〉と呼ばれます。最近、アクテゴリー〈加群圏〉の需要(?)が増しているようですが、定義や記述が整理されてません。ゴチャゴチャしてしまう理由のひとつは、台〈underlying thing〉を2つ持つ複合構造だからでしょう。パート抽出関手で台を分離すれば情勢は見えやすくなると思います。今日はパート抽出関手を導入しただけで、アクテゴリー〈加群圏〉の定義と記述はまたいずれ。 *1:ちゃんと記述するなら、体の圏上で定義されたインデックス付き圏とそのグロタンディーク構成を使います。