「依存アクテゴリーに向けて」において：
当然に、アクテゴリーは依存アクテゴリーの事例となります。その他に良い事例はないでしょうか？ 「最近の型理論： 拡張包括構造を持ったインデックス付き圏」で概要を述べた包括圏〈comprehension category〉が、依存アクテゴリーの事例になりそうです。
「最近の型理論： 拡張包括構造を持ったインデックス付き圏」は、バート・ジェイコブス〈Bart Jacobs〉の包括圏〈comprehension category〉というより、ファミリー付き圏と局所デカルト閉圏を若干抽象化した圏を想定して書いていたようです。
型理論では、型の意味論としてファミリー付き圏〈CwF | category with families〉や局所デカルト閉圏〈LCCC | locally cartesian closed category〉なども使われます。もし、包括圏が依存アクテゴリーになるとしたら、ファミリー付き圏や局所デカルト閉圏が依存アクテゴリーになる可能性は高いでしょう。
事例がないと何していいか分からないので、事例を探すことにします。とりあえずは、前節で述べた型理論からの事例を確認かな。
依存アクテゴリーの事例が見つかる可能性がある、型理論の参考資料／参考文献を列挙します。
カステラン、クレランボー、ディビエ
クレランボーの次の論文はよくまとまっていて便利です。https じゃなくて http のURLを持っているせいか(?)、検索に引っかかりにくいようです。
- [Cla06-]
- Title: From Categories with Families to Locally Cartesian Closed Categories
- Author: Pierre Clairambault
- Date: June 12, 2006
- Pages: 25p
- URL: http://perso.ens-lyon.fr/pierre.clairambault/cwfreport.pdf
カステランのスライドはザッと眺めるには良いです。これだけでは詳細はわかりませんが。
- [Cas14-]
- Title: Dependent type theory as the initial category with families
- Author: Simon Castellan
- Date: December 8, 2014
- Pages: 26p （スライド）
- URL: https://pdfs.semanticscholar.org/11d5/10a7c8d1f9266a6c2903b27d67b73cddc543.pdf
クレランボー／ディビエによる、型理論のモデルとなる圏達の2-圏〈双圏〉のあいだの2-圏同値〈双同値〉を示す話は以下。
- [CD11-]
- Title: The Biequivalence of Locally Cartesian Closed Categories and Martin-Löf Type Theories
- Authors: Pierre Clairambault, Peter Dybjer
- Submitted: 15 Dec 2011
- Pages: 45p
- URL: https://arxiv.org/abs/1112.3456
カステラン／クレランボー／ディビエによるファミリー付き圏のテキスト〈教科書的論文〉。
- [CCD19-20]
- Title: Categories with Families: Unityped, Simply Typed, and Dependently Typed
- Authors: Simon Castellan, Pierre Clairambault, Peter Dybjer
- Submitted: 1 Apr 2019 (v1), 7 Jul 2020 (v2)
- Pages: 46p
- URL: https://arxiv.org/abs/1904.00827
ビドリングマイヤー
TYPES 2019 (25th International Conference on Types for Proofs and Programs) の講演アブストラクトに気になることが書いてあります。"big category" とは、サイズも次元も上がった圏のことです。
- [Bid19]
- Title: Coherence via big categories with families of locally cartesian closed categories
- Author: Martin Bidlingmaier
- Date: June 2019
- Pages: 2p
- URL: http://www.ii.uib.no/~bezem/abstracts/TYPES_2019_paper_13
おそらく、上のアブストラクト（とトーク）の内容をまとめたものが次の論文でしょう。
- [Bid20-21]
- Title: An interpretation of dependent type theory in a model category of locally cartesian closed categories
- Author: Martin E. Bidlingmaier
- Submitted: 6 Jul 2020 (v1), 25 May 2021 (v2)
- Pages: 30p
- URL: https://arxiv.org/abs/2007.02900
ハズラトプール
「局所デカルト閉圏の勉強をしたのでまとめます」という感じの文書。ドラフト状態です。
- [Haz19-]
- Title: Notes on Locally Cartesian Closed Categories
- Author: Sina Hazratpour
- Date: 13/05/2019
- Pages: 18p
- URL: https://sinhp.github.io/files/CT/notes_on_lcccs.pdf
グラッツァー／スターリング
依存型理論を、今風の観点と定式化で俯瞰的に述べています。
- [GS20-21]
- Title: Syntactic categories for dependent type theory: sketching and adequacy
- Authors: Daniel Gratzer, Jonathan Sterling
- Submitted: 19 Dec 2020 (v1), 9 Mar 2021 (v2)
- Pages: 22p
- URL: https://arxiv.org/abs/2012.10783
追記： コラリア／エメネガー
今年の3月5日にarXivに投稿された新しい論文です。10ページまでに書かれている、コモナドと随伴系とのあいだの関係が面白いです。
- [CE24-]
- Title: A 2-categorical analysis of context comprehension
- Authors: Greta Coraglia, Jacopo Emmenegger
- Submitted: 5 Mar 2024
- Pages: 29p
- URL: https://arxiv.org/abs/2403.03085
追記2： nLab
追記2は 2024-05-27。nLabの依存型理論の長めの記事がまとまっていて読みやすいです。
- [nLab]
- Title: categorical semantics of dependent type theory
- Authors: nLab authors
- Date: Last revised on February 2, 2024
- URL: https://ncatlab.org/nlab/show/categorical+semantics+of+dependent+type+theory
追記2： ジャン
ファイブレーションと包括圏〈comprehension category〉に基づいて、圏論的型理論とその意味論を展開しています。ピッツ〈Pitts〉のタイプ圏〈type category〉にも触れています。
- [Zha21-22]
- Title: Type theories in category theory
- Author: Tesla Zhang
- Submitted: 28 Jul 2021 (v1), 4 Apr 2022 (v5)
- Pages: 47p
- URL: https://arxiv.org/abs/2107.13242
追記2： ベンジャミン／フィンスター／ミムラム
とある型理論のモデルが球体的弱ω-圏となること、あるいは、球体的弱ω-圏が、型理論により記述できることが書いてあります。
- [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
