…utom`$ は、双インデックス付き圏〈biindexed category〉に、結合と恒等〈composition and identity〉を載せた構造になるでしょう。 [/追記]圏 $`\HoareAutom`$ に定義を追加してリッチな構造を持たせることが出来ます。2つのモノイド積〈monoidal product〉 $`\boxtimes, \boxplus`$ を導入できます。これらのモノイド積は、集合圏の直積と直和、あるいは論理のANDとORに似たものです。また…

…ので、$`G`$ はインデックス付き圏とみなせます。インデックス付き圏としての $`G`$ にグロタンディーク構成を施せるので、それを $`\int G = \int_{\mbf{ss}} G`$ と書きます。前層に対するグロタンディーク構成（の結果）を特に要素の圏〈category of elements〉とも呼び、$`\mrm{el}(G)`$ とも書きます。グロタンディーク構成は、次のファイバー付き圏〈fibered category | グロタンディーク・ファイブレー…

… クラン／コクラン インデックス付き圏（宣言関手） 包括自然変換 拡張作用と厳密単位 インスタンス＝ハープーン射 包括圏の使い方 包括圏と反包括圏包括圏〈comprehension category〉は次の図式で記述できます。$`\quad \xymatrix{ {\cat{C}} \ar@{=}[r] &{\cat{C}} \\ {\cat{E}} \ar[r]^\rho \ar[d]_\pi \ar[u]^\alpha &{\mrm{Arr}(\cat{C}) } \ar…

…。前層 $`X`$ ごとにファイバー付き圏が構成できます。オーバー圏 $`\cat{C}/X`$ もファイバー付き圏 $`\int_\cat{C}X`$ も、前層 $`X`$ をパラメータに持ちます。つまり、どちらも前層達の圏 $`\cat{C}^\wedge`$ 上のインデックス付き圏とみなせます。このインデックス付き圏達は、もとのコンマ圏や要素の圏より上位レベルに居る構造達です。コンマ圏と要素の圏の対応がハッキリすれば、上位レベルの構造を調べることも出来るようになります。

インデックス付き圏〈indexed category〉の一般化として、インデックス付きn-圏を定義します。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mbf}[1]{\mathbf{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\msc}[1]{\mathscr{#1}} %\newcommand{\msf}[1]{\mathsf{#1}} \newcommand{…

…圏のファミリーとは、インデックス付き圏〈indexed category〉 バンドルとファミリーは互いに対応します（「バンドル-ファミリー対応 再考」参照）。バンドルに対するファミリー$`a: A \to B`$ が集合のバンドルのとき、$`a`$ に対するファミリーは $`a^{-1}`$ と書くことにします。$`\quad a^{-1} : B \to |\mbf{Set}| \In \mbf{SET}`$ 上記のことを次のようにも書きます。$`\quad a^{-1} …

…できた二重圏上の二重インデックス付き圏を定義しています。「状態遷移系達の二重圏の直接的定義」より： なお、マイヤースは、二重圏上の二重インデックス付き圏〈doubly indexed category〉という概念も提示しています。二重インデックス付き圏が、違和感／ズレを解消してくれるかも知れません。 複圏、二重圏、三重圏といった高次元圏類似構造の上にインデキシングを考えるという方向性はだいたい同じです。システムの記述は、必然的に高次元のインデキシング／高次元のファイブレーショ…

…ァイブレーション／余インデックス付き圏の構造を持つ。 2-圏達の3-圏内に居る2-ファイブレーションとかを使うとうまく定式化できるのかな？ と思ったりしますが、現状はよく分かりません。しかし、IOCシステムにその制御インターフェイスを対応させる写像 $`\mrm{Ctrl}`$ と、反ファイブレーション／余インデックス付き圏の構造を公理化することはできそうです。[追記] 以下に出てくる $`\quad \mrm{Ctrl}(\Phi ; \Psi) \cong \mrm{Ct…

…ヤース本の流儀では、インデックス付き圏からグロタンディーク二重構成〈the Grothendieck double construction〉を使ってアリーナ達の二重圏を作ります。ここでの具体例では、集合圏のインデックス付きスライス圏 $`\mbf{Set}/\hyp`$ が、“もとになるインデックス付き圏”です。グロタンディーク二重構成は、1つのインデックス付き圏 $`\msc{A}`$ に対する2つのグロタンディーク構成の組み合わせです。 通常のグロタンディーク構成 $`…

…レーションに対応するインデックス付き圏の再インデキシング関手を $`f^*`$ とすると、 $`\quad A = f^*(B)`$ という条件で縛られます。この条件を加味すると、プルバック四角形はさらに次のように書き換えられます。$`\quad \xymatrix{ {X\cdot f^*(B) } \ar[d]_{\rho_X^{f^*(B)} } \ar[r] \ar@{}[dr]|{\text{p.b.}} &{Y\cdot B } \ar[d]^{\rho_Y^B}…

…宣言関手（一般論ではインデックス付き圏）の翻訳関手（一般論では再インデキシング関手）です。逆グロタンディーク構成のアットマーク記法（「包括コンテキスタッドに向けて // グロタンディーク構成と逆グロタンディーク構成」参照）を使えば次のように書けます。$`\quad f^* = \mrm{Decl}(f) = \cat{D}@(f)`$ファイブレーション〈ファイバー付き圏〉 $`\cat{D}`$ とファミリー〈インデックス付き圏〉 $`\cat{D}@`$ は相互に置き換え可…

…拡張包括構造を持ったインデックス付き圏」に次のような追記をしています。 型理論の意味論の話をします。（[追記]意味論とは言っても、ほんとのセマンティクスと言うよりは、形式体系の構文圏〈syntactic category〉を構成する話なので、広義の構文論内部の狭義の意味論という感じです。[/追記]） 型理論に出てくる圏、C-システム〈C-system〉、ファミリー付き圏〈category with families〉、包括圏〈comprehension category〉など…

…ション ファミリー〈インデックス付き圏〉 グロタンディーク構成と逆グロタンディーク構成 ファイブレーション的プルバック四角形 デカルト持ち上げと亀裂子／分裂子 反ファイブレーション 局所ホニャララ・ファイブレーション 中置演算子記号の使い方 セクションとレトラクション トータル射の結合公式と図示 おわりに 補足： グロタンディーク対応 追記： 終対象の保存 ハブ記事： コンテキスタッド、包括圏、ハイパードクトリン ファイブレーションファイブレーションに関する過去記事達（古い順…

…れたインデキシング〈インデックス付き圏〉です。 グロタンディーク構成 : インデキシング〈インデックス付き圏〉→ ファイブレーション〈ファイバー付き圏〉 逆グロタンディーク構成 : ファイブレーション〈ファイバー付き圏〉→ インデキシング〈インデックス付き圏〉 トータル射 $`F`$ のファイバーパート〈fiber part〉は $`F^\flat`$ と書くことにします。ファイバーパートは次のような垂直射（ファイバー内の射）です。$`\quad F^\flat : A \t…

…次のような反変関手（インデックス付き圏）となります*2。$`\quad \mrm{Sub} : \cat{C}^\op \to \mbf{CAT}`$ $`\mrm{Sub}`$ は、包含構造から誘導されたインデックス付き圏なので、スード関手ではなくて厳密関手となります。前節のようにして、対象 $`A`$ ごとに $`\mrm{Sub}(A)`$ 上にミート半束構造を入れられるので、反変関手 $`\mrm{Sub}`$ は次のように分解〈factorization〉できます。…

…ゲット2-圏〉とするインデックス付き圏〈indexed category〉$`P`$ です。ハイパードクトリンのキモは限量子なのですが、今回は限量子には注目しないで、インデックス付き圏 $`P`$ だけに注目します。（限量子の話は「述語論理： ハイパードクトリンとパルムクイスト二重圏」に書いています。）$`\quad P: \cat{C}^\op \to \cat{L} \In 2\mathbb{CAT}`$ 2-圏 $`\cat{L}`$ が1-圏に退化していて、サイズもあ…

…も多くて、エス関手がインデックス付き圏〈indexed category〉となることもあります。つまり、一般には余域がk-圏となります。ただし、完全に抽象的なk-圏では議論がしにくいので具象k-圏だとします。具象2-圏については「述語論理： ハイパードクトリンとパルムクイスト二重圏 // エス関手」で述べています。具象1-圏については「圏の具象性に関する資料」で参考文献を挙げています。次元3以上の具象性はよく分かりませんが、当面使うこともないと思います。具象k-圏を余域とする…

…モデルとして、前層やインデックス付き圏ではなくて、ファイバー付き圏を想定している。 ファイバー付き圏のベース圏もファイバー〈局所圏〉も、通常の圏ではなくて複圏を想定している。 ベース圏もファイバーも、デカルト構造と余デカルト構造を持つ。 ベース圏もファイバーも、デカルト閉構造を持つ。 命題論理の構造はファイバー方向で表現される。 述語論理の構造は、ベース方向とファイバー方向の組み合わせ（絡み合い）で表現される。 型コンテキストは単なるリストで依存性は考慮してない。が、依存性の…

…拡張包括構造を持ったインデックス付き圏」から使っている記法です。依存型理論では、型はコンテキストと切り離すことができません。したがって、型 $`B`$ にコンテキストを添えて $`B@\Delta`$ と書くことにします。これは、「コンテキスト $`\Delta`$ における型 $`B`$〈type $`B`$ at a context $`\Gamma`$〉」という意味です。$`B@\Delta`$ は依存ペア〈dependent pair〉です。依存ペアの特別な書き方はな…

…(2013-05) インデックス付き圏を拡張してファイバー付き圏へ (2019-04) 14年ぶりにファイバー付き圏 (2019-04) 集合のバンドルと圏のバンドル (2024-06) ファイブレーションの亀裂と分裂 (2024-06) アロー圏 ＝ バンドルの圏 (2024-07) 関手のデカルト射とファイバー付き圏 (2024-12) 包括構造を備えた圏が包括圏です。記号の乱用で、包括圏とその台圏を同じ記号 $`\cat{C}`$ で表します。包括圏の定義にクラン構造が…

…拡張包括構造を持ったインデックス付き圏 // 拡張包括構造」にも記述がありますが、ちょっと分かりにくいので再論したのが上記過去記事です。クランは、拡張包括構造を載せる下部構造として適切だと思います。クランについては、以下の過去記事を参照してください。 クラン、ファイブレーション、スパン C-システムは、ほどよい抽象度の型理論的圏（「指標の圏はコンテキストの圏の反対圏」参照）です。以下の過去記事を参照してください。 C-システム、分裂ディスプレイクラス、カートメルツリー構造 さ…

…デキシング圏〉とするインデックス付き圏〈indexed category〉$`\mbf{Fam}_{(\mbf{Set}, P, S)}[\hyp]`$ を考えて、グロタンディーク構成すればOKです。$`\quad \mbf{Fam}_{(\mbf{Set}, P, S)} := {\displaystyle \int_{\mbf{Set}\times\mbf{Set}}} \mbf{Fam}_{(\mbf{Set}, P, S)}[\hyp]`$ 豊穣靴履きファミリー$`F…

…11年11月の記事「インデックス付き圏のフビニ／グロタンディーク同値」「大量のモナド類似物を取り扱う方法：参考文献」で言及されているので。過去記事から参照したURLは今は無効ですが、21 May 2010 日付の21枚スライドがインターネットにありました。そして、15ページの論文が CiteSeerX に投稿されていました。現在は40ページの長い論文になり、第3章が斜モノイド圏の話になっています。このブログ記事に書いたシナリオは、アルテンキルヒ／チャップマン／ウウスタルにより…

…タンディーク構成は、インデックス付き圏のグロタンディーク構成の非常に特殊なものです。その特殊性を理解するために、インデックス付き圏のグロタンディーク構成を知っていたほうがいいかも知れません。以下に過去記事： インデックス付き圏のグロタンディーク構成 グロタンディーク構成と積分記号 この節（の文脈／スコープ）での $`\cat{S}`$ は、リーディ圏とは限らない小さな圏とします。一般的グロタンディーク構成を特に前層 $`F:\cat{S}^\op \to \mbf{Set}`…

…d}(J)`$ 上のインデックス付き圏 $`\mrm{Repr}[\hyp]`$ と、圏 $`\mrm{FMnd}(\mbf{Set})`$ 上のインデックス付き圏 $`\mrm{EM}[\hyp]`$ のあいだのある種の同値性の主張です。説明を端折って一言でいってしまうのですが； 表現達の圏 $`\mrm{Repr}[R]`$ もアイレンベルク／ムーア代数達の圏 $`\mrm{EM}[M]`$ も、右加群〈right module〉達の圏だと思えます。左右は約束で決まるので…

…}`$ と書きます。インデックス付き圏のグロタンディーク構成を使えば次のように書けます。$`\quad \mbf{Cont} := {\displaystyle \int_{\mbf{Set}} } \mbf{Cont}[\hyp]`$ グロタンディーク構成に伴う標準射影は $`(X, F) \mapsto X,\; (f, \varphi)\mapsto f`$ です。コンテナのあいだの射を $`\alpha = (f, \varphi)`$ と書いたときは、次の記法を使い…

…CAT})`$ は余インデックス付き圏達の2-圏となります。つまり、この事例の図式とは余インデックス付き圏です。図式空間は余インデックス圏達の2-圏です。おわりにDiag構成は、Diag構成のセットアップのもとで図式空間を定義する手法です。「図式」という呼び名を採用してますが、メタレベル 0 の簡単な（自明な）例では 図式＝述語、メタレベル 1 の簡単な例では 図式＝余前層、メタレベル 2 の簡単な例では 図式＝余インデックス付き圏 でした。メタレベルが違うと、Diag構成で…

…}`$ 前層を特別なインデックス付き圏だとみなして、グロタンディーク構成を施して作った平坦化圏〈flattened category〉を要素の圏〈category of elements〉と呼びます。要素の圏は $`\mrm{El}(\hyp)`$ と書きましょう。要素の圏 $`\mrm{El}(\mrm{PL}_X)`$ を具体的に記述すると： 要素の圏の対象は、ポジション付き有限順序ツリー $`S`$ と、ポジション・ラベリング $`a : \mrm{Pos}(S) \t…

…使ってみては？ あるいは、既に小さい骨格が使われているかも知れない。 前層やインデックス付き圏を見たら、すぐにグロタンディーク構成しよう。グロタンディーク構成の平坦化圏やファイバー付き圏を使ったほうが見やすいことも多い。 二種類の射があるように思えたら、二重圏あるいは二重圏類似構造が存在するかも。 三種類の射があるように思えたら、三重圏あるいは三重圏類似構造が存在するかも。 オペラッド構造が見つかるといいことあるよ。見つけよう。 モナドが見つかるといいことあるよ。見つけよう。

…: https://arxiv.org/abs/math/0412512 URL: http://homepage.sns.it/vistoli/descent.pdf (PDF) このテキストは、20年近く前の記事で紹介しました。 見つけもの：Angelo Vistoliのていねいな論文 (2005年3月31日) 以下の過去記事でも言及しています。 インデックス付き圏を拡張してファイバー付き圏へ 14年ぶりにファイバー付き圏 現時点でも、ヴィストリの解説はおすすめできます。