リーディング・リスト

1. Kraus. The General Universal Property of the Propositional Truncation (2015)

   Univalent Foundationsにおけるpropositional truncationからの関数の特徴付け。Reedy limitなどを使う。

2. Swan. Irregular models of type theory (2025)

   スライド。Extensional type theoryやunivalent type theoryの、propositional truncationのないモデルを与える。

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

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

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

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

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

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