自然数全体の集合を $`\mathbf{N}`$ と書きます。最初の無限順序数は $`\omega`$ と書きます。$`\mathbf{N}`$ も $`\omega`$ も特定の集合を名指す固有名です。現在主流のオフィシャルな立場から言えば、$`\mathbf{N}`$ と $`\omega`$ は同じです。特定の集…

「順序数と集合圏」において順序数の話をしました。その続きとして、この記事では基数の話をします。集合圏の骨格を作ると同時に、フォン・ノイマン流の基数割り当ても定義します。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} …

基本的な素材から構成される構造物を記述するためのほぼ唯一の手段が指標です。型理論の「コンテキスト」は「指標」の同義語です。その他に「仕様」「表示〈presentation〉」「セオリー」「ボキャブラリー」と呼ばれることもあります。プログラミング言語で…

順序数の話は以下の過去記事でしたことがあります。 再帰的構成のために： 順序数の圏 その動機を以下のように書いています。 順序数に沿って再帰的構成や帰納的証明をするとき、順序数全体をモノイド圏だとみなしたほうが便利なので、そのことを話題にしま…

2年ほど前（2023年の春）、二重圏ベースでハイパードクトリンを定義できないかとジタバタしていました。 述語論理： 二重圏的ハイパードクトリン 述語論理： シード付き二重圏 -- 訂正と再論 結局、ハッキリとした定式化は得られず、締りのないままに放置。…

「方向と向きは区別しなさい」と教わって、それを守ってきたつもりですが、テクニカルタームだとしても「方向」と「向き」を区別して運用するのはどうも無理がある気がしてきました。方向は direction で、向きは orientation のことなのですが、思い切って…

「バタニンのペースティング図をXyJax (Xy-pic extension for MathJax)で描いてみる」の続き。2-圏のなかの構造といえば、なんつっても随伴系〈adjunction | adjoint system〉ですよね。ニョロニョロ関係式〈snake {law | relation | equation | identity}〉…

もう何年も、いやっ何十年も悩みの種で年中愚痴っていることは： 圏論で使う絵図（ペースティング図やストリング図）をWeb上で描けない。描けたとしても手間がかかり過ぎる。 圏論で使う絵図のテキスト化がうまくいかない。やれるとしても手間がかかり過ぎる…

ペースティング図は、2-圏や二重圏内に描かれた図式〈diagram〉です。1-圏でも、射のあいだの等式を2-射とみなせば2-圏になります。そして、1-圏のペースティング図は可換図式なのです。圏論ではペースティング図（可換図式含む）を多用しますが、ペースティ…

「関手のテンソル積（コエンド） // あれれ」において、関手のテンソル積と類似した状況があちこちで出現するけど何でだろう？ てなことを書いています。これはおそらく、米田拡張やコエンド公式〈coend formula〉が色々な場面で使われる、ってことでしょう…

タイトルはダブルミーニングです。ひとつは「二重圏は面白いよなー」ということ。もうひとつは「興味深い二重圏の事例を幾つか紹介するよ」ということです。過去記事への参照をたくさん含むので、二重圏関連のハブ記事になっています。最後に、まだ触れたこ…

ファイバー積はコスパン（V字形の図式）の極限対象です。コスパンの拡張であるW字形の図式にもファイバー積が定義可能です。V字形からW字形への移行が自明のように扱っていることがありますが、それほど簡単とも言えません。$`\newcommand{\cat}[1]{\mathcal…

集合を係数〈スカラー〉とするベクトルや行列の計算は、相対モナドを使うとうまく定式化できます。やってみましょう。小手調べとして、自然数係数の有限次元行列の計算についても述べます。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\math…

「二重圏でどんないいことあったの？」より： いいこと三つ目、「二重圏化と米田モナド」の最後のほうに書いたことですが、「関数：関係：包含 ＝ 関手：プロ関手：制限自然変換」という“比例式”がより鮮明になってきました。 どういうことかと言うと、関数…

バエズ〈John C. Baez〉が、イズベル双対性に関して3ページの短い解説を書いています。 [Bae22-23] Title: Isbell Duality Author: John C. Baez Submitted: 21 Dec 2022 (v1), 3 Sep 2023 (v2) Pages: 3p URL: https://arxiv.org/abs/2212.11079 バエズの論…

本日3投稿目。プロ関手とその結合〈プロ結合〉は重要なんですが、分かりにくいんですよね。もっと分かりやすい概念として混合圏を紹介します。「混合圏」は僕が命名したのですが、混合圏に関係する概念として「ヘテロ射〈heteromorphism〉、ブリッジ〈bridge…

本日さきほど上げた記事「二重圏化と米田モナド」にて： 最近、思っていることなんだけど； 通常の圏〈1-圏〉や2-圏でやっていたことを、二重圏でやってみると割といいことあるよね。たまに“すごくいいこと”もあります。うまいこと、二重圏／三重圏（一般に…

最近、思っていることなんだけど； 通常の圏〈1-圏〉や2-圏でやっていたことを、二重圏でやってみると割といいことあるよね。たまに“すごくいいこと”もあります。「惑わされないために」より： 二種類の射があるように思えたら、二重圏あるいは二重圏類似構…

「二重圏のコンパニオン／コンジョイントと米田の星」の冒頭で： 形式圏論を考える舞台として2-圏より二重圏のほうが良さそうな気がします。ちょっとした状況証拠をひとつ挙げます。 “二重圏を使った圏論”について考えているわけです。「コーナー、キンク、…

とある勉強会で使っているとある教科書*1のガロア理論の文脈のなかで、とある随伴関手ペア〈随伴系〉が出てきたので紹介します。一般的な手法で定義できる2つの関手が、特定の状況下では随伴関手ペアになる、という定理です。ガロア理論の文脈でこういう随伴…

圏論をベースに型理論を展開するアプローチがあります。このアプローチは圏論的型理論と言えるでしょう。とはいえ、現在の型理論において圏論を使わないことは考えにくいので、型理論＝圏論的型理論 だと言っていいでしょう。また、依存性を扱う依存型理論が…