過去記事「バタニン・ツリー 再論」の最初の節にバタニン・ツリーの参考文献を載せました。内容的重複がありますが、この記事でも参考資料／参考文献を紹介します。過去記事より細かいコメントを付けます。が、いずれの論文も拾い読みしかしてないので、拾い読みした範囲内でのコメント（注目・注意ポイントと文言・図の引用）です。イビツなコメントであることはご承知おきください。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
`$
内容：
ウェーバー 2004
バタニン・ツリーが、ストリート〈Ross Street〉の球体基数〈globular cardinal〉と同値であることが書いてあります。また、バタニン・ツリーの表現として、なめらかなジグザグ自然数列〈smooth zig-zag sequence〉が導入されています。
- [Web04-]
- Title: Generic morphisms, parametric representations and weakly cartesian monads
- Author: Mark Weber
- Year: 2004,
- Pages: 45p
- URL: http://www.tac.mta.ca/tac/volumes/13/14/13-14abs.html
注目・注意ポイント：
- p.9 -- p.16 "4. Globular cardinals" で球体基数の解説
- p.10 で球体プレ順序（solid triangle order と呼んでいる）の定義。球体基数は球体プレ順序を使って定義される。
- p.11 からジグザグ列〈zig-zag sequence〉の解説
- p.11 にストリート〈Ross Street〉の結果「球体基数 ＝ ペースティングスキーム」の引用
- 球体圏〈球体の形状〉$`\mathbb{G}`$ の射は、余ソース／余ターゲット〈cosource/cotarget〉と呼んでいる。辻褄が合っている。余ソース・アロー（$`\mathbb{G}`$ の射）は $`\sigma_i : i \to i + 1`$
- 球体集合の圏は $`\mbf{Glob}`$
- 球体基数（ペースティングスキームと事実上同じもの）の圏の固有名は $`\Omega`$
フィンスター／ミムラム 2017
「指標の話： ペースティング図とバタニン・ツリー」で最初に参照して、その後「球体集合達の圏の構文表示 1/2」などでも繰り返し参照しているフィンスター／ミムラムの論文。p. 7 "D. Batanin trees" で、僕は初めてバタニン・ツリーを知りました。短い論文ですが、色々なことが要領よく書いてあるので役に立ちます。
- [FM17-]
- Title: A Type-Theoretical Definition of Weak ω-Categories
- Authors: Eric Finster, Samuel Mimram
- Submitted: 9 Jun 2017
- Pages: 12p
- URL: https://arxiv.org/abs/1706.02866
注目・注意ポイント：
- p.4 -- p.9 "III. PASTING SCHEMES" でペースティングスキームの解説
- p.9 -- p.12 "IV. WEAK ω-CATEGORIES" で一貫子〈{coherator | coherence} {cell}?〉という概念が導入されている。
- p.4 （"III. PASTING SCHEMES" の直前）で、型理論の集合論的モデル〈set-theoritic model〉が定義されている。
- 球体的なプレックスである円板〈disk〉と、それらの球体和〈globular sum〉が定義されている。
- p.5 "A. Globular extensions" で、“球体圏”〈globular category〉を定義しているが、さすがにこれはマズいネーミングなので、後の論文「ベンジャミン／フィンスター／ミムラム 2022-2024」では球体構造〈globular structure〉に変更している。
- 球体圏〈形状 | globe category〉は、明示的には定義していない。
- 球体集合の圏は $`\mbf{GSet}`$
- 球体集合 $`G`$ のソース写像／ターゲット写像は $`s_n,t_n : G_{n+1} \to G_n`$
- テータ圏 $`\Theta_0`$ が定義され、テータ圏の対象とペースティングスキームは同一視される。
- 球体プレ順序の非反射バージョンが、関係記号 $`\triangleleft`$ として導入されている。
- $`\triangleleft`$-linear な球体集合とペースティングスキームは同一視可能なことが示される。
- (-1)次元の球体集合としての空集合を表す記号は $`\star`$ 。便宜上、0-セルの両端（境界）は(-1)次元の球体集合だと考える。あくまでも便宜上で、(-1)-セルは当然に存在しない。
- ツリーの頂点〈ノード〉に対するパイ形〈扇形〉領域は、この論文ではセクター〈sector〉と呼んでいる。
幾つかの図を引用します。
ペースティングスキームの事例をドット＆アロー＆ダブルアロー図で描いたもの：
上の事例を、幾つかの円板達の球体和で表した図：
上の球体和の（通常の意味の）図式：
セルのアタッチメントを繰り返して球体集合を作る過程：
ベンジャミン／フィンスター／ミムラム 2022-2024
「依存型理論の圏論的セマンティクスの資料」で紹介したベンジャミン／フィンスター／ミムラムの論文。「フィンスター／ミムラム 2017」の発展として、とある型理論のモデルがマルチニオティ〈Maltsiniotis〉スタイルの球体的弱ω-圏となること、あるいは、球体的弱ω-圏が、型理論により記述できることが書いてあります。バタニン・ツリーに対する直接的な言及はあまりありません。
- [BFM21-24]
- Title: Globular weak ω-categories as models of a type theory
- Authors: Thibaut Benjamin, Eric Finster, Samuel Mimram
- Submitted: 8 Jun 2021 (v1), 2 Feb 2024 (v2)
- Pages: 70p
- URL: https://arxiv.org/abs/2106.04475
p.34 "4 Type theory for weak ω-categories" からが本ちゃんですが、全然目を通してないです。以下、p.34 より前を拾い読みしたコメントです。
注目・注意ポイント：
- ペースティングスキーム／弱ω圏へのアプローチとして、グロタンディーク／マルチニオティ・アプローチ、バタニン／レンスター・アプローチ、フィンスター／ミムラム・アプローチが同値であることを示している。ただし、バタニン／レンスター・アプローチについては書かれてない。
- 「フィンスター／ミムラム 2017」で定義した型理論を $`\mbf{CaTT}`$ と名付けている。$`\mbf{CaTT}`$ のOCaml実装が https://github.com/thibautbenjamin/catt にある。
- 球体圏（"category of globes" と呼んでいる）の射＝形状アローは $`\sigma_i,\tau_i`$ 、球体集合の射〈関数〉は $`s_i,t_i`$ と区別している。球体圏を定義する関係式は "coglobular relations" 。球体集合の関係式は "globular relations" 。
- 球体圏〈形状 | globe category〉は $`\mathscr{G}`$ 。
- 球体集合の要素はセル、球体的なn-プレックスはn-円板〈n-disk〉。
- n-円板（という球体集合）の境界としてn-球面〈n-sphere〉（という球体集合）を定義している。
- 球体集合の圏は $`\mbf{GSet}`$ 。
- 導出系〈演繹系 | 証明系 | 論理系〉の基本導出規則の組み合わせで“正しい”ものを "admissible rule" と呼んでいる。
- 特別な前層としての "familially representabe functor"（nLabでは "multirepresentabe functor"）の概念を使っている。
- 型理論の構文圏〈syntactic category〉がモデルの圏の始対象になる、という始対象原理〈The initiality principle〉を使っている。
頭のほうに、高次圏の定義が幾つも提案されているが、それらを比較するのは難しいという話があります。
The comparison between the proposals is still an ongoing research topic, and seems to be technically out of reach for now for some of them.
円板（あるいは球体）と球面（あるいは円周）の次元が低い場合の図：
ディーン／フィンスター／マルカキス／リアター／ヴィカリー 2022-2024
ディーン達の論文の p.6 "2 Batanin trees" でもバタニン・ツリーを扱っています。バタニン・ツリーの節しか読んでません。
- [DFMRV22-24]
- Title: Computads for weak ω-categories as an inductive type
- Authors: Christopher J. Dean, Eric Finster, Ioannis Markakis, David Reutter and Jamie Vicary
- Submitted: 18 Aug 2022 (v1), 20 Mar 2024 (v3)
- Pages: 67p
- URL: http://arxiv.org/abs/2208.08719
注目・注意ポイント：
- 球体集合のソースとターゲットは $`\mathsf{src}, \mathsf{tgt}`$
- 球体圏〈形状〉 $`\mathbb{G}`$ の余面アローは $`s, t`$ 、余面アローも（余ソース、余ターゲットではなくて）ソースとターゲットと呼んでいる。
- 球体集合の圏は $`\mbf{Glob}`$
- バタニン・ツリーに対して、k-境界作用素 $`\partial_k`$ を定義している。
- バタニン・ツリー $`B`$ のポジション集合（球体集合）$`\mrm{Pos}(B)`$ を、単に $`B`$ と書く略記を採用。
- 球体集合としての $`\mrm{Pos}(B)`$ のソース／ターゲットは $`\mathsf{src\text{-}pos},\mathsf{tgt\text{-}pos}`$
バタニン・ツリーのポジション集合に全順序を入れて、通し番号を付けた図：
ペースティングスキームの境界とその埋め込み：
