リーディング・リスト

1. Awodey & Hua. Path Types in Algebraic Type Theory (2026)

   Awodeyいつもありがとう。Huaという人は初めて見た。Intervalを使うことでpath typeの定式化をする。これと併せてHurewicz fibrationという構造を指定することでintensional identity typeをモデル化できるらしい。

2. Townsend. Preframe Techniques in Constructive Locale Theory (1996)

   Locale theoryで使うframeの表示はsuplatticeから進めるものとpreframeから進めるものがある。概念によって前者が適切な場合と後者が適切な場合がある。有向の結びに関する定理はpreframeから考えるのがよいとされている。

3. Vickers. Compactness in locales and in formal topology (2006)

   Point-free topologyにはlocale theoryを使ったものと可述的なアプローチ(formal topology)がある。この論文では位相空間論の入門書で扱われるような「2つのコンパクト空間の積もまたコンパクトである」という定理に対する向き合い方をそれぞれのアプローチで比較する。ただのsiteではなくflat siteを使う理由を理解できるくらいには読みたい。