「導出系： 反省と課題 // ソート付き集合の圏は変わる」において、ソート付き集合達の圏 $`\mathbf{SortedSet}`$ を導入したのですが、その定義は関係をベースにしています。関係をベースにした定義は、どうも分かりにくいし扱いにくいので、ファミリー〈集…

カプチ／マイヤース〈Matteo Capucci, David Jaz Myers〉のコンテキスタッドは、最近の記事「コンテキスタッドかぁ、ウーム‥‥」で紹介しました。依存アクテゴリーと呼ばれていた頃（2023年末）から注目はしていましたが（「依存アクテゴリーが面白い」参照）…

モナドや随伴系〈adjunction | adjoint system〉が見つかると良いことあります*1。なので、モナドや随伴系を頑張って探すわけです。相対モナド／相対随伴系は、より一般性がある構造です。もちろん、見つかると良いことあります。しかし、相対モナド／相対随…

前回（昨日）、長い記事「形式言語理論にも使える導出系」を書きました。いつものことで、熟考したわけではなくて勢いで書いています。読み返すと気になる点がすぐに見つかります（でも、もとの記事は修正しません）。この記事で、前回記事に対する反省と課…

演繹、推論、導出、証明などと呼ばれる行為を形式的に遂行する概念的システムは色々な場面で色々な呼び名で出てきます。ここでは、それらのシステムを総称して導出系〈derivation system | 導出システム〉と呼ぶことにします。論理や型理論だけではなく、形…

2024年の春に、依存アクテゴリー〈dependent actegory〉に関する一連の記事を書きました。 ハブ記事： 環境付き計算と依存アクテゴリー 1/n 依存アクテゴリーは、マッテーオ・カプチとディビッド・ジャズ・マイヤースの発案による圏論的構造です。2023年時点…

圏または圏類似代数系〈category-like algebraic {system | structure}〉を対象とする圏において、既存の対象（圏または圏類似代数系）にk-射（k = 0, 1, 2, ...）の集合を付け足して拡張できるか？ という問題を考えます。この問題に肯定的に答えられるとき…

「帰納的型とリカーサー」と「帰納原理を完全に書き下す」において、自然数上の帰納原理について述べました。自然数に限らない一般的な帰納構造に対する帰納原理について述べます。帰納原理を確認したい動機は、形式体系の健全性〈soundness〉を証明するとき…

プロ関手 $`\mathcal{C}^{\mathrm{op}}\times \mathcal{D} \to \mathbf{Set}`$ の方向を「$`\mathcal{C}`$ から $`\mathcal{D}`$」とするか、はたまた「$`\mathcal{D}`$ から $`\mathcal{C}`$」とするかは好みの問題でその選択は恣意的です。僕は、「$`\math…

「離散」と「微分」は相容れない概念です。「離散微分幾何」は意味不明もいいとこ。実は、離散微分は差分のことです。ですから「差分幾何」でもよいのですが、「離散微分幾何」のほうが「なんじゃそれ？」感によるインパクトがあります。離散微分幾何のひと…

「おー、$`\Delta`$ と $`\nabla`$ を組み合わせたら $`\diamondsuit`$ になるな、むふふふふ」と、ダジャレな記法を思いついて悦にいっている今日このごろ。何の話かというと； カリー／ハワード／ランベック対応によれば、型と命題は事実上同じものなので…

この記事の目的は二つあります。一つめは、相対モナドの簡単で面白い例を提供すること。二つめは、図式順記法のプロモーションです。図式順記法を使えば気持ち良く計算が出来るよ、とアピールしたい。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm…

随伴系〈adjunction | adjoint system〉は左関手と右関手のペアとして、$`F \dashv U`$ のように書かれることが多いですが、これらは随伴系という構造の下っ端なヤツラです。注目すべきは、以下のモノとコトです。$`\newcommand{\cat}[1]{\mathcal{#1}} \new…

次の記事達の続きです。 アドホック随伴系と自由対象・台対象 アドホック随伴問題と自由対象の求め方 アドホック随伴系は、自由-忘却・随伴系の自由関手が欠如した“随伴系もどき”だと説明しました。しかし、より正確に言うなら、自由関手は欠如しているので…

随分と時間（21ヶ月ほど）がたっていますが、この記事は「アドホック随伴系と自由対象・台対象」の続きです。アドホック随伴系とは、自由-忘却・随伴系〈free-forgetful adjunction〉の自由関手が欠如したものです。それは結局、単一の関手があるだけなので…

このブログ内で「反射的球体集合」を検索したらヒットしない。「えっ？」と思いました。てっきり書いたことあると思い込んでた。書いてないなら書きましょう、この記事で。毎度の悩みの種である反対圏と反変関手に関するゴタゴタと、関手の域圏と余域圏の混…

クラン（クラン、ファイブレーション、スパン）に、バート・ジェイコブスの意味での包括構造（「拡張包括構造のもうひとつの定式化」参照）を載せると包括クラン（「テレスコープと包括クラン」参照）になります。包括クランは、型理論の圏論的定式化の基本…

圏と関手の小ネタ。boo は bijecton on objects の頭文字です。二文字 bo を使うこともあります（nLab は bo）。ff は full and faithful の頭文字です。(boo, ff)-分解〈(boo, ff)-factorization〉は、関手 $`F:\mathcal{C}\to \mathcal{D}`$ を、boo部分と…

自然数全体の集合を $`\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…