ヒルベルトのイプシロン記号は、集合からその要素を気まぐれに（まったく予測できないスタイルで）取り出す操作です。ヒルベルトのイプシロン記号が便利な場面や必須な場面があります。しかし、ヒルベルトのイプシロン記号に空集合を渡したときの挙動がよく…
形式化された議論であれ非形式的〈インフォーマル〉な議論であれ、命題と規則を区別する必要はあります。「型理論と論理： 非形式シーケント記法 // 規則は命題ではないのだが」において、規則は命題ではないと言ったのですが、混同されるのはそれなりの理由…
あー、そういうことかぁ！僕は、用語の語源にあまりこだわらないので、「包括圏」の語源は知らなかったし、調べることもしませんでした。「なんでか知らんけど、『包括圏』って呼ぶのね」で済ませていました。語源や逸話を知らないと概念を理解できないわけ…
「型理論周辺、何で混乱するのか？」において： 型理論／論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです 地雷原になってしまう大きな理由に、ターンスタイル記号 '$`\vdash`$'、二重矢印 '$`\R…
どこに引っ越すのか？ それは“コンテキスタッドの世界”への引っ越しです。コンテキスタッドが型理論／論理／インスティチューション理論に対して、統合的・整合的な枠組みを与えるだろう、と思っています。それは、最近の記事達の内容や動機になっています。…
型理論周辺の用語・記法・説明が混乱誘発的〈confusing〉で、それは僕の長年の悩みの種です。型理論／論理／形式言語理論／インスティチューション理論などを学ぶのは、ハマリ所だらけで地雷原を歩くようなものです*1。最近、包括コンテキスタッド（「型理論…
包括圏とコンテキスタッドの組み合わせは、型理論やインスティチューション理論に向いているようです（「型理論とコンテキスタッド： コンテキストフル射」参照）。この記事では、包括コンテキスタッド（包括圏とコンテキスタッドの組み合わせ）を定義し利用…
集合 $`X`$ 上の方程式が与えられたとき、その解集合（空集合でも $`X`$ 全体でも、なんであれ）は一意に決まると我々は信じています。しかし、トポスのなかで方程式を考えると、解集合（に相当する解対象）は一意に決まることは保証されません。これって、…
圏の恒等射だけで部分圏ができます。が、この部分圏はファイブレーションクラスにはなりません。包含的圏（「色々な包含的圏」参照）の包含射達は部分圏を形成しますが、これもファイブレーションクラスにはなりません。圏のファイブレーションクラスの定義…
「名前の解釈： 正確なコミュニケーションのために」、「名前の解釈 その2」の続きです。$`\newcommand{\In}{\text{ in }} \newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right] } \newcommand{\hyp}{ \text{－} } \newcommand{\mbf}[1]{ \mathbf{#1}…
「名前の解釈： 正確なコミュニケーションのために」の続きです。$`\newcommand{\In}{\text{ in }} \newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right] } \newcommand{\hyp}{ \text{－} } \newcommand{\mbf}[1]{ \mathbf{#1} } \newcommand{\mrm}[1…
名前の解釈をちゃんとしよう -- と、口頭では何百回も言った気がするのですが、ちゃんと書いたことはなかったので、この記事にまとめておきます。名前を正確に解釈せずにボヤッとした印象で済ませてしまう癖を矯正するのは難しいですね。それが、何百回も言…
カプチ／マイヤース〈Matteo Capucci, David Jaz Myers〉のコンテキスタッド（「コンテキスタッド、包括圏、ハイパードクトリン」参照）は、型理論と思いのほか相性がいいようです。ちょっと驚いています。型理論的概念である包括圏を、テレスコープ構成によ…
「色々な包含的圏」において、包含的圏の変種を6種類定義しました。圏の対象達全体の集合に載る大域的な構造と、各対象ごとに構成できる局所的な構造の2つの観点から分類しています。この記事では、包含的圏（の変種）の事例であり、同時に誤解しやすい点に…
包含的圏〈inclusive category〉の定義は人により色々です。型理論やインスティチューション理論に使うことを目的にして、包含的圏に関して整理しておきます。$`\newcommand{\cat}[1]{\mathcal{#1}} \newcommand{\mrm}[1]{\mathrm{#1}} \newcommand{\mbf}[1]…
「導出系： 反省と課題 // ソート付き集合の圏は変わる」において、ソート付き集合達の圏 $`\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〉の自由関手が欠如したものです。それは結局、単一の関手があるだけなので…
