公理的集合論やグロタンディーク宇宙の公理系では、順序を持たないペアが作れることは保証しています。が、順序を持つペアは頑張って作るのが普通です。作り方は一通りではありません。典型的な順序ペアの作り方を見ておきましょう。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\In}{\text{ in }} \newcommand{\Imp}{\Rightarrow } \newcommand{\Iff}{\Leftrightarro…

…いています。 贅沢なグロタンディーク宇宙とPropositions-As-Types Propositions-As-Typesを曲解しないで理解するために 要約しておくと： $`|\mbf{Logic}| = |\mbf{Set}|`$ 、したがって、対象は集合 $`\mbf{Logic}`$ はやせた圏。したがって、2つの対象のあいだの射はあってもひとつ。 $`X \ne \emptyset`$ のとき $`\mbf{Logic}(X, \emptyset)`$ は空集合…

…にサイズが大きくなるグロタンディーク宇宙の系列と、各グロタンディーク宇宙に対する集合圏、さらにはn-圏達の(n + 1)-圏達がグリッド状（下の表のよう）に配置されて世界〈world〉が形成されます。サイズレベルが $`r`$ であるn-圏達を対象とする(n + 1)-圏は $`n\mbf{Cat}_{\# r}`$ と書きます。また、宇宙達は次のように書きます。$`\quad \mbf{Univ}_{\# r} := |0\mbf{Cat}_{\# r}|`$$`r, n`…

…ものと、集合の宇宙〈グロタンディーク宇宙〉を余域とするものがある。 警告は、語彙エントリー内に書くのもありでしょう。複数の用語の組み合わせに関する注意事項は、特定の語彙エントリー内には書きにくいので別ファイルとなるでしょうが。用法や警告以外にも、用語を憶える助けなるエピソードや、関連する人物の情報なども語彙エントリーとは別種のファイルとしてリンクしておけば役に立つかも知れません。学習の方法としての語彙目録作成Obsidianを使って試しに幾つかの語彙エントリーを作ってみたので…

…台集合も許すならば、グロタンディーク宇宙も一種の代数系とみなせます。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mbf}[1]{\mathbf{#1} } %\newcommand{\mbb}[1]{\mathbb{#1} } %\newcommand{\u}[1]{\underline{#1} } \newcommand{\Imp}{\mathre…

…日の記事「非継承的なグロタンディーク宇宙」の最後の節に、ZF集合論の公理達を並べているのですが、あまり読みやすくないですね。論理式も、記法やレイアウトを工夫すると可読性が向上することがあります。やってみましょう。$`\newcommand{\Uin}{\mathrel{\epsilon} } \newcommand{\mbf}[1]{\mathbf{#1} } `$試してみることは： 限量子の直後の '$`\in U`$' の省略 限量子記号 '$`\forall`$' の省…

ここ最近、グロタンディーク宇宙の話をしています。 贅沢主義者のグロタンディーク宇宙 (7月20日) 型・インスタンス・宇宙とタルスキ宇宙系列 (7月22日) 贅沢なグロタンディーク宇宙とPropositions-As-Types (7月24日) ZF宇宙、グロタンディーク宇宙、型宇宙 (7月27日) 今日もグロタンディーク宇宙の話です。通常のグロタンディーク宇宙は、ZF集合論における普通の集合 $`U`$ です。が、$`U`$ のなかでZF集合論ができる集合です。$`U`$ …

…論のなかで定義できるグロタンディーク宇宙でおおよそモデル化できます。が、型宇宙はグロタンディーク宇宙そのものだ、とは言いにくいです。なんか食い違いがある。この食い違いについて考えてみます。$`\newcommand{\mrm}[1]{\mathrm{#1} } %\newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\mbf}[1]{\mathbf{#1} } \newcommand{\u}[1]{\underline{#1} } \…

「贅沢なグロタンディーク宇宙とPropositions-As-Types」に対して、老婆心的な補足をします。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\mbf}[1]{\mathbf{#1} } \newcommand{\In}{\text{ in }} `$内容： 「命題」を排除したい！ ベリティ型とその型宇宙 述語 ＝ ベリティ型ファミリー 同義語・曖昧多義語 「命題」を排除したい！「贅沢なグロタンディーク宇宙とPr…

…です。 贅沢主義者のグロタンディーク宇宙 型・インスタンス・宇宙とタルスキ宇宙系列 Propositions-As-Typesというよく知られたキャッチフレーズを、グロタンディーク宇宙の観点からなるべく明確にします。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\cat}[1]{\mathcal{#1} } \newcommand{\In}{\text{ in }} \newcommand{\mbf}[1]{\mathbf{…

「贅沢主義者のグロタンディーク宇宙」でグロタンディーク宇宙の話をしました。贅沢主義か節約主義かは、公理系を設定するときの態度であって、どちらの態度で公理系を設定しても、得られる概念は同じです。ところで、単一のグロタンディーク宇宙ではなくて、宇宙の無限系列を考えることがあります。$`\quad U_0 \in U_1 \in U_2 \in \cdots`$番号を 0 から始めましたが、1 から始めることもあります。番号付け方式の違いはどうでもいい違いです。宇宙の無限系列を、集…

…することがあります。グロタンディーク宇宙の公理系を節約と経済性の原則を無視して再定義してみます。$`\newcommand{\mrm}[1]{\mathrm{#1} } \newcommand{\In}{\text{ in }} \newcommand{\mbf}[1]{\mathbf{#1} } \newcommand{\Imp}{\Rightarrow} \newcommand{\hyp}{\text{－} } \newcommand{\dtimes}{\mathop{!…

… U'`$ を2つのグロタンディーク宇宙とします。2つのグロタンディーク宇宙から作られた2つの集合圏を次のように書きます。$`\quad {\bf Set}_U\\ \quad {\bf Set}_{U'} `$デフォルトの宇宙を $`U`$ 、デフォルトより一段大きな宇宙を $`U'`$ と考えて、次の略記をします。$`\quad {\bf Set} := {\bf Set}_U\\ \quad {\bf SET} := {\bf Set}_{U'} `$大きな集合圏 $`…

…ワーキング宇宙であるグロタンディーク宇宙 $`{\bf U}`$ のなかで考えます。つまり：$`\quad |{\bf Odnl}| \subseteq {\bf U}`$$`|{\bf Odnl}|`$ はグロタンディーク宇宙 $`{\bf U}`$ のなかに閉じ込められていますが、$`|{\bf Odnl}|\in {\bf U}`$ ではないので小さい集合ではありません。順序数全体の集合は、$`{\bf U}`$-小集合ではなくて$`{\bf U}`$-クラス（真のクラ…

…書いています。適当なグロタンディーク宇宙を設定するにしても、$`|{\bf Odnl}|`$ は非常に大きな集合（むしろ、非常に長い集合）です。$`|\cat{I}|`$ は小さい集合なので、次の性質を持つ順序数 $`\gamma`$ が存在します。$`\quad \forall i\in |\cat{I}|.\, \mrm{dim}_\cat{I}(i) \le \gamma`$このような順序数 $`\gamma`$ のなかで最小な順序数が一意に存在するので、それを $`\…

…\#r`$ は宇宙〈グロタンディーク宇宙〉のレベルです。大きなサイズが必要なときは、$`r`$ の値を大きくとります。 $`j`$ は切り落とし次元〈truncation dimension〉です。デフォルトは $`j = 1`$ 。$`j = 0`$ のときモデル空間は単なる集合になります。 例えば、モノイドを「指標」と呼ぶことにして、編入子は、モノイドを単一対象の圏とみなす関手だとします。$`\quad J : {\bf Mon} \to \dimU{\bf CAT}{1…

…ズに関しては、宇宙〈グロタンディーク宇宙〉のレベルを $`r`$ として、レベル $`r`$ の宇宙で定義された“n-圏達の(n+1)-圏”は次のように書きます。$`\quad n{\bf Cat}_{\#r}`$デフォルトの宇宙レベルを決めて、文字種〈フォント〉により宇宙レベル（サイズの基準）を区別する書き方も使います。以下は、「ファミリー構成モナド： 大規模構造の事例として // 一般化されたファミリーとその圏」からコピーした表です。 $`r = d `$ $`r = d…

…。圏のサイズについてグロタンディーク宇宙の系列（「最近の型理論： 宇宙・世界・銀河 もう少し」の前半参照）から、デフォルトの宇宙 $`U`$ と、$`U`$ の次の宇宙 $`U'`$ を取り出して考えます。$`U`$ の要素を小さい集合〈small set〉といいます。$`U'`$ の要素を大きい集合〈large set〉といいます。次は成立しています。$`\quad U \in U'\\ \quad U \subset U' `$定義より、「小さい集合は大きい集合です」。自…

…。つまり、どの宇宙〈グロタンディーク宇宙〉のなかでも関手という概念は一律に通用するのです（宇宙多相〈universe polymorphic〉な定義が可能）。言い方を変えると、関手を定義する行為には、サイズの違いは影響しません。関手 Fam特定固有な関手 $`\mrm{Fam}`$ を定義するために、その対象パート $`\mrm{Fam}_0`$ から定義します。何を定義すべきか（主題）を、先に $`\Subject`$で宣言して、それに続けて実際の定義を書くことにします。$…

…で定義します。 *4:関手意味論の言葉で言えば、図式とは関手モデルのことです。 *5:すべての集合とは言っても、グロタンディーク宇宙 $`U`$ のなかで考えているので、無闇に大きいわけではありません。 *6:ペローネ／ソーレンは、図式の2-圏を定義していますが、ここでは1-圏とします。 *7:余米田埋め込みは $`\cat{C}^\op \to \cat{C}^\vee`$ ともとれます。 *8:ペローネ／ソーレンは小さい前層〈small presheaf〉と呼んでいます。

…\lambda\, i\in I. \bs{t}_i`$ *3:グロタンディーク宇宙の系列です。 *4:日本語の「の」の曖昧性で、正確な表現が難しい。この場合、テーブルインスタンスに所属するタプル $`t \in T`$ ではなくて、テーブルインスタンス達 $`T_1, T_2, \cdots, T_N`$ を成分として作ったタプル $`(T_1, T_2, \cdots, T_N)`$ の意味です。日本語だけではく、数式表現も参照してもらえれば、誤解しにくいとは思いますが。

…に定義しています。 グロタンディーク宇宙 $`U`$ に対して、$`U`$-局所小圏 $`\cat{C}`$ がデカルト閉圏であり、離散完備かつ離散余完備なとき、$`\cat{C}`$ を $`U`$ 上の銀河〈galaxy over $`U`$〉、あるいはより短く$`U`$-銀河〈$`U`$-galaxy〉と呼ぶことにします。 この銀河の条件は厳しすぎる気もします*1。うんと条件を緩めるなら、単なるデカルト閉圏でも銀河と認めるという案もあります -- 緩め過ぎかも。適切な条…

…列に並べられた宇宙〈グロタンディーク宇宙〉の系列です。$`\quad U_0 \in U_1 \in U_2 \in \cdots`$この系列を仮定するのは、異常に超越的です*1が、まーいいんじゃないかと思います -- 認めましょう。宇宙 $`U = U_i`$ ごとに集合圏 $`{\bf Set}_U`$ が付属しています。1：1に対応した宇宙と集合圏の集まりが世界のコア（コア宇宙とコア銀河）となります。コア宇宙（一列に並んだグロタンディーク宇宙）とコア銀河（集合圏）以外の…

…'`$ を三階層分のグロタンディーク宇宙とします。三階層分あればたいてい間に合います。集合圏や圏の圏は $`U, U', U''`$ に相対的に考えます。 $`{\bf Set} := {\bf Set}_U`$ $`{\bf Cat} := \mrm{Cat}({\bf Set})`$ （$`\mrm{Cat}(\hyp)`$ は内部圏の2-圏を作り出す構成） $`{\bf SET} := {\bf Set}_{U'}`$ $`{\bf CAT} := \mrm{Cat}(…

…。 $`U`$ ： グロタンディーク宇宙。$`{\bf Set}, {\bf SET}, {\bf Cat}, {\bf CAT}`$ などは、$`U`$ に対して相対的に定義されるとします。 $`\cat{C}, \cat{D}`$ ： $`U`$-局所小なデカルト圏（小さいデカルト圏なら、もちろんOK）。$`\cat{D}`$ は$`\cat{C}`$-両完備だとします。 $`\cat{P}`$ ： $`\cat{P}[\hyp] := {\bf CAT}(\J(\hyp…

…階層（表の横方向）はグロタンディーク宇宙の階層に起因します。それについては、次の記事を見てください。 最近の型理論： 宇宙・世界・銀河 もう少し // 絶対的大宇宙とグロタンディーク宇宙 $`\cat{C}, \cat{D}`$ が圏のとき、関手圏を $`[\cat{C}, \cat{D}]`$ と書きますが、指数記法 $`\cat{D}^\cat{C}`$ も使います。関手圏のホムセットを書くときは、指数記法のほうが視認性が良いようです。$`\quad \cat{D}^\c…

…ます。到達不能基数とグロタンディーク宇宙は事実上同じものですから、型宇宙をグロタンディーク宇宙で解釈していることになります。Coqの型宇宙を定式化するのが目的のようです。Coq風の型システム／構文によるZFC集合論の記述も書いてあります。これにより、ZFC集合論と型理論は双方向にシミュレート可能だと分かります。 Title: An Intuitionistic Set-theoretical Model of $`\mrm{CC}^\bar{\omega}`$ Authors…

…階層（表の横方向）はグロタンディーク宇宙の階層に起因します。それについては、次の記事を見てください。 最近の型理論： 宇宙・世界・銀河 もう少し // 絶対的大宇宙とグロタンディーク宇宙 集合圏のホムセットを次のようにも書きます。$`\quad \mrm{Map}(A, B) := {\bf Set}(A, B) \;\in |{\bf Set}|\\ \quad \mrm{MAP}(A, B) := {\bf SET}(A, B) \;\in |{\bf SET}|`$圏の…

…容： 絶対的大宇宙とグロタンディーク宇宙 型宇宙 圏論的銀河 世界の構造と法則 シリーズ・ハブ記事： 最近の型理論： 宇宙と世界、そして銀河 絶対的大宇宙とグロタンディーク宇宙“絶対的大宇宙”とは、現在の集合論〈ZFC集合論〉の宇宙です。あらゆる集合はこの宇宙内に居て、宇宙の外を考えることは出来ません。絶対的大宇宙〈absolute macrocosm〉を $`\mathbb{V}`$ で表すことにすると、次が成立します。$`\quad x`$ は集合である $`\Iff x…

…e}`$ の要素）はグロタンディーク宇宙です。グロタンディーク宇宙は、集合論〈ZFC集合論〉で“集合”と認められる集合ですが、そのなかで集合論的構成が自由に行えるような集合です。「集合論的構成が自由に行える」とはどんなことかは、次の記事を読むと感じがつかめるでしょう。 セクションとタプル グロタンディーク宇宙そのものに関しては、以下の過去記事とそこから参照される関連記事になにやら書いています。 グロタンディーク宇宙って何なんだ？ あなたはこの公理を信じますか グロタンディーク…