…f{Set} `$ シグマ型（離散圏のグロタンディーク構成）とパイ型（セクション空間）を知っていれば、それを使って $`\mrm{Sect}(F_k)`$ を定義してもかまいません（そのほうがカッコイイ）。次の同型が成立するのでした。$`\quad \mrm{Sect}(F_k)\cong \bigoplus_{\sigma\in G_k}F_k(\sigma) \In \mbf{FdIpVect}`$外微分作用素2-セルラー層に関する外微分作用素〈exterior diff…

…の集合を定義します。シグマ型、パイ型、グロタンディーク構成などを引き合いに出さず、直接的定義をします。$`\bigcup_{i\in V}\u{F_\mrm{vert}(i)}`$ は、ベクトル空間の台集合（下線で示している）達をすべて合併した集合です。ベクトル空間ファミリー $`F_\mrm{vert}`$ のセクション〈section〉とは次のような写像です。$`\quad \bs{x} : V \to \bigcup_{i\in V}\u{F_\mrm{vert}(i)…

…hi`$ が、総和〈シグマ型〉$`\sum_{a\in |\cat{C}|} X(a)`$ に値を取ると考える場合（通常はそう考える）は、値を依存ペアの形で書きます。$`\quad \Phi(\An{a, \varphi, X}) = (a, \varphi^\flat) \text{ where } a\in |\cat{C}|, \varphi^\flat \in X(a) `$ 単一の値 $`\varphi^\flat`$ と依存ペア $`(a, \varphi^\fl…

…i_f`$ 左右は、シグマ型（集合族の総和）とパイ型（集合族のセクション空間）にちなみます。実際、シグマ型とパイ型を使って $`\Sigma_f, \Pi_f`$ を書けます。ここから先、ギリシャ文字大文字の $`\Sigma, \Pi`$ と、総和記号 $`\sum`$ 、総積記号 $`\prod`$ は次のように使い分けます。 $`\Sigma_f`$ は、$`\Delta_f = f^*`$ の左随伴関手 $`\Pi_f`$ は、$`\Delta_f = f^*`$ の…

…f{N} `$ まずシグマ型を作ります。$`\quad \sum_{x\in X}F(x) := \bigcup_{x\in X} (\{x\}\times F(x) ) `$ $`X`$ から $`\sum_{x\in X}F(x)`$ へのセクション達の集合がパイ型です。$`\quad \prod_{x\in X}F(x) := \mrm{Sect}(\pi : \sum_{x\in X}F(x) \to X)`$ここで、$`\pi`$ はシグマ型の標準射影で、セクション…

…依存型のひとつであるシグマ型（集合の総和）を使って $`\mrm{Cut}`$ のプロファイル（入出力の仕様）を書くと次のようです。$`\quad \mrm{Cut} : \sum_{A\in |\mbf{BM}|} IE(A) \to |\mbf{BM}| \In \mbf{SET}`$ ここで、$`IE(A)`$ は、半グラフ $`A`$ の内部辺〈internal edge〉達の集合です。依存型を使うと、他の半グラフ・コンビネータのプロファイルも正確に書けます。準備とし…

…プルは、依存型理論のシグマ型／パイ型と、ハイパードクトリン（「述語論理： ハイパードクトリンとパルムクイスト二重圏」参照）の存在限量子／全称限量子に現れます。モデル関手インスティチューション理論に出てくるモデル関手は、モデル理論におけるモデルの抽象的定式化（モデル関手の関手戻り値対象である圏の対象がモデル）です。モデル関手は通常 $`\mrm{Mod}`$ と書かれますが、加群〈module〉の圏と誤認されないように、$`\mrm{Model}`$ を使います。$`\quad…

…まる。 この手順を、シグマ型構成により書き下したのが以下の形（再掲）です。$`\quad \sum_{f\in \mrm{Map}(\base{F}, \base{G})} \mrm{Nat}(F, f^*(G) : \base{F}\to \mbf{Set})`$$`\varphi = (\base{\varphi}, \varphi^\#)`$ という書き方は依存ペアです。ペアの第一成分がベースパート、第一成分に依存して選ばれる第二成分がファイバーパートです。圏としての恒…

…合は、大きな集合達のシグマ型構成を用いて次のように書けます。$`\quad \sum_{X\in |\mbf{Set}|}\mrm{MAP}(X, \mbf{SynConstr})`$ ホムセット $`\mbf{SET}(\hyp, \hyp)`$ を $`\mrm{MAP}(\hyp, \hyp)`$ と書いています。（$`\mbf{Set}(\hyp, \hyp)`$ は $`\mrm{Map}(\hyp, \hyp)`$ です。）ソート無し導出系達の圏ソート無し導出系達…

…とします。このとき、シグマ型とパイ型は次のように書きます。$`\quad \sum(X \mid F) = \sum(x\in X \mid F(x))`$ $`\quad \prod(X \mid F) = \prod(x\in X \mid F(x))`$ ファミリー〈族〉の合併も同様な書き方をします。$`\quad \bigcup(X \mid F) = \bigcup(x\in X \mid F(x) )`$ ファミリー自体は次のように書きます。$`\quad F =…

…。他に、前層に対してシグマ型とパイ型が構成できるとします。シグマ型とパイ型の高水準な定義は、$`f:X \to Y`$ （離散圏間の関手とみなした関数）によるプレ結合引き戻し関手 $`\Delta_f`$ の左随伴関手がシグマ型、右随伴関手がパイ型です。次の随伴トリプルがあります。$`\quad \sum_f \dashv \Delta_f \dashv \prod_f`$ 具体的・構成的に $`\sum_f, \Delta_f, \prod_f`$ を定義することもできます…

…のような集合の総和（シグマ型）です。$`\quad |\cat{E}| = \sum_{X\in |\cat{D}|} H(X) = \sum_{X\in |\cat{D}|} \cat{C}(A, U(X)) `$ $`|\cat{E}|`$ の要素（圏の対象）を $`(X, a)\text{ where }a\in H(X)`$ のような依存ペアで表します。2つの対象 $`(X, a), (Y, b)`$ のあいだの射とは、射 $`f:X \to Y \In \cat{D…

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

…んが、集合の無限和（シグマ型）は定義できます。ファミリー $`X`$ は次のように表示できます。（$`\delta_a`$ は $`\delta_A(a)`$ の略記。）$`\quad X \cong \sum_{a\in A} X^a \times \delta_a`$ 注意すべきは、総和記号が、集合〈スカラー〉を足し合わせているのではなくて、ファミリー〈集合係数ベクトル〉を足し合わせていることです。成分 $`X^a = X(a)`$ は集合〈スカラー〉ですが、$`\del…

…\hyp)`$ は、シグマ型（集合族の総和）を表します。 台圏〈underlying category〉： $`\cat{C}`$ （記号の乱用で、包括圏全体も $`\cat{C}`$ と書く） エス関手〈ess functor〉： $`\msc{S}_\cat{C}: \cat{C}^\op \to \mbf{Set}\In \mbf{CAT}`$ コンテキスト拡張演算〈context extension operator〉： $`\mrm{CExt}_\cat{C}: \…

…合は、集合達の総和〈シグマ型〉で与えます。$`\quad |\mrm{El}(F)| := {\displaystyle \sum_{\xi\in |\cat{S}|} } F(\xi)\\ = {\displaystyle \bigcup_{\xi \in |\cat{S|} } } (\{\xi\}\times F(\xi) ) `$集合 $`|\mrm{El}(F)|`$ の要素は、$`|\cat{S}|`$ の要素 $`\alpha`$ と $`F(\alpha)`$…

…\sum}`$ は、シグマ型（集合達の総直和）を表す記号。 $`P\H\mbf{Bun}^\mrm{fin}_C`$ は、セル達（「一般化ハイパーグラフ → P-バンドル、P-ファミリー」参照）の集合が有限である$`P`$-バンドル達からなる $`P\H\mbf{Bun}_C`$ の充満部分圏。 $`\mrm{Templ}^\Sigma_X(H, A)`$ は、次の条件を満たすストリング図テンプレート達（「ストリング図、ストリング図動画が“使える”とは？」参照）の集合。 ワイ…

…〈パイ型〉と総直和〈シグマ型〉は次のように書きます。 総直積： $`\prod_{i\in I}A(i)`$ または $`{\displaystyle \prod_{i\in I}A(i)}`$ 総直和： $`\sum_{i\in I}A(i)`$ または $`{\displaystyle \sum_{i\in I}A(i)}`$ 総直積は集合圏における極限対象、総直和は余極限対象であることに注意してください。極限対象からは射影〈projection〉があり、余極限対象への入…

…、コンテキスト拡張がシグマ型に、セクション達の集合がパイ型となっているからです。一方で、エス関手がハイパードクトリンを定義するとき、水増し関手 $`\Delta_{\Gamma, A}`$ の左随伴を $`\Sigma_{\Gamma, A}`$ 、右随伴を $`\Pi_{\Gamma, A}`$ と書いたりもします。$`\Sigma, \Delta, \Pi`$ が作る随伴トリプルをΣ-Δ-Π随伴〈Σ-Δ-Π adjunction〉と呼んだりします。この随伴トリプルは、エス…

…ructor〉と有限シグマ型コンストラクタ〈finite sigma type constructor〉を定義します。$`\quad \prod \vec{A} = \prod (A_1, \cdots, A_n) = \prod (A_i)_{i\in \bar{n}} = \prod_{i\in \bar{n}} A_i`$ $`\quad \sum \vec{A} = \sum (A_1, \cdots, A_n) = \sum (A_i)_{i\in \bar{n}}…

…僕は不快です。また、シグマ型を構成する演算記号としても使われます。 リスト処理のコンス演算（リストの先頭に項目追加）の演算記号としては、カンマではなくて '$`\cons`$' を使う。 リスト処理のスノック演算（リストの末尾に項目追加）の演算記号としては、カンマではなくて '$`\snoc`$' を使う。 リスト処理の連接演算（2つのリストを繋ぐ）の演算記号としては、カンマではなくて '$`\#`$' を使う。 シグマ型を構成する演算記号としては、カンマではなくて '$`\…

…、存在限量子としてはシグマ型を使えるので、述語論理まで含めて論理演算の代わりに集合演算が使えて大変に便利です。ソフトウェアを作る立場だと、集合演算さえ実装すれば論理演算にそのまま流用できるので、これはとてもアリガタイことになります。真偽値としての集合達を圏に仕立てたものが $`\mbf{Logic}`$ です。圏 $`\mbf{Logic}`$ については以下の記事で書いています。 贅沢なグロタンディーク宇宙とPropositions-As-Types Proposition…

…`$ は、次のごとくシグマ型（の集合）に所属しています。$`\quad ((X, Y), f) \in \sum_{(X, Y)\in |\mbf{Set}|^2} \mbf{Set}(X, Y)`$なので、関数 $`\text{is-injective}`$ のプロファイルは次のようにも解釈できます。$`\quad \text{is-injective} : \sum_{(X, Y)\in |\mbf{Set}|^2} \mbf{Set}(X, Y) \to |\mbf{L…

…いは余極限、あるいはシグマ型構成（どれも同じ意味）です。集合 $`X`$ を動かしてやると、次のような関数が定義できます。$`\quad P(\hyp) := \sum_{i\in I} \hyp^{C(i)} \;: |\mbf{Set}| \to |\mbf{Set}| \In \mbf{SET}`$ハイフン〈無名ラムダ変数〉の場所には写像〈集合圏の射〉を入れることもできて、関手性〈functoriality〉も示せるので、関数から関手に昇格できます。$`\quad P …

…b{SET}`$ のシグマ型構成です。 順序なしペアの構成： $`\{\hyp,\hyp\} : U\times U\to U \In \mbb{SET}`$ 述語による部分集合の構成（分出公理）： $`\{\hyp \mid \hyp\} : \Sigma(x\in U \mid \mrm{AMap}(x, \mbf{B}) )\to U \In \mbb{SET}`$ ファミリーの合併集合の構成： $`\bigcup(\hyp) : \Sigma(x\in U \mid …

…的型としてのパイ型とシグマ型は似たような形になりがちです（どちらも型ファミリーを素材として作る型だからです）。パイ型は、もっと馴染みがある言い方をすれば構造体型とかレコード型です。シグマ型は、タグ付きユニオン型といえば少し分かりやすいでしょう。見た目は同じ式を使うとして、構造体型／レコード型を定義する形式なら $`\format{record-type-def}`$ 、タグ付きユニオン型を定義する形式なら $`\format{tagged-union-type-def}`$ …

…o \{x\}`$ シグマ型： $`(f:x \to U)\mapsto \Sigma(x\mid f)`$ パイ型： $`(f:x \to U)\mapsto \Pi(x\mid f)`$ オメガ型： $`(f:x \to U)\mapsto \Omega(x\mid f)`$ 直和集合、直積集合、関数集合も最初から入れてもいいですが、これらは極めて簡単に定義できます。 直和集合： $`x + y := \Sigma(\{1,2\} \mid \{ 1\mapsto x, …

…リー $`F`$ のシグマ型となっている場合を考えます。このときの $`f`$ はシグマ型の標準射影〈canonical projection〉です。$`\quad s : B \to \Sigma(B \mid F) \In \cat{C}\\ \quad \text{where } s;f = \mrm{id}_B `$型、インスタンス、インスタンスの居住地の概念は単純型理論より面倒になりますが、インスタンスのコンテキストが域〈domain〉であることは単純型理論と変わり…

…ます。$`U`$ はシグマ型構成とパイ型構成に関して閉じているとします。前節の「族〈ファミリー〉の合併構成に関して閉じている」に似た形の公理になります。 $`U`$ は、シグマ型構成に関して閉じている： $`\forall x, f.\; x\in U \land f\in \mrm{Map}(x, U) \Imp \Sigma(f)\in U`$ $`U`$ は、パイ型構成に関して閉じている： $`\forall x, f.\; x\in U \land f\in \mrm…

…理と約束」で定義したシグマ型を表す二項演算子記号。もともとは、「シグマ型とパイ型の短縮記法（便利）」で '$`\ltimes`$' として導入したもの。感嘆符に変更したのは、$`!\!{+},\, !\!{\to}`$ なども使いたいから。 $`q^\#g`$ は、$`q`$ による $`g`$ のファイバー引き戻し。上の図の $`g'`$ のこと。「ファイバー引き戻し」は、「ファイバーの計算の動機としてのプルバック公式 // プルバックってなに？」で色々な「引き戻し」を区別…