このブログの更新は Twitterアカウント @m_hiyama で通知されます。
Follow @m_hiyama

メールでのご連絡は hiyama{at}chimaira{dot}org まで。

はじめてのメールはスパムと判定されることがあります。最初は、信頼されているドメインから差し障りのない文面を送っていただけると、スパムと判定されにくいと思います。

［参照用 記事］

依存型理論の圏論的セマンティクスの資料

雑記／備忘

「依存アクテゴリーに向けて」において：

当然に、アクテゴリーは依存アクテゴリーの事例となります。その他に良い事例はないでしょうか？ 「最近の型理論： 拡張包括構造を持ったインデックス付き圏」で概要を述べた包括圏〈comprehension category〉が、依存アクテゴリーの事例になりそうです。

「最近の型理論： 拡張包括構造を持ったインデックス付き圏」は、バート・ジェイコブス〈Bart Jacobs〉の包括圏〈comprehension category〉というより、ファミリー付き圏と局所デカルト閉圏を若干抽象化した圏を想定して書いていたようです。

型理論では、型の意味論としてファミリー付き圏〈CwF | category with families〉や局所デカルト閉圏〈LCCC | locally cartesian closed category〉なども使われます。もし、包括圏が依存アクテゴリーになるとしたら、ファミリー付き圏や局所デカルト閉圏が依存アクテゴリーになる可能性は高いでしょう。

事例がないと何していいか分からないので、事例を探すことにします。とりあえずは、前節で述べた型理論からの事例を確認かな。

依存アクテゴリーの事例が見つかる可能性がある、型理論の資料を列挙します。

カステラン、クレランボー、ディビエ

クレランボーの次の論文はよくまとまっていて便利です。https じゃなくて http のURLを持っているせいか(?)、検索に引っかかりにくいようです。

カステランのスライドはザッと眺めるには良いです。これだけでは詳細はわかりませんが。

クレランボー／ディビエによる、型理論のモデルとなる圏達の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" とは、サイズも次元も上がった圏のことです。

おそらく、上のアブストラクト（とトーク）の内容をまとめたものが次の論文でしょう。

  • [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

ハズラトプール

「局所デカルト閉圏の勉強をしたのでまとめます」という感じの文書。ドラフト状態です。

グラッツァー／スターリング

依存型理論を、今風の観点と定式化で俯瞰的に述べています。

  • [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