高次圏論へのアプローチ（使用する方法論・手法）には色々なものがあります。 単体アプローチ〈simplicial approach〉 球体アプローチ〈globular approach〉 方体アプローチ〈cubical approach〉 オペトープ・アプローチ〈opetopic approach〉 樹形体アプロ…

用語・用法図は「パンダ用法と用語・用法図」で導入した図／図解法です。この記事で、用語・用法図の辺に付けるラベルを増やすことにより、用語・用法図を知識グラフにまで拡張します。知識グラフはその名の通り、知識の記述や分析に効果的に使用できます。…

「パンダ用法： 流転する呼称」において、「パンダ」という言葉の解釈がややこしいことを説明しました。「パンダ」のようにややこしい言葉は他にもあります。過去記事では「非可換環」を挙げました。「大きい集合」や「境界付き多様体」なども同様にややこし…

グロタンディーク宇宙は、フォン・ノイマン宇宙（ZFC集合論の宇宙）のなかの“ある種の代数系（演算を備えた集合）”だと考えられます。代数系としてのグロタンディーク宇宙での計算には、通常のラムダ計算が使えます。なぜなら、外側のフォン・ノイマン宇宙か…

「ホーア論理とホーアオートマトン 8/n ： ローヴェア、ゴグエン、ホーア、メイヤー // 造花は花か？」にて： レッドヘリングを口頭で説明するために、僕はパンダの話をしたり（昔は「パンダ＝レッサーパンダ」だった、とか）するのですが、今回は「花と造花…

タルスキー／グロタンディーク集合論〈Tarski-Grothendieck set theory〉は、現在の標準的集合論であるZFC集合論に宇宙公理を加えた体系内で解釈可能な、より使い勝手を良くした集合論です。タルスキー／グロタンディーク集合論は、圏論や依存型理論の基盤と…

AIコーディングエージェントの登場により、“狭い意味でのコーディング”はAIに任せられるようになりました。しかし、次の作業はまだ人間がやったほうがよさそうです。 プログラムの仕様の記述 テストの設計・計画 人間が、プログラムの仕様を記述して、テスト…

「AI支援形式証明への道」は、記述が断片的で分かりにくかったと思うので補足をします。そして、Comet を使って色々試している現状を報告します。内容： Comet について 僕の想定 Comet との経緯 今はこんな感じ オマケ： 絵図証明 関連記事： Perplexity Co…

ジャズ・マイヤース〈David Jaz Myers〉が、Categorical Systems Theory のなかで、「アリーナの二重圏」という概念を定義しているのですが、なんだかピンとこない。実例を考えてみました。具体的な状態遷移系をタイト射とする二重圏です。この具体的な状態…

名前の解釈をちゃんとしよう -- と、口頭では何百回も言った気がするのですが、ちゃんと書いたことはなかったので、この記事にまとめておきます。名前を正確に解釈せずにボヤッとした印象で済ませてしまう癖を矯正するのは難しいですね。それが、何百回も言…

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

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

表題の話題については過去に書いているのですが、改めて何回かの記事に分けて書こうかと思います。過去記事を参照〈リンク〉はしますが、参照をたどらなくても済むように出来るだけ自己充足的〈self-contained〉なスタイルにします。「出来るだけ」ですけど…

古典テンソル計算は何度も話題にしていますが、不満や愚痴として僕がよく言っていたことは； 「計算の手順だけ教わって、それを機械的に遂行するのは辛い」てなことです。しかしこれは、言葉を換えると、機械的な計算手順だけでも（セマンティクスをろくに知…

「カン拡張ラムダ計算化計画」より： この記事ではこれ以上の内容は述べませんが、引き続く記事達でカン拡張ラムダ計算化計画をちょっとずつ実行する予定です。 というわけで、ちょっと書きます。内容： 使う道具・技術・枠組み 使う具体例 関連する過去記事…

カン拡張とラムダ計算の関係をはじめて意識したのは2013年のことです。以下の記事に書いてあります。 右カン拡張が、自然変換のラムダ計算における指数型らしい件 次の絵が2013年記事にあります。このとき、次のようなことを言ってます。 runは自然変換です…

「バエズ／ドーラン茂みとリントン／ローヴェア・モナド」と「多項式関手とスケマティックなリントンの定理」において、「たわ言かも知れない」「与太話かも知れない」「怪しい話」を書いていて、出来ればちゃんとした話にしたいと思っているわけです。その…

「ローヴェア・セオリーのモデルの圏と、ローヴェア・セオリーに対応するモナドのアイレンベルク／ムーア圏が圏同値である」という結果は、リントン〈Fred Linton〉が示したのだと僕は思っていました。しかし、リントンのオリジナルの論文 "Some aspects of …

指標は宣言文の集まりです。各宣言文は、順番〈位置番号〉でも名前でも一意識別できます。実用上は、（順番は覚えにくいので）名前が使われます。が、理論上は名前が邪魔になることがあるので、ときに、名前を削除する必要があります。名前の削除方法の記述…

同義語・多義語の問題について過去3回の記事で述べました。 同義語・多義語にホトホト困っている 同義語・多義語の問題（続き） 同義語・多義語の問題： タグによる修飾と分類 同義語・多義語の問題は、正確なコミュニケーションにとっては深刻な障害となり…

[追記]「論理計算のための宇宙と型 補遺」に続きがあります。[/追記]型理論と圏論の言葉は次のように対応します。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\mfk}[1]{ \mathfrak{#1} } \newcommand{\In}{ \text{ in } }`$ 型理論 圏論 型 対象 型…

「指標の話： 形状の記述と形状付き集合」において、形状付き集合について述べました。よく使われる形状付き集合に球体集合〈球体的集合〉があります。球体集合達の圏の部分圏（有限な球体集合達）に対して、その構文表示を考えましょう。圏の構文表示とは、…

以下の論文、タイトルを見て興味をそそられました。が、「んっ？ 思ってたのと違う」となりました。コンピュータッドも指標も僕が知っているコンピュータッド／指標とは定義が異なるのです。が、冷静になって考えると「あっ、やっぱり同じか」となりました。…

圏のスパンの全体は、プルバックを使って圏にすることができます。スパンの左脚と右脚に制約を付けても圏を構成できるときがあります。こうして作った制約付きスパンの圏が役に立つことがあります。$`\newcommand{\mrm}[1]{ \mathrm{#1} } \newcommand{\cat}…

最近の応用圏論〈ACT | Applied Category Theory〉では、モノイド圏、アクテゴリー、二重圏、三重圏などの複雑な構造を平気で使います。このような複雑な構造を扱うときは、名前に十分な注意をはらう必要があります。複雑な構造でなくても、名前に十分な注意…

随伴系、モナド、モナドのアイレンベルク／ムーア代数、自己関手のランベック代数、ベックの分配法則などを扱っていると、こういうモノ達を系統的に組織化したい、という気持ちになります。代数的構造の組織化のためには、ゴグエン／バーストル〈Joseph Gogu…

カプチ／マイヤース〈Matteo Capucci, David Jaz Myers〉の依存アクテゴリーは、アクテゴリーと二重圏の中間にある、ほど良い感じの概念的フレームワークです（「依存アクテゴリーが面白い」参照）。まだ定義さえハッキリしない状態ですが、僕は期待してます…

“ファイバーの計算”（「ファイバーの計算 基本概念」参照）に関する一連の記事のひとつとして、木と林の話を書き始めたのですが、独立した話題として扱えるので、シリーズ記事からは外れた記事にします。木と林は有向グラフの種類のことで、現実世界の植物の…

バタニン／マークル〈Michael Batanin, Martin Markl〉のオペラディック圏は、オペラッドを定義するための道具ですが、“ファイバーの計算”を抽象化したものだともみなせます。この記事では、抽象化する前の具象的な“ファイバーの計算”、つまり集合圏の部分圏…

レナート・ベッチ／ロバート・ウォルターズ〈Renato Betti, Robert F.C. Walters〉のとある論文を眺めていて、カン拡張／カン持ち上げの記述で戸惑ってしまいました。右カン持ち上げだと記されていたペースティング図が間違っていて左カン持ち上げになってい…