カプチ／マイヤース〈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部分と…