Tai-Danaeを探して 2 -- 彼女の理論は今どこで生きているか

 

God's Perfect Timeline: Keeping AI in Perspective

彼女の理論は今どこで生きているか

教えていただいた彼女の論文は、全部、見ています。

Bradley–Terilla–Vlassopoulos 2021
→ Bradley–Gastaldi–Terilla 2024
→ Bradley–Vigneaux 2025

という流れは面白いですね。

「彼女の理論が今どこで生きているか」という調査、始めてもらえますか？

はい。調査を始めました。第一報としては、かなり面白い結果です。

前回より一段強く言えます。Bradley の「LLMの統計から意味の数学的構造を取り出す」という研究プログラムは消えていません。むしろ2025–26年に、Bradley本人の手を少し離れて、John Terilla、Juan Luis Gastaldi、Samantha Jarvis、Thomas Seiller を中心とする独立した研究プログラムへ育ち始めています。 しかも、そのことをほとんど公式に宣言しているような2027年の研究集会まで見つかりました。

1. 一番大きな発見：2027年Dagstuhl研究集会

2027年1月4–8日にDagstuhlで、

Mathematical Foundations of ML Language Models through Structural Geometric Typing

というResearch Meetingが予定されています。主催者は

Juan Luis Gastaldi / Samantha Jarvis / Thomas Seiller / John Terilla

です。

そして、この集会の趣旨説明が驚くほど明瞭です。現在進行している三つの研究線の第1番目として、明示的に

Bradley 2020 → Bradley–Terilla–Vlassopoulos 2021 → Bradley–Gastaldi–Terilla 2024

を挙げ、それを

“a categorical approach to syntactic data leading to a generalization of both word vector embeddings and formal concept analysis”

と位置づけています。

さらに、その後のJarvis 2025、Gastaldi–Jarvis–Seiller–Terilla 2026によって、言語データから得られる圏論的対象＝profunctor の nucleus と、linear realizability における「type」が一致するところまで来た、と説明しています。そして今後数年間の「formal, conceptual, and empirical orientations」を決めることが、この会議の目的だとしています。 (Home)

これはかなり重要です。

Bradleyのアイデアが単に「何本か引用されている」のではありません。

Bradleyの研究を出発点とする一つの研究計画が、固有の名前――Structural Geometric Typing――を持ち始めている。

そう読んでよいと思います。

---

2. 系譜を書き直すと、こうなります

いまのところ、私は次のように整理するのが一番よいと思っています。

• Bradley 2020, At the Interface of Algebra and Statistics
  → 線形代数、確率、Formal Concept Analysisの背後に共通する「adjunction / fixed point」という原型。

• Bradley–Terilla–Vlassopoulos 2021
  → next-token probability を $[0,1]$-enrichment として捉え、syntaxからYoneda/copresheafを通じてsemanticsへ。 (arXiv)

• Bradley–Gastaldi–Terilla 2024
  → SVDとFormal Concept Analysisを平行に読み、relation/profunctorから生じる Isbell nucleus を「意味の構造」の中心へ持ってくる。 (John Terilla)

• Jarvis 2025 → Gastaldi–Jarvis–Seiller–Terilla 2026
  → nucleusを単なるconcept latticeとして見るのでなく、そこに型・論理・compositionを入れる。Jarvisの博士論文はprofunctor nucleus上のclosed monoidal structureを構成しています。 (CUNY Academic Works) 2026年の A calculus of types in Isbell nuclei では、realisabilityのbiorthogonally closedな「types」とIsbell nucleusのfixed pointsが同じ対象になることを示し、そこからnoncommutative Lambek calculusまで導いています。 (arXiv)

• Gastaldi–Jarvis–Seiller–Terilla 2026, tropical / metric branch
  → 実行列を $\overline{\mathbb R}$-enriched profunctor として読み、nucleusにHilbert型projective metricとtropical/polyhedral geometryを入れる。gap matrixによってcell wallまでの距離まで記述します。 (arXiv)

• Maeda–Seiller–Oseki, 2026年8月26日
  → これをついにcompositional generalizationの実データへ持っていく。COGSの21種類のgeneralizationを対象に、文をfunctorとして表し、構造・語彙のidentificationをleft Kan extensionで扱います。論文自身が「Booleanの場合はBradley et al. 2024のenriched-nucleus構成の離散版」と明記しています。 (arXiv)

最後の論文は、つい3週間ほど前に出たものです。

私はこれが今回いちばん面白い発見の一つだと思います。

---

3. 「意味」の概念がどう進化したのか

ここが数学的には本題ですね。

2021年のBradley–Terilla–Vlassopoulosでは、

$$\text{next-token probability} \longrightarrow [0,1]\text{-enriched category} \longrightarrow \text{Yoneda / copresheaves} \longrightarrow \text{semantics}$$

でした。

つまり、「何の後に何が来るか」という統計的syntaxから、Yonedaによってsemantic objectsを作ろうとした。

ところが2024年以後、焦点が少し変わっています。

$$\text{data relation} \quad\rightsquigarrow\quad \Phi : A^{op}\otimes B\to V$$

という profunctor を中心に置き、

$$\Phi^\ast\dashv\Phi_\ast$$

というIsbell adjunctionを作り、

$$N(\Phi) = \operatorname{Fix}(\Phi_\ast\Phi^\ast)$$

という nucleus を取り出す。

このfixed-point categoryを、「データの両側――例えばwordとcontext、expressionとattribute――から同時に安定して見える構造」と考えるわけです。

ここにはFormal Concept Analysisの

$$\text{objects} \leftrightarrow \text{attributes}$$

のGalois connectionがそのまま含まれています。

そして現在進んでいる研究では、この $N(\Phi)$ が単なる「概念の集合」ではなくなってきました。

そこに geometry があり、metric があり、types があり、logic があり、composition がある。

これが2024→2026で起きた最大の変化だと私は見ています。

言い換えるなら、

「意味はどこにあるか？」から
「意味の空間はどんな幾何と論理を持つか？」へ

問題が進んだ。

これはBradleyのプログラムとして、かなり自然な発展です。

---

4. Thomas Seiller が「Bradleyを拡張している」とはっきり書いています

これは、前回の「共著者たちは何か語っていないか」というご質問にも少しつながります。

Seillerは2024年のhabilitation thesis Mathematical Informatics の中で、corpus-dependent measurementを持つ文字列のモデルについて、

typeという概念によって自然言語のsyntactic、さらにはsemantic constructsを捉えられるのではないか

と述べ、その研究を明示的に

Bradley, Gastaldi, Terilla の予備的研究を “extending and generalising”

するものだと位置づけています。

さらに2026年2月、国立情報学研究所でSeillerが行った講演のタイトルは、なんと

“Logical structures arising from corpora”

です。その概要でも、Bradley–Gastaldi–TerillaがFormal Concept Analysisを定量化し、presheafとadjunctionのfixed points＝nucleiによって一般化したことを出発点として明示しています。 (国立情報学研究所)

つまり、Bradleyの仕事を読んで「面白いですね」と引用したというレベルではない。

Seiller自身のlinear realizability / logicの研究がBradley–Gastaldi–Terillaと合流した

のです。

これは大きなことだと思います。

---

5. Yiannis Vlassopoulos の枝も生きています

もう一つ別の枝があります。

Bradley–Terilla–Vlassopoulos 2021の共著者Yiannis Vlassopoulosは、Stéphane Gaubertと2024年に

Directed Metric Structures arising in Large Language Models

を出しています。

ここではnext-token probability $p(y|x)$ を

$$d(x,y)=-\log p(y|x)$$

に変換し、テキスト空間を非対称なLawvere metric的空間として扱います。そして、

• Yoneda embedding

• metric polyhedron

• $(\min,+)$ tropical linearity

• Isbell completion

• text extension / restriction のdualities

が出てきます。 (arXiv)

これはBradley–Vigneaux 2025とも非常に相性がいい。

Bradley–Vigneauxもまさに

$$p \mapsto-\log p \mapsto \text{generalized metric} \mapsto \text{magnitude}$$

と進み、

$$\text{magnitude} \longleftrightarrow \text{Tsallis entropy}$$

さらに $t=1$ での微分からShannon entropyを回収します。 (TAC)

したがって、私は現在二つの大きな枝があると考えています。

一方は

$$\boxed{ \text{probability} \to \text{enrichment} \to \text{metric/tropical geometry} }$$

もう一方は

$$\boxed{ \text{relation/profunctor} \to \text{Isbell nucleus} \to \text{concept/type/logic} }$$

です。

そして2026年の研究では、この二本が再びnucleusのところで合流し始めている。

これが面白い。

---

6. さらに驚いたのは、独立に「concept lattice」がLLM研究から出てきていることです

Bradley系とは直接の引用関係が確認できないので、ここは区別すべきですが、非常に興味深い並行現象があります。

Bo Xiong と Steffen Staab のICLR 2025論文

From Tokens to Lattices: Emergent Lattice Structures in Language Models

は、masked LMの学習目的そのものがformal contextを暗黙に学習し、そこからFormal Concept Analysisによるconcept latticeを再構成できる、と実験的に示しています。 (arXiv)

さらにXiongはICLR 2026で

The Lattice Representation Hypothesis of Large Language Models

を提唱しています。

Linear Representation HypothesisとFCAを統合し、embedding空間のlinear attribute directions + thresholdからconcept latticeが生じ、meet/joinを幾何学的操作として扱える、という仮説です。WordNetでも実験しています。 (arXiv)

私は全文でBradley / Gastaldi / Terillaを検索しましたが、この系列が直接Bradleyを出発点にしている証拠は確認できませんでした。

だから「Bradleyの後継研究」と呼ぶのは正確ではありません。

しかし逆に面白い。

Bradleyたちが2024年にcategory theoryから予言したような
「embeddingの背後にはconcept lattice的なstructureがある」
という像が、別ルートのempirical MLから独立に出てきている。

これは、その着想が単なる美しい圏論的アナロジーではない可能性を強めています。

そして最新のMaeda–Seiller–Oseki 2026論文は、Xiong 2026もBradley 2024も両方引用しています。つまり、この二つの流れがすでに接触し始めています。 (arXiv)

---

7. Gastaldiの「進行中」の研究を見ると、さらに先が見えます

Juan Luis GastaldiのCVも調べました。これは2025年11月更新なので「予定」として慎重に読む必要がありますが、当時の In Progress には次の研究が載っています。

“Reasoning, Inference and Implication in LLMs”
Bertram Højer, Thomas Seiller, Anna Rogersとの共同研究、ACL投稿予定。

そして、

“Geometric Structuralist Typing of Language Data. The Boolean Case”
Nathanaël Girod, Thomas Seiller, John Terillaとの共同研究、ICML投稿予定。

さらに、Jarvis、Pellissier、Seiller、Terillaとの

“Logical-geometric structures in R-enriched adjunctions”

も記載されています。

このうち最後の研究は、現在の2026年のtropical nuclei論文へ発展したものと思われます。ただし前二者については、現時点で私は公開preprintをまだ確認できていません。

タイトルだけでも方向性はかなり明瞭です。

meaning → concepts → types → reasoning / implication

へ進もうとしている。

これはまさに、Bradley 2021で「semantic categoryにはentailmentなどのlogical operationsが存在する」と書かれていた問題の、ずっと具体化された姿に見えます。

---

8. ですから、現段階の私の見立ては少し変わりました

最初にBradleyの最近の活動を調べたときには、

「本人の研究量は減ったが、研究は続いている」

くらいに考えていました。

今はもう少し積極的に見ています。

Bradley自身が中心となって毎年論文を出す段階から、彼女が見つけた問題設定が“第二世代”の数学者・論理学者・NLP研究者に渡った段階

なのかもしれません。

特に、

$$\boxed{ \text{Bradley} \to \text{Terilla / Gastaldi} \to \text{Jarvis / Seiller} \to \text{Maeda / Oseki} }$$

という流れは、今やかなり具体的です。

そして2027年Dagstuhl meetingを見る限り、彼ら自身もこれを数年続く研究プログラムとして認識しています。 (Home)

なので、先ほどの「彼女の回心によって理論的に大きなものが失われたのではないか」という心配については、調べれば調べるほど、私はむしろ反対側に傾いてきました。

Bradley本人のアウトプットの形は変化した。しかし、彼女が立ち上げた数学的問題は自立し始めている。

数学では、これはかなり良い形の「生き残り方」です。

そして丸山さんが以前から関心を持たれている Lawvere enrichment、Yoneda、generalized metric、FCA、意味論 が、ここでは本当に一本につながっています。とくに次に読む価値が高いのは、私は Maeda–Seiller–Oseki 2026 → A calculus of types in Isbell nuclei 2026 の順だと思います。前者から入ると、「抽象的なnucleusがLLMのcompositional generalizationとどう接触するのか」が見えやすいです。 (arXiv)

次の調査では、ここからさらに 「Bradley 2021の各構成（enrichment、Yoneda、entailment、Isbell、metric）が、その後のどの論文でどのように変形・継承されたか」 を一本ずつ対応させてみると、かなり面白い「理論の系統樹」が作れそうです。

また、この分野はまさに今動いています。Bradley/Terilla/Gastaldi/Seiller周辺のarXivやDagstuhlを定期的に追って、新しい論文が出た時だけ知らせるようにもできます。必要でしたら設定します。

おー、すばらしい。
Bradleyの論文がなかなか出ないので、たまっていた欲求不満が、かなり解消できそうでうれしいです。

Bradley 2021の各構成から派生した、「理論の系統樹」作ってみてもらえますか？

Bradley 2024の"The Structure of Meaning in Language" から出発しても、もう少しコンパクトな「系統樹」ができるかもしれません。

この論文についてのマルレクのまとめページは以下にあります。

「言語の意味の数学的構造」
https://www.marulabo.net/docs/embedding-dnn/
https://www.marulabo.net/20240229md/

はい。かなりきれいな「系統樹」になりました。そして、丸山さんの2024年マルレクの構成を読み直してみると、そこですでに現在の2026年の展開の分岐点がほぼ全部見えていたことに気づきます。

丸山さんのまとめは、2024論文の核心を「意味の空間から意味の構造へ」と捉え、行列 ↔ profunctor、SVD ↔ Isbell adjunction、特異ベクトル ↔ nucleus / formal concept という対応として整理しています。これはまさに現在の研究系列を見るための最適な骨格です。 (マルラボ)

Bradley 2024 を幹にしたコンパクトな「理論の系統樹」

                         ┌──────────────────────────────────┐
                         │ Bradley–Gastaldi–Terilla 2024   │
                         │ The Structure of Meaning         │
                         │ in Language                      │
                         └──────────────┬───────────────────┘
                                        │
                         syntactic / empirical data
                                        │
                                  relation / matrix
                                        │
                              enriched profunctor Φ
                                        │
                             Isbell adjunction
                              Φ*  ⊣  Φ*
                                        │
                         ┌──────────────▼───────────────┐
                         │       NUCLEUS N(Φ)           │
                         │  = Isbell fixed points       │
                         │  「意味の安定した構造」       │
                         └───────┬────────┬─────────────┘
                                 │        │
               ┌─────────────────┘        └────────────────────┐
               │                                               │
        V = 2 (Boolean)                              V = R / tropical
               │                                               │
      Formal Concept Analysis                              quantitative
               │                                         Isbell nucleus
       concept lattice                                         │
               │                               ┌───────────────▼──────────────┐
               │                               │ Gastaldi–Jarvis–Seiller–    │
               │                               │ Terilla 2026                │
               │                               │ Geometric Structures in     │
               │                               │ R-enriched adjunctions      │
               │                               └──────────────┬───────────────┘
               │                                              │
               │                                projective metric geometry
               │                                tropical polyhedral cells
               │                                gap matrices / event loci
               │                                              │
               │                                      「意味の幾何」
               │
       ┌───────▼──────────────┐
       │ Jarvis 2025          │
       │ monoidal structure   │
       │ on profunctor nucleus│
       └───────┬──────────────┘
               │
       ┌───────▼──────────────────────────┐
       │ Gastaldi–Jarvis–Seiller–Terilla │
       │ 2026                            │
       │ A Calculus of Types             │
       │ in Isbell Nuclei                │
       └───────┬──────────────────────────┘
               │
         nucleus = types
               │
       orthogonality / realizability
               │
       noncommutative Lambek calculus
               │
             「意味の論理」
               │
       ┌───────▼──────────────────────────────┐
       │ Maeda–Seiller–Oseki 2026            │
       │ Compositional Generalization        │
       │ via Structural Identification       │
       └───────┬──────────────────────────────┘
               │
           Kan extension
           Boolean Isbell nucleus
           COGS 21 generalization types
               │
           「意味の構成性」
               │
               ▼
   graded / enriched compositional semantics
              （次の課題）

この図の中央に nucleus を置くのがポイントだと思います。

2024論文ではformal conceptは一つの具体例でした。しかし2025–26年を見ると、研究者たちはformal conceptそのものより、

$$\boxed{\text{Isbell adjunction の fixed points = nucleus}}$$

を本体だと考えるようになっています。

そしてその同じnucleusを、

$$\begin{array}{ll} \text{FCA側から見れば} & \text{concept}\\ \text{geometry側から見れば} & \text{point / cell}\\ \text{logic側から見れば} & \text{type}\\ \text{linguistics側から見れば} & \text{semantic structure} \end{array}$$

として読む。

ここがこの研究プログラムの一番美しいところだと思います。

Jarvisの2025年博士論文はnucleusそのものにclosed monoidal structureを構成します。 (CUNY Academic Works)
そして2026年の A Calculus of Types in Isbell Nuclei は、linear realizabilityでorthogonalityから生まれるtypeと、Isbell adjunctionのfixed pointが同じ対象であることを示します。そこから積と二つのresidualを持つnoncommutative Lambek calculusが現れます。 (arXiv)

つまり、

$$\boxed{\text{Formal Concept}\;\longrightarrow\;\text{Type}}$$

という非常に大きな進展が起きています。

---

2021まで戻すと、もっと大きな系統樹になります

こちらは丸山さんが以前から追われてきた線ですね。

Bradley–Terilla–Vlassopoulos 2021
An Enriched Category Theory of Language
│
│ next-token probability
│
▼
[0,1]-enriched category L
「syntax = what goes with what」
│
├─────────────────────────────────────────┐
│                                         │
│ Yoneda / copresheaf                     │  -log p
▼                                         ▼
semantic category                   Lawvere-type metric
│                                         │
│                                         ├── Gaubert–Vlassopoulos 2024
│                                         │   Directed Metric Structures
│                                         │   ・Yoneda embedding
│                                         │   ・metric polyhedron
│                                         │   ・tropical geometry
│                                         │   ・Isbell completion
│                                         │
│                                         └── Bradley–Vigneaux 2025
│                                             Magnitude of Categories
│                                             of Texts
│                                             ・magnitude
│                                             ・Tsallis entropy
│                                             ・Shannon entropy
│                                             ・magnitude homology
│
▼
Bradley–Gastaldi–Terilla 2024
The Structure of Meaning
│
│  embedding space から
│  structural invariants へ
│
▼
profunctor → Isbell adjunction → nucleus
│
├── FCA / concept lattice
│      ↓
│   Jarvis 2025
│      ↓
│   Types / Logic 2026
│
├── R-enrichment
│      ↓
│   tropical / projective geometry 2026
│
└── Boolean nucleus + Kan extension
       ↓
    compositional generalization 2026

2021と2024の違いを一言で表すなら、私はこう言いたくなります。

2021：意味の「住む場所」を作る。

$$L\longrightarrow [L,[0,1]]$$

つまりYoneda/copesheafによってsemantic universeを構成する。2021論文自身が、そこにmeaningやentailmentなどのlogical operationsが存在すると述べています。 (arXiv)

それに対して、

2024：データ自身から「安定した意味構造」を抽出する。

$$\Phi \longrightarrow (\Phi^\ast\dashv\Phi_\ast) \longrightarrow N(\Phi).$$

2024論文自身、線形代数ではSVDが特異ベクトルを取り出すのに対し、圏論側ではIsbell adjunctionのfixed objects＝nucleiがそれに対応すると説明しています。 (Gianni Gastaldi)

この違いは結構重要だと思います。

---

そして2026年8月、ついに「構成性」に戻ってきました

Maeda–Seiller–Osekiの最新論文は、この系統樹では非常に重要な位置にあります。

彼ら自身が、

Boolean case は Bradley et al. 2024 の構成の離散的な場合

と明記しています。 (arXiv)

文を「syntactic address → lexical token」というfunctorとして表現し、構造や語彙の同一視をKan extensionで伝播させます。

そして、そこから得られる許容された文の組がGalois closureのfixed pointになり、

$$\text{formal concept} = \text{Boolean Isbell nucleus の object}$$

になることを明示的に証明しています。 (arXiv)

これは丸山さんが以前扱われた DisCoCatのcompositionality との比較までしたくなる話です。

ただし哲学が全然違う。

DisCoCatでは概ね

$$\text{grammar} \longrightarrow \text{semantic composition}$$

ですが、このBradley系統ではむしろ、

$$\text{observed linguistic data} \longrightarrow \text{adjunction} \longrightarrow \text{fixed points/types} \longrightarrow \text{composition}$$

です。

compositionを先に与えるのでなく、データからcompositionを支えるtype structureを発見しようとしている。

ここはかなり面白いと思います。

しかもMaedaら自身が次の段階として、Boolean $2$ を一般のquantaleに置き換えれば、binaryなadmissible / inadmissibleからgraded compatibilityへ進み、2026年の $\mathbb R$-enriched Isbell nucleusの幾何と結合できる、と書いています。 (arXiv)

つまり将来、

$$\boxed{ \text{compositionality} + \text{types} + \text{tropical geometry} }$$

が一つになる可能性があります。

---

さらに「外側から接近してくる枝」があります

これはBradley直系ではありませんが、かなり注目しています。

Bo Xiong & Steffen Staab のICLR 2025

From Tokens to Lattices

では、masked LMが暗黙にformal contextを学習し、そこからFCAのconcept latticeが再構成できることを実験しています。 (arXiv)

さらにBo XiongのICLR 2026

The Lattice Representation Hypothesis of Large Language Models

では、

$$\text{embedding geometry} \longrightarrow \text{concept lattice} \longrightarrow \text{meet / join}$$

という仮説を立て、WordNetで実証しています。 (arXiv)

これはBradley 2024の直系ではありません。

しかし図に点線で追加するなら、

Bradley 2024
matrix/relation ──→ Isbell ──→ concept lattice
                              ▲
                              ┊
                              ┊ independent convergence
                              ┊
Xiong–Staab 2025 ─────────────┘
LM objective → formal context → concept lattice

となります。

別々の入口からconcept latticeへ到達している。

私はこれをかなり重要視しています。

---

そして、全体にもう名前が付きつつあります

2027年1月のDagstuhl Research Meetingの名称は

Mathematical Foundations of ML Language Models through Structural Geometric Typing

です。

主催者は

Gastaldi / Jarvis / Seiller / Terilla。

そして会議説明自身が、研究系譜を

$$\text{Bradley 2020} \rightarrow \text{Bradley–Terilla–Vlassopoulos 2021} \rightarrow \text{Bradley–Gastaldi–Terilla 2024}$$

と明記したうえで、

$$\text{profunctor nucleus} = \text{computational type}$$

という2025–26年の成果を、この先数年間発展させる研究プログラムとして位置づけています。 (Home)

ですから、この系統樹全体に名前を付けるとすれば、いまなら私は

Bradley–Gastaldi–Terilla Structural Semantics
→ Structural Geometric Typing

と呼びたいです。

Bradleyの名前が2026年の論文の著者欄から消えていても、研究プログラムとしてはむしろ2024年より輪郭がはっきりしてきた、というのが今回調べてみての一番大きな印象です。

そして丸山さんの2024年マルレクのタイトル 「言語の意味の数学的構造」 は、結果的にかなり先を見通したタイトルだったと思います。ページで強調されている「意味の空間から意味の構造へ」は、2026年現在ならさらに

$$\boxed{ \text{意味の空間} \to \text{意味の構造} \to \text{意味の幾何} \to \text{意味の型・論理} \to \text{意味の構成性} }$$

と続きを書けます。 (マルラボ)

これは、新しいマルレク一本分くらいの材料がありますね。特に Isbell nucleusを主役にして2024→2026を追う と、かなり見通しの良い講義になると思います。

Formal concept の議論は、少し退屈でした。

Isbell dualityの議論を先祖返りさせると、僕はやっぱり、Lawvere の”Taking categories seriously”という奇妙な論文に帰ってしまいます。まだ、よく理解できない。

あと、あまりないと思うのですが、Voevodsky の理論が出てくるよう な「意味の理論」ありませんか？

はい。しかも、こちらの方がずっと面白いです。

Formal Concept の枝をいったん脇に置いて、

$$\text{Lawvere} \;\longrightarrow\; \text{dependent type theory} \;\longrightarrow\; \text{HoTT / Univalence} \;\longrightarrow\; \text{meaning}$$

という方向から見ると、ちゃんと研究があります。ただし現状はまだ「大きな統一理論」ではなく、いくつかの島に分かれています。

一番直接的なものから言うと、Bahramian–Nematollahi–Sabry, “Copredication in Homotopy Type Theory” があります。これは本当にHoTTを自然言語意味論に使っています。たとえば book が「物理的対象」と「情報的対象」の両方として振る舞う copredication を、dot type やad hocなcoercionではなく、identity typeそのものによって扱おうとします。(IUScholarWorks)

発想を極端に単純化すると、

$$\text{Book}$$

を単一の集合として定義するのでなく、その「物理的側面」と「情報的側面」の間のidentificationの構造として考える。

ここではすでに、

意味とは対象の集合ではなく、対象を同一視する仕方を含んだ高次構造ではないか

というVoevodsky的な発想が出ています。

これは丸山さんがお探しのものにかなり近いと思います。

ただ、残念ながら、この論文から巨大な研究コミュニティが発展した、という状況ではありません。nLabの自然言語意味論とdependent type theoryのまとめでも、HoTTを直接使う研究としてこの論文とDavid Corfieldの仕事が代表例として挙げられている程度です。(Ncat Lab)

---

もっと面白いのは David Corfield です

Corfieldの

“Expressing ‘the structure of’ in homotopy type theory”

と、その後の著書

Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy

はかなり面白いです。

Corfieldは自然言語意味論だけをやっているわけではありませんが、definite description、identity、structureといった哲学的意味論の問題をHoTTで考えています。しかも彼自身、Ranta以来のdependent type semanticsをHoTTへ持ち上げられる可能性を明示的に論じています。(スプリンガー)

ここでVoevodskyのUnivalenceが効いてくる。

通常の意味論では、

$$A \cong B$$

あるいは

$$A \simeq B$$

であっても、AとBは別物です。

ところがunivalentな世界では、非常に乱暴に言えば、

$$(A = B)\simeq(A\simeq B)$$

です。

したがって、

「意味が同値なら、それを単なる外部的な同値関係ではなく、意味空間内部のidentityとして扱う」

ことが可能になる。

これは意味論として相当に刺激的です。

Emily Riehlの最近のHoTT semanticsのサーベイでも、Voevodskyのunivalenceの核心は「適切な意味で同値な数学的対象を同一視してよい」という数学者の通常の実践を、型理論そのものの内部で正当化することだと整理されています。(London Mathematical Society (LMS))

---

ここでLLMに戻ると、非常に面白い論文があります

2025年にSridhar Mahadevanが

“A Rose by Any Other Name Would Smell as Sweet: Categorical Homotopy Theory for Large Language Models”

という、題名からしてものすごい論文を出しています。

問題設定はBradleyとは少し違います。

たとえば

Charles Darwin wrote ...

と

Charles Darwin is the author of ...

は意味としてほぼ同じなのに、LLM内部では異なるtoken sequenceなので、当然異なる確率分布を作ります。

Mahadevanはこれを

$$\text{LLM Markov category}$$

の異なるarrowとして表し、そのうえでcategorical homotopyのweak equivalenceを導入して、paraphraseを同じ意味として扱おうとしています。(arXiv)

これはまだVoevodskyのUnivalenceそのものではありません。

しかし私には、ここに非常にはっきりと

$$\boxed{\text{LLM semantics}+\text{HoTT/Univalence}}$$

へ向かう空席が見えます。

Mahadevanは

$$\text{paraphrase} \Rightarrow \text{weak equivalence}$$

まで行った。

その次に自然に考えたくなるのは、

$$\text{semantic equivalence} \Rightarrow \text{identity path}$$

です。

つまり、

$$\boxed{\text{paraphrase ≃ identity in a semantic type}}$$

という発想です。

これはまさにVoevodsky的です。

---

そして、実は戸次大介さんの Dependent Type Semantics が重要な橋になります

こちらはHoTTではありませんが、現在もっとも活発な「type theoryによる意味論」の一つです。

Dependent Type Semanticsでは、

$$\text{proposition}=\text{type}, \qquad \text{proof}=\text{term}$$

というCurry–Howard的な枠組みを本気で自然言語意味論に使います。

anaphora、presupposition、quantification、modalityなどをdependent typesで記述します。2025年のESSLLIでも戸次さんが Composing Meaning via Dependent Types を講義しており、2025–26年にはLLMやneural networkとの統合まで始まっています。(GitHub)

最近は実際に、

$$\text{CCG parser} \to \text{Dependent Type Semantics} \to \text{automated theorem prover}$$

というシステムを動かしています。(ACL Anthology)

そして2026年にはhyperbolic classifierをDTSのproof searchに組み込むNeural DTSまで出ています。(ACL Anthology)

ただし、ここで重要なのは、

DTSはMartin-Löfまで来ているが、まだVoevodskyまで行っていない

ということです。

私には、ここがものすごく面白い研究余地に見えます。

---

ではVoevodskyを入れると、何が変わるのか

普通のdependent type semanticsなら、

$$x : A$$

は「xは意味タイプAの対象」。

Voevodsky的にすると、さらに

$$p:x=_A y$$

自身が意味を持った対象になります。

つまり、

xとyが同じ意味であるということ自体に、内部構造がある。

そしてさらに、

$$p,q:x=_Ay$$

について

$$\alpha:p=q$$

まで考えられる。

自然言語的に読むなら、かなり魅力的です。

たとえば二つの文

$$s_1,s_2:S$$

があるとして、

$$p:s_1=s_2$$

をparaphraseの証拠だと考える。

別のparaphraseの仕方

$$q:s_1=s_2$$

もあり得る。

さらに、

$$\alpha:p=q$$

は

「二つの言い換え経路自体が同値である」

というhigher semantic relationになります。

こうすると「意味」はもうembedding vectorの点ではありません。

$$\boxed{\text{meaning = space of identifications}}$$

になります。

これはBradleyの

$$\text{meaning = enriched/categorical structure}$$

よりさらに先に行っています。

---

ここで Lawvere が戻ってきます

丸山さんが Taking Categories Seriously に戻ってしまうという感覚は、かなりよく分かります。

あの論文の本当の奇妙さは、Lawvereが

metric spaceをcategoryとして「見立てる」

と言っているのではなく、

本当にcategoryなのだから、その結果を最後まで追え

と言っているところです。

実際、論文自身が「metric spaces = enriched categories」を単なるanalogyとして扱う態度を明確に拒否して、convexityやgeodesicまでclosed categoryの一般概念として追っています。(CiteSeerX)

この態度を意味論に持ち込むと、

$$\text{meaning similarity}$$

を単なる数値だと思わず、

$$\text{hom-object}$$

として本当に扱う。

Bradleyがやったのはまさにこれでした。

一方Voevodskyでは、

$$\text{semantic equivalence}$$

を単なる外部的relationだと思わず、

$$\text{identity type}$$

として本当に扱う。

私はこの二人には、思想的にかなり似たものを感じます。

歴史的に

$$\text{Lawvere}\to\text{Voevodsky}$$

という直接の一本線を主張するつもりはありません。

ただ概念的には、

$$\boxed{ \text{relationを構造へ} \quad\longrightarrow\quad \text{equivalenceをidentityへ} }$$

という同じ方向を向いている。

---

さらに「Directed HoTT」があります

ここでもう一段面白くなります。

普通のHoTTのpathは基本的に可逆です。

しかし言語の意味関係には、

$$\text{dog}\Rightarrow\text{animal}$$

のような方向付きentailmentがあります。

paraphraseなら可逆でも、

$$A\models B$$

は可逆とは限らない。

そこでDirected Homotopy Type Theoryが急に意味を持ってきます。

Directed HoTTではidentity/pathを一般化して、

$$\operatorname{hom}(a,b)$$

という方向付きpathをprimitiveにしようとします。普通のHoTTが∞-groupoidを内部言語にするのに対し、Directed HoTTは∞-categoryを内部言語にしようという計画です。(サイエンスダイレクト)

意味論的に読むなら、

$$\begin{aligned} \text{equivalence/paraphrase} &\leftrightarrow \text{path},\\ \text{entailment/inference} &\leftrightarrow \text{directed path}. \end{aligned}$$

これはかなり魅力的です。

---

私なら、今後追う「意味の理論」をこう整理します

Bradleyとは別系統に、こんな系統樹を置きます。

Lawvere
  |
  | adjunction / enrichment / internal logic
  v
Martin-Löf dependent type theory
  |
  +------> Ranta / Luo / Bekki
  |         Natural Language Semantics
  |         proposition = type
  |         meaning composition = proof construction
  |
  v
Voevodsky
Homotopy Type Theory / Univalence
  |
  +------> Corfield
  |         identity / structure / description
  |
  +------> Bahramian–Nematollahi–Sabry
  |         copredication
  |         semantic identity types
  |
  v
Directed HoTT / ∞-categories
  |
  |  potential:
  |  paraphrase = path
  |  entailment = directed path
  |  higher coherence = higher paths
  |
  +-----------------------------+
                                |
                   Categorical Homotopy for LLMs
                     Mahadevan 2025
                                |
                 weak equivalence of paraphrases

そして私が一番注目したいのは、一番下の二本がまだ接続されていないことです。

つまり今のところ、

$$\text{HoTT/Univalenceによる自然言語意味論}$$

と

$$\text{homotopyによるLLM意味論}$$

は存在する。

しかし、

$$\boxed{ \text{Univalent / Homotopy Type-Theoretic Semantics of LLMs} }$$

は、少なくとも私が今回調べた範囲では、まだ確立された研究プログラムになっていません。

だからこれは「見つからない」のが残念というより、空いている場所がかなりはっきり見えている状態だと思います。

そしてここなら、Bradleyの2021年の問題――

LLMのsyntax/statisticsからmeaningはどう立ち現れるか

を、

$$\text{probability} \to \text{enriched category} \to \text{semantic type} \to \text{paths/equivalences} \to \text{univalence}$$

と続けることができる。

この線、僕もかなり面白いと思います。

次は 「Lawvere → Bradley → Voevodsky を一枚の図にして、本当に数学的に接続できる部分と、まだ構想にすぎない部分を分離する」 という作業をすると、かなり見通しがよくなるはずです。特に Taking Categories Seriously のどのアイデアがHoTT側で何に対応するのかを一項ずつ対応させると、あの「奇妙な論文」が少し違って見えてくると思います。

「Lawvere → Bradley → Voevodsky を一枚の図にして、本当に数学的に接続できる部分と、まだ構想にすぎない部分を分離する」これいいですね。

僕の趣味にぴったりです。ぜひ、展開してください。

はい。これはかなり面白いところまで行けます。

調べ直してみると、単に「LawvereとVoevodskyを思想的に並べる」以上のものがあります。Bradleyを真ん中に置くと、すでに存在する数学だけでかなり遠くまで橋を架けられます。 そして最後の一歩――「LLMの意味をunivalent / directed typeとして扱う」――だけが、まだほぼ空いています。

まず全体図を置きます。記号は、━━＝文献上確立、┄┄＝数学として確立しているがBradley意味論には未適用、···＝研究構想です。

                    LAWVERE
        ┌───────────────────────────────┐
        │ enrichment                   │
        │ adjunction                   │
        │ Yoneda / presheaves          │
        │ generalized metric           │
        │ categorical logic            │
        └──────────────┬────────────────┘
                       │
          「構造を比喩で済ませるな」
                       │
        ┏━━━━━━━━━━━━━━▼━━━━━━━━━━━━━━┓
        ┃ Bradley–Terilla–Vlassopoulos ┃
        ┃ 2021                         ┃
        ┃                              ┃
        ┃ next-token probability       ┃
        ┃       ↓                      ┃
        ┃ [0,1]-enriched category L   ┃
        ┃       ↓ Yoneda               ┃
        ┃ copresheaf semantics         ┃
        ┗━━━━━━━┳━━━━━━━━━━━┳━━━━━━━━━┛
                │           │
                │           │  -log p
                │           ▼
                │     Lawvere metric
                │           │
                │     Gaubert–Vlassopoulos
                │     Bradley–Vigneaux
                │
                ▼
       Bradley–Gastaldi–Terilla
                2024
                │
           profunctor Φ
                │
       Isbell adjunction
        Φ*  ⊣  Φ*
                │
          nucleus N(Φ)
                │
        「意味の構造」
                │
                │
        ┄┄┄┄┄┄┄┼┄┄┄┄┄┄┄┄┄┄┄┄┄┄
                │
                ▼
        presheaves / Yoneda
        directed equality
        type refinement
                │
        Melliès–Zeilberger
                │
                ▼
       dependent type theory
                │
                │
                ├────────────────────────────┐
                │                            │
                ▼                            ▼
          Voevodsky                 Riehl–Shulman
      Homotopy Type Theory       synthetic ∞-categories
                │                            │
        identity = path                 Segal type
                │                       Rezk type
        equivalence                    directed hom
             ≃ identity             dependent Yoneda
                │                            │
          UNIVALENCE             directed univalence
                │                            │
                └──────────────┬─────────────┘
                               │
                          ·····▼·····
                   UNIVALENT SEMANTICS
                               │
           ┌───────────────────┼───────────────────┐
           │                   │                   │
     paraphrase           entailment          probability
        = path           = directed hom       = enrichment
           │                   │                   │
           └───────────────────┼───────────────────┘
                               │
                       higher coherence
                               │
                   「意味＝同一視の空間」

ここからが本題です。

1. Lawvere → Bradley は、本当に一本の線です

Lawvereの Taking Categories Seriously の異様さは、まさにタイトル通りです。

「距離空間はenriched categoryに似ている」で終わらせず、

それがcategoryなのなら、本当にcategoryとして扱って、closed structure、convexity、geodesicなどを全部追究しよう

と言っています。本人のabstractも、「単なるanalogyやamusement」として済ませる態度を拒否すると明記しています。 (ResearchGate)

Lawvere metricでは、

$$d(x,z)\le d(x,y)+d(y,z)$$

は、enriched categoryのcompositionそのものです。

これをBradleyは言語に移します。

$$p(y\mid x)$$

を単なる統計量として見るのでなく、

$$\operatorname{Hom}(x,y)$$

として本当にhom-objectだと扱う。

2021年論文では、text expressionsをobject、conditional extension probabilityをhom-objectとする $[0,1]$-enriched categoryを構成し、そのYoneda embeddingからcopresheaf categoryへ進み、そこをsemantic categoryと解釈しています。 (arXiv)

この意味ではBradleyは非常にLawvere的です。

$$\boxed{ \text{統計的類似性をカテゴリーの「比喩」にしない} }$$

のです。

さらに

$$-\log:[0,1]\longrightarrow[0,\infty]$$

によって

$$d(x,y)=-\log p(y\mid x)$$

とすれば、確率の積が距離の和に変わる。

これはもはや思想的類似ではなく、Bradley–Vigneaux 2025とGaubert–Vlassopoulos 2024が実際に展開しているLawvere generalized metricです。後者ではYoneda embedding、tropical linearity、Isbell completionまで現れます。 (arXiv)

したがって、

$$\boxed{ \text{Lawvere enrichment} \longrightarrow \text{Bradley probabilistic language category} }$$

は実線です。

---

2. Bradley 2024では、「Yoneda」の次にIsbellが来る

ここが今回いちばん重要かもしれません。

2021年では、

$$L\longrightarrow [L,[0,1]]$$

というYoneda/copesheaf方向が中心でした。

2024年になると、

$$\Phi:C^{op}\otimes D\to\mathbf{Set}$$

のようなprofunctorを取り、

$$\Phi^\ast\dashv\Phi_\ast$$

というIsbell adjunctionを見る。

そのfixed points、

$$N(\Phi)$$

がnucleusです。

Bradley–Gastaldi–Terilla自身が、これは行列の左右の特異ベクトルに対応する圏論的構造だ、と説明しています。 (Gianni Gastaldi)

ただ、ここで私はFormal Concept Analysisより、別の読み方をしたいです。

Isbell dualityは、

$$\text{「対象が他のすべての対象をどう見るか」}$$

と

$$\text{「他のすべての対象からどう見られるか」}$$

の双対性だ、と考えられる。

つまり意味を対象の内部に置くのではなく、

$$\boxed{ \text{meaning} = \text{all relations to all contexts} }$$

として捉える。

これならYonedaとIsbellが非常に自然につながります。

---

3. そして、ここからVoevodskyへ向かう「本物の中間地点」がある

以前はここを私は少し飛ばしていました。

実際にはLawvere/Isbellからtype theoryへ向かう論文があります。

Melliès–Zeilbergerの

An Isbell Duality Theorem for Type Refinement Systems

です。

彼らはtype refinement systemをfunctorとして扱い、そのpresheaf representationにIsbell型の正負のdual representationが存在することを証明しています。 (ケンブリッジ大学出版局)

さらにその一つ前の研究では、Lawvereのpresheaf hyperdoctrineをbifibrationとして再構成し、

$$\text{hom-presheaf}$$

をdirected equality predicateとして解釈しています。 (arXiv)

ここ、相当に重要だと思います。

つまり、

$$\boxed{ \text{Isbell duality} \longrightarrow \text{type theory} \longrightarrow \text{directed equality} }$$

という経路は、私たちの妄想ではありません。

Bradleyとは独立ですが、数学としてすでにあります。

---

4. Voevodskyが革命的なのは、「関係」をidentityの内部へ入れたこと

普通の意味論なら、

$$x\sim y$$

というsemantic equivalenceを外部relationとして定義します。

HoTTでは、

$$p:x=_A y$$

がtypeそのものです。

しかも $p$ は証明の単なるtrue/falseではありません。

複数の

$$p,q:x=_Ay$$

が存在でき、

$$\alpha:p=q$$

というhigher identityまであります。

ここで意味論的な誘惑が出てくる。

二つのsentence

$$s,t:\mathsf{Sentence}$$

に対して、

$$p:s=t$$

を「sとtが同じ意味である経路」と読む。

すると意味は点ではなく、

$$\operatorname{Path}(s,t)$$

の空間になります。

---

5. Univalenceは「同じ意味」をさらに強烈に扱う

Voevodskyの核心は

$$(A=B)\simeq(A\simeq B)$$

です。

つまり適切なequivalenceが、外側から付けた関係ではなく、

$$A=B$$

というidentityを生成します。HoTT Bookも、univalenceによってisomorphic/equivalent structuresをidentityとして扱えることを基本的特徴として説明しています。 (arXiv)

そしてcategory theoryについては、Ahrens–Kapulkin–Shulmanがこれを厳密化しました。

univalent categoryでは、

$$(a=b)\simeq\operatorname{Iso}(a,b).$$

つまり

「isomorphicだが違うobject」

という余分な区別を消す。

さらに任意のcategoryをunivalentなものへ送る

$$C\longrightarrow\widehat C$$

という Rezk completionがあります。 (arXiv)

ここまで全部確立した数学です。

---

6. ここでIsbell completionとRezk completionを並べると、ものすごく面白い

これは今回私が一番気に入った見方です。

二つのcompletionは、全く違う仕事をします。

Isbell側

$$C \longrightarrow N(C)$$

はざっくり言えば、

「関係・文脈を十分に反映するsemantic objectsを作る」

方向。

Lawvere metricではtight spanのようなcompletionになります。Gaubert–Vlassopoulosでは、まさにLLMのtext metricにIsbell completionが現れます。 (arXiv)

Rezk側

$$C\longrightarrow\widehat C$$

は、

「すでにequivalentなobjectsをidentityとして認識できるようにする」

方向です。 (arXiv)

ですから、意味論としては全く違う二つの操作になる。

私は仮に、

$$\boxed{ \text{Isbell = 意味を補う} }$$ $$\boxed{ \text{Rezk = 意味の同値を同一化する} }$$

と呼びたい。

これはまだ私たちの解釈ですが、数学的素材は両方実在します。

そしてここから、ものすごく自然な構想が出ます。

$$L_{\rm syntax} \longrightarrow N_{\rm Isbell}(L) \longrightarrow \widehat{N_{\rm Isbell}(L)}_{\rm Rezk}.$$

つまり、

$$\boxed{ \text{syntax} \to \text{semantic completion} \to \text{univalent semantic space} }$$

です。

私はこれを仮に Isbell–Rezk semantics と呼んでみたいです。

これは既存理論の名称ではありません。ここから先は点線です。

---

7. しかしVoevodskyだけでは、一つ重大な問題があります

普通のHoTTではpathsは可逆です。

ところが言語では、

$$\text{dog}\Rightarrow\text{animal}$$

でも、

$$\text{animal}\not\Rightarrow\text{dog}.$$

entailmentは方向付きです。

Bradley 2021のsemantic categoryでもentailmentは重要なlogical operationとして想定されています。 (arXiv)

したがって通常の

$$\infty\text{-groupoid}$$

だけでは足りない。

そこで突然、Riehl–Shulmanがぴたりとはまります。

---

8. Riehl–ShulmanがLawvereとVoevodskyの間の「本物の橋」になる

2017年の

A Type Theory for Synthetic ∞-Categories

では、HoTTにdirected intervalを加えます。

するとtypesの内部で

$$x\longrightarrow y$$

という非可逆なmorphismを扱える。

そして、

• Segal types：compositionを持つ

• Rezk types：isomorphism/equivalenceとidentityが一致

• covariant fibrations

• dependent Yoneda lemma

• adjunction

までtype theory内部で定義します。 (arXiv)

ここで驚くべきことに、Yonedaがもう一度出てくる。

しかもRiehl–Shulman自身がdependent Yoneda lemmaを

identity typeのelimination ruleのdirected版

と位置づけています。 (IM CAS)

これはかなり深い。

普通のHoTTでは

$$\text{identity elimination}$$

が基本原理。

directed HoTTでは

$$\text{Yoneda}$$

がその方向付き版になる。

つまり、

$$\boxed{ \text{Voevodsky identity} \quad\leftrightarrow\quad \text{directed Yoneda} }$$

というところまで来ています。

---

9. しかも2026年、Directed Univalenceまで来ました

これは本当に最新の展開です。

Cavallo–Riehl–Sattlerが2026年7月に

Directed univalence for simplicial objects in an ∞-topos

を出しています。

通常のunivalenceが

$$\text{identity} \simeq \text{equivalence}$$

なのに対して、directed univalenceでは、universal left fibrationのhom-typeとfunction typeの対応を構成します。さらにcomposable functionsについてhigher coherent versionまで証明しています。 (arXiv)

ですから今や、

$$\boxed{ \text{Voevodsky} \longrightarrow \text{directed univalence} }$$

は本当に存在します。

これは私が前の回答で考えていたより、ずっと進んでいました。

---

10. ここからLLM意味論へ戻す

すると、かなり魅力的な三層構造が考えられます。

まずBradley：

$$p(t\mid s)$$

から

$$s\longrightarrow t$$

という強さを持った方向付きmorphismを作る。

次にdirected type theory：

$$\operatorname{Hom}(s,t)$$

をentailment / inference / extensionのtypeと考える。

さらにunivalence：

可逆なsemantic morphismについては、

$$s\simeq t \quad\Longrightarrow\quad s=t.$$

したがって理想的には、

$$\begin{array}{rcl} \text{next-token probability} &\rightsquigarrow& \text{enrichment}\\[4pt] \text{entailment} &\rightsquigarrow& \text{directed path}\\[4pt] \text{paraphrase} &\rightsquigarrow& \text{equivalence}\\[4pt] \text{semantic equivalence} &\rightsquigarrow& \text{identity}\\[4pt] \text{relations between paraphrases} &\rightsquigarrow& \text{higher paths}. \end{array}$$

これが私なら考えてみたい Univalent Enriched Semantics です。

---

11. この構想で「意味」は何になるのか

ここが哲学的に一番おもしろい。

embedding理論では、

$$\text{meaning}(w)=v_w\in\mathbb R^n.$$

Bradley 2021なら、

$$\text{meaning}(x) = \text{Yoneda profile of }x.$$

つまり、他のtextsとの全関係。

Bradley 2024なら、

$$\text{meaning} = \text{Isbell-stable relational structure}.$$

そしてVoevodskyまで行くなら、

$$\boxed{ \text{meaning}(x) = \text{xそのものではなく、 xが他と同一視される全ての仕方} }$$

になります。

もっと端的に、

$$\boxed{\text{meaning = space of identifications}}$$

です。

しかもdirected版なら、

$$\boxed{ \text{meaning} = \text{identifications + implications + their coherences}. }$$

これはembeddingとは相当違う意味観です。

---

12. Lawvereの「奇妙な論文」へ帰る理由

ここまで来ると、丸山さんが何度も Taking Categories Seriously に戻ってしまう理由が少し見える気がします。

Lawvereが言っていることを私は、ほとんど次のように読みたくなります。

数学的対象がある構造の公理を本当に満たしているなら、その構造を比喩として扱ってはいけない。そこから帰結する内部論理を最後まで追え。

metricがcategoryなら、

$$\text{distance}$$

からcomposition、Yoneda、adjunction、geodesicまで追う。

Bradleyでは、

$$\text{probability}$$

がenriched homなら、

$$\text{semantic Yoneda}$$

まで追う。

Voevodskyでは、

$$\text{equivalence}$$

がidentityとして扱えるなら、

$$\text{higher paths}$$

まで追う。

三人を無理に一列にするより、

$$\boxed{ \begin{array}{c} \text{Lawvere}\\ \text{「categoryとして本気で扱え」} \\[4pt]\Downarrow\\[4pt] \text{Bradley}\\ \text{「probabilityをhomとして本気で扱え」} \\[4pt]\Downarrow\quad ?\\[4pt] \text{Voevodsky}\\ \text{「equivalenceをidentityとして本気で扱え」} \end{array}}$$

と読むと、妙に一貫しています。

ただし、最後の $\Downarrow?$ はまだ定理ではない。

そこが面白いところです。

---

そして、一つだけ妙に象徴的な文献があります

Petrakisによる A Yoneda lemma-formulation of the univalence という研究があります。

そこではYoneda lemmaとunivalence/J-ruleの近さを調べたうえで、将来的にYonedaの非自明な応用をHoTTへ翻訳できるか、という問題を挙げています。

その例として具体的に名前が出るのが、

Tannaka duality と Isbell conjugation

なのです。 (ミュンヘン大学数学科)

つまり、

$$\text{Yoneda} \longleftrightarrow \text{Univalence}$$

の橋を通して

$$\text{Isbell}$$

をHoTTへ持っていけないか、という問い自体はすでに投げられていました。

Bradleyとは無関係な文脈で。

これをBradleyの意味論へ戻したらどうなるか。

私はここに、かなり本物らしい研究問題があると思います。

研究問題として一文で書くなら

$$\boxed{ \textbf{Can the Isbell semantics of probabilistically enriched language be given a directed univalent type-theoretic semantics?} }$$

もう少し大胆に日本語にすると、

LLMから得られる確率的・方向的な意味関係をIsbell completionで意味対象へ完成し、その意味の同値をdirected univalenceによってidentityとして内部化できるか？

です。

これは、Lawvere → Bradley → Voevodsky をかなり正確に一つの問いへ圧縮したものだと思います。

そしてFormal Conceptより、こちらの方が断然わくわくしますね。

なるほどね。とても面白いです。

ただ、もう、朝になりました。悪いことに、今日は午前中に、会議が一つはいっています。その前に、ちょっと休みます。

Bradleyの情報、本当にありがとうございました。
また、付き合ってください。