/-!
# 付録C：研究史と注釈付き文献

## 文献学上の方針

研究史は、現在の概念を過去へそのまま投影しないため、次を区別します。

1. **先行する問題**：逆理、形式化、計算、自然性など、研究を動かした問い。
2. **原文の体系**：その文献が実際に定義・証明した範囲。
3. **後世の再構成**：Curry–Howard対応、BHK解釈など、複数の仕事を束ねる呼称。
4. **Leanでの実装**：歴史的体系から影響を受けても同一ではないkernelとelaborator。

したがって「XがYを発明した」という単独帰属は、一次文献がその主張を支える場合に限ります。
年は原則として刊行年です。原稿年と刊行年が異なる場合は両方を記します。

## 読解のための年代軸

本書の主題は一本の発展史ではなく、少なくとも四つの研究系列が交差して成立しています。

1. **記号論理と基礎論**：Fregeの量化論理、Russellの型理論、Heytingの直観主義論理。
2. **計算の形式体系**：Churchのラムダ計算、Curryの組合せ論理、型付き計算体系。
3. **構成的型理論**：Howardのformulae-as-types、Martin-Löf型理論、CoCとCIC。
4. **構造の数学**：集合・写像・関係の抽象化、圏・関手・自然性・普遍性。

Lean 4はこれらの原典のいずれか一つをそのまま実装したものではありません。依存型理論を核に、
帰納族、宇宙階層、証明無関係な `Prop`、商、型クラス、elaborationを組み合わせた現代の
対話的定理証明環境です。年代順の近さから形式体系の同一性を推論しないでください。

## 記号論理・集合・自然数

* **[FRE79]** Gottlob Frege, *Begriffsschrift, eine der arithmetischen nachgebildete
  Formelsprache des reinen Denkens*, Louis Nebert, Halle, 1879,
  [原著デジタル版](https://gallica.bnf.fr/ark:/12148/bpt6k65658c)。量化、関係、判断を
  二次元記法で組織した原典。現代の `∀` 記法へ翻訳するだけでは、判断線など原体系の
  構造を失うため、現代述語論理そのものとして読まない。
* **[DED88]** Richard Dedekind, *Was sind und was sollen die Zahlen?*, Vieweg,
  Braunschweig, 1888, [ETHデジタル版](https://www.e-rara.ch/zut/content/titleinfo/19451279)。
  自然数を単純無限系と写像により特徴づけ、再帰的定義と帰納的推論を基礎づける原典。
  Leanの `Nat` 宣言の仕様書ではない。
* **[PEA89]** Giuseppe Peano, *Arithmetices principia, nova methodo exposita*,
  Fratres Bocca, Turin, 1889, [EuDML書誌・本文](https://eudml.org/doc/203509)。
  自然数算術を記号的公理体系として提示した原典。現在「Peano公理」と呼ばれる複数の
  一階・二階定式化との差を確認して読む。
* **[ZER08]** Ernst Zermelo, “Untersuchungen über die Grundlagen der Mengenlehre I,”
  *Mathematische Annalen* 65, 261–281, 1908,
  [EuDML本文・書誌](https://eudml.org/doc/158344)。最初の集合論公理化の原典。
  本書の述語集合 `α → Prop` はZermelo集合論の集合概念の実装ではない。
* **[CAN74]** Georg Cantor, “Ueber eine Eigenschaft des Inbegriffes aller reellen
  algebraischen Zahlen,” *Journal für die reine und angewandte Mathematik* 77,
  258–262, 1874, [EuDML本文・書誌](https://eudml.org/doc/148238)。代数的数の可算性と
  実数の非可算性を扱う最初期の原典。後世の一般的なCantorの定理や集合論公理系を同論文へ
  そのまま帰属させない。
* **[ZOR35]** Max Zorn, “A Remark on Method in Transfinite Algebra,” *Bulletin of
  the American Mathematical Society* 41, 667–670, 1935,
  [DOI: 10.1090/S0002-9904-1935-06166-X](https://doi.org/10.1090/S0002-9904-1935-06166-X)。
  後にZornの補題と呼ばれる極大原理を代数学の方法として提示した原典。選択公理との同値性は
  集合論的背景を明示して別に扱う。
* **[TAR55]** Alfred Tarski, “A Lattice-Theoretical Fixpoint Theorem and Its
  Applications,” *Pacific Journal of Mathematics* 5(2), 285–309, 1955,
  [DOI: 10.2140/pjm.1955.5.285](https://doi.org/10.2140/pjm.1955.5.285)。完備格子上の
  単調写像とその不動点集合を扱う基準文献。プログラム意味論における連続性や計算可能な反復近似は
  追加の構造であり、この定理だけへ帰属させない。
* **[SCO70]** Dana S. Scott, *Outline of a Mathematical Theory of Computation*,
  Technical Monograph PRG-2, Oxford University Computing Laboratory, 1970,
  [Oxford書誌・公開版](https://www.cs.ox.ac.uk/publications/publication3720-abstract.html)。データを
  近似順序で捉え、再帰とラムダ計算の数学的意味論を構成する研究計画を提示する一次資料。
* **[SCO72]** Dana S. Scott, “Continuous Lattices,” in *Toposes, Algebraic Geometry
  and Logic*, Lecture Notes in Mathematics 274, 97–136, 1972,
  [DOI: 10.1007/BFb0073967](https://doi.org/10.1007/BFb0073967)。連続格子、位相、関数空間を
  扱う基準文献。本書のω-CPOだけの定義を同論文の全理論と同一視しない。

## 型理論とラムダ計算

* **[RUS08]** Bertrand Russell, “Mathematical Logic as Based on the Theory of Types,”
  *American Journal of Mathematics* 30(3), 222–262, 1908,
  [DOI: 10.2307/2272708](https://doi.org/10.2307/2272708)。
  分岐型理論の一次資料。Leanの宇宙階層の直接仕様ではない。
* **[CHU32]** Alonzo Church, “A Set of Postulates for the Foundation of Logic,”
  *Annals of Mathematics* 33(2), 346–366, 1932,
  [DOI: 10.2307/1968337](https://doi.org/10.2307/1968337)。関数抽象と変換を含む初期の
  論理体系。後に逆理が判明した体系全体と、現在いうラムダ計算の計算核を区別する。
* **[CHU33]** Alonzo Church, “A Set of Postulates for the Foundation of Logic
  (Second Paper),” *Annals of Mathematics* 34(4), 839–864, 1933,
  [DOI: 10.2307/1968702](https://doi.org/10.2307/1968702)。1932年論文に続く第二論文。
  二論文を一つの完成済みな現代的非型付きラムダ計算として遡及的に読まない。
* **[CHU36]** Alonzo Church, “An Unsolvable Problem of Elementary Number Theory,”
  *American Journal of Mathematics* 58(2), 345–363, 1936,
  [DOI: 10.2307/2371045](https://doi.org/10.2307/2371045)。ラムダ定義可能性を用いて
  有効計算可能性を定式化し、決定不能性を示した一次資料。
* **[CHU40]** Alonzo Church, “A Formulation of the Simple Theory of Types,”
  *Journal of Symbolic Logic* 5(2), 56–68, 1940,
  [原論文PDF](https://www.classes.cs.uchicago.edu/archive/2007/spring/32001-1/papers/church-1940.pdf)。
  単純型理論とラムダ変換を結びつけた基準文献。
* **[ML84]** Per Martin-Löf, *Intuitionistic Type Theory*, notes by Giovanni Sambin,
  Bibliopolis, 1984, [公開PDF](https://www.cse.chalmers.se/~peterd/papers/MartinL%C3%B6f1984.pdf)。
  命題・型、Π型・Σ型、同一性型、帰納的対象を理解する歴史的基準点。Leanの型理論と
  規則が全て一致するという意味ではない。
* **[CAR78]** John Cartmell, *Generalised Algebraic Theories and Contextual
  Categories*, D.Phil. thesis, University of Oxford, 1978,
  [著者公開版](https://ncatlab.org/nlab/files/Cartmell-Thesis.pdf)。依存するsortを持つ一般化代数理論と、
  文脈・代入を表すcontextual categoryを構築した一次資料。1986年の論文版と区別する。
* **[DYB96]** Peter Dybjer, “Internal Type Theory,” in *Types for Proofs and
  Programs, TYPES ’95*, Lecture Notes in Computer Science 1158, 120–134,
  Springer, 1996, [DOI: 10.1007/3-540-61780-9_66](https://doi.org/10.1007/3-540-61780-9_66)。
  category with familiesを導入し、依存型の構文に近い圏論的モデルとcoherence問題を扱う一次論文。
* **[DB72]** N. G. de Bruijn, “Lambda Calculus Notation with Nameless Dummies, a
  Tool for Automatic Formula Manipulation, with Application to the Church–Rosser
  Theorem,” *Indagationes Mathematicae (Proceedings)* 75(5), 381–392, 1972,
  [DOI: 10.1016/1385-7258(72)90034-0](https://doi.org/10.1016/1385-7258(72)90034-0)。
  束縛変数名を束縛子までの距離で置き換える記法の一次資料。
* **[PLO75]** Gordon D. Plotkin, “Call-by-Name, Call-by-Value and the λ-Calculus,”
  *Theoretical Computer Science* 1(2), 125–159, 1975,
  [DOI: 10.1016/0304-3975(75)90017-1](https://doi.org/10.1016/0304-3975(75)90017-1)。
  名前呼び・値呼びの評価とプログラミング言語の対応を比較する基準文献。本書のLeanによる
  一段実行関数を原論文の定義そのものとはみなさない。
* **[AC93]** Roberto M. Amadio and Luca Cardelli, “Subtyping Recursive Types,”
  *ACM Transactions on Programming Languages and Systems* 15(4), 575–631, 1993,
  [DOI: 10.1145/155183.155231](https://doi.org/10.1145/155183.155231)。再帰型の同値と
  部分型を、規則、アルゴリズム、無限木の意味論の対応として研究する。本書のiso-recursive型の
  小ステップ体系は同論文の部分型計算そのものではない。
* **[WF94]** Andrew K. Wright and Matthias Felleisen, “A Syntactic Approach to
  Type Soundness,” *Information and Computation* 115(1), 38–94, 1994,
  [DOI: 10.1006/inco.1994.1093](https://doi.org/10.1006/inco.1994.1093)。
  操作的意味論、subject reduction、進行型の議論をプログラミング言語の型健全性へ適用する
  基準文献。本章の純粋STLCを同論文のStandard ML核と同一視しない。
* **[TAI67]** William W. Tait, “Intensional Interpretations of Functionals of
  Finite Type I,” *Journal of Symbolic Logic* 32(2), 198–212, 1967,
  [DOI: 10.2307/2271658](https://doi.org/10.2307/2271658)。有限型の汎関数に対する
  解釈を展開する一次資料。後世のreducibility candidatesや本章のLean定義と同一視せず、
  正規化証明法の系譜を読む基準点とする。
* **[REY83]** John C. Reynolds, “Types, Abstraction and Parametric Polymorphism,”
  in *Information Processing 83*, IFIP, 513–523, 1983。
  多相型の関係解釈と抽象化定理をプログラミング言語の文脈で展開する一次資料。後世の
  “theorems for free”という標語や本書のLean構造を同論文へそのまま帰属させない。
* **[WAD89]** Philip Wadler, “Theorems for Free!,” in *Proceedings of FPCA ’89*,
  347–359, ACM Press, 1989,
  [DOI: 10.1145/99370.99404](https://doi.org/10.1145/99370.99404)。Reynoldsの
  抽象化定理から多相プログラムの方程式を導く方法を展開した基準文献。適用可能性は言語の
  効果・部分性・型機構の仮定とともに読む。
* **[CH88]** Thierry Coquand and Gérard Huet, “The Calculus of Constructions,”
  *Information and Computation* 76(2–3), 95–120, 1988,
  [DOI: 10.1016/0890-5401(88)90005-3](https://doi.org/10.1016/0890-5401(88)90005-3)。
  構成計算（CoC）の基本理論を提示した基準文献。帰納型やLean固有のkernel機能を含む
  現代の体系と同一ではない。
* **[BAR91]** Henk Barendregt, “Introduction to Generalized Type Systems,”
  *Journal of Functional Programming* 1(2), 125–154, 1991,
  [DOI: 10.1017/S0956796800020025](https://doi.org/10.1017/S0956796800020025)。
  型付きラムダ計算を一般化型システムとして統一し、CoCを八頂点のラムダ・キューブとして
  分析した一次資料。
* **[HS98]** Martin Hofmann and Thomas Streicher, “The Groupoid Interpretation of
  Type Theory,” in *Twenty-Five Years of Constructive Type Theory*, Oxford Logic
  Guides 36, 83–111, 1998,
  [DOI: 10.1093/oso/9780198501275.003.0008](https://doi.org/10.1093/oso/9780198501275.003.0008)。
  内包的型理論の同一性型を群oidで解釈し、同一性証明の一意性が一般には導けないことを示す
  基準文献。後の一価性公理そのものを述べた文献ではない。
* **[AW09]** Steve Awodey and Michael A. Warren, “Homotopy Theoretic Models of
  Identity Types,” *Mathematical Proceedings of the Cambridge Philosophical Society*
  146(1), 45–55, 2009,
  [DOI: 10.1017/S0305004108001783](https://doi.org/10.1017/S0305004108001783)。
  model categoryにおけるMartin-Löf型理論のモデルを構成し、同一性型とホモトピー論の接続を
  展開する。一価的基礎全体の標準教科書とは役割が異なる。
* **[HOTT13]** The Univalent Foundations Program, *Homotopy Type Theory:
  Univalent Foundations of Mathematics*, Institute for Advanced Study, 2013,
  [公式公開版](https://homotopytypetheory.org/book/)。一価性、高次帰納型、ホモトピーレベルを
  系統的に扱う共同執筆の標準文献。Lean 4の `Eq : Prop` の仕様書ではない。

この系列を読むときは、Russellの型による階層化、Churchの単純型理論、Martin-Löfの
判断的な型理論、PTSによる再分類を一つの体系の版違いとして扱わないことが重要です。
特に同じ `type` という語でも、逆理回避の階層、項を分類する対象、命題の意味説明、
プログラム静的意味論という役割が異なります。

## 構成的論理と命題＝型対応

* **[GEN35]** Gerhard Gentzen, “Untersuchungen über das logische Schließen I–II,”
  *Mathematische Zeitschrift* 39, 176–210 and 405–431, 1935,
  [Part I DOI: 10.1007/BF01201353](https://doi.org/10.1007/BF01201353),
  [Part II DOI: 10.1007/BF01201363](https://doi.org/10.1007/BF01201363)。自然演繹と
  シーケント計算を導入し、正規化とcut除去へ至る証明論的構造を扱う原典。現在のLeanの
  tactic状態や証明項をGentzenの原体系そのものとはみなさない。
* **[HEY30]** Arend Heyting, “Die formalen Regeln der intuitionistischen Logik I–III,”
  *Sitzungsberichte der Preußischen Akademie der Wissenschaften*, 42–56, 57–71,
  158–169, 1930, [書誌情報](https://bibbase.org/network/publication/heyting-dieformalenregelnderintuitionistischenlogikiiiiii-1930)。
  直観主義命題・述語論理の形式化。Brouwerの研究計画そのものとは区別する。
* **[KOL32]** A. Kolmogorov, “Zur Deutung der intuitionistischen Logik,”
  *Mathematische Zeitschrift* 35, 58–65, 1932,
  [EuDML本文・書誌](https://eudml.org/doc/168345)。直観主義論理を問題と解法として読む
  解釈の一次資料。後世の “BHK” という総称は同時代の固有名ではない。
* **[CUR34]** H. B. Curry, “Functionality in Combinatory Logic,” *PNAS* 20(11),
  584–590, 1934, [DOI: 10.1073/pnas.20.11.584](https://doi.org/10.1073/pnas.20.11.584)。
  組合せ子の型と含意論理の対応の早い一次資料。
* **[HOW80]** William A. Howard, “The Formulae-as-Types Notion of Construction,” in
  *To H. B. Curry*, 479–490, Academic Press, 1980,
  [原論文PDF](https://www.cs.cmu.edu/~crary/819-f09/Howard80.pdf)。原稿は1969年。Curryの結果を
  単に再掲したのではなく、自然演繹と構成の対応を広げる。

## プログラミング言語の型

* **[ROB65]** J. A. Robinson, “A Machine-Oriented Logic Based on the Resolution
  Principle,” *Journal of the ACM* 12(1), 23–41, 1965,
  [DOI: 10.1145/321250.321253](https://doi.org/10.1145/321250.321253)。resolution原理による
  自動推論の一部として単一化アルゴリズムを提示した一次資料。後世の型推論器に現れる単一化だけを
  切り出して原論文全体とみなさない。
* **[HIN69]** J. Roger Hindley, “The Principal Type-Scheme of an Object in
  Combinatory Logic,” *Transactions of the American Mathematical Society* 146,
  29–60, 1969, [DOI: 10.2307/1995158](https://doi.org/10.2307/1995158)。組合せ論理の
  対象に対するprincipal type-schemeを扱う。MLの型推論アルゴリズムを記述した論文ではない。
* **[MIL78]** Robin Milner, “A Theory of Type Polymorphism in Programming,”
  *Journal of Computer and System Sciences* 17(3), 348–375, 1978,
  [DOI: 10.1016/0022-0000(78)90014-4](https://doi.org/10.1016/0022-0000(78)90014-4)。
  プログラミング言語の多相型規律、Algorithm W、意味論的・構文的健全性を提示する一次資料。
* **[DM82]** Luís Damas and Robin Milner, “Principal Type-Schemes for Functional
  Programs,” *POPL ’82*, 207–212, 1982,
  [DOI: 10.1145/582153.582176](https://doi.org/10.1145/582153.582176)。関数型プログラムの
  principal type-schemeを研究する基準文献。依存型や型クラスを含むLeanのelaborationへ
  完全性をそのまま移せるわけではない。
* **[DK13]** Jana Dunfield and Neelakantan R. Krishnaswami, “Complete and Easy
  Bidirectional Typechecking for Higher-Rank Polymorphism,” *ICFP ’13*, 429–442,
  2013, [DOI: 10.1145/2500365.2500582](https://doi.org/10.1145/2500365.2500582)。
  高階ランク多相を対象に、証明論に基づく双方向型付けと健全・完全なアルゴリズムを与える。
  本書の単相の合成・検査判断は、その情報流を理解するための限定された例である。

* **[FP91]** Tim Freeman and Frank Pfenning, “Refinement Types for ML (Extended
  Abstract),” *PLDI ’91*, 268–277, 1991,
  [著者側書誌](https://hjemmesider.diku.dk/~henglein/bib/publications/frpf91.html)。
  “refinement types” をMLの型システムとして定式化した代表的な初期文献。Leanの
  `Subtype` と同じ型検査方式ではない。
* **[DYB94]** Peter Dybjer, “Inductive Families,” *Formal Aspects of Computing* 6,
  440–465, 1994, [DOI: 10.1007/BF01211308](https://doi.org/10.1007/BF01211308)。
  Martin-Löf型理論における一般化された帰納族の形成・導入・再帰を扱う。
* **[WB89]** Philip Wadler and Stephen Blott, “How to Make Ad-hoc Polymorphism Less
  Ad Hoc,” *POPL ’89*, 60–76, 1989,
  [DOI: 10.1145/75277.75283](https://doi.org/10.1145/75277.75283)。
  Hindley–Milner系に型クラスを導入した一次資料。Leanのインスタンス探索はこの発想を
  発展させているが、同じ推論系ではない。

## 圏論

* **[EM45]** Samuel Eilenberg and Saunders Mac Lane, “General Theory of Natural
  Equivalences,” *Transactions of the American Mathematical Society* 58, 231–294,
  1945, [AMS原論文PDF](https://www.ams.org/journals/tran/1945-058-00/S0002-9947-1945-0013131-6/S0002-9947-1945-0013131-6.pdf)。
  圏、関手、自然同値を体系的に導入した一次資料。現在の教科書的な普遍性・随伴・極限の
  全体系をこの一論文へ遡及的に帰属させない。

Eilenberg–Mac Laneの1945年論文の中心語は圏・関手・自然同値です。現在の教科書で中心的な
普遍性、随伴、表現可能性、極限の統一的提示は、その後の研究と教科書化を経ています。
したがって本書の積・余積の普遍性を [EM45] の定義の直接的な写しとはしません。

* **[YON54]** Nobuo Yoneda, “On the Homology Theory of Modules,”
  *Journal of the Faculty of Science, University of Tokyo, Section I* 7,
  193–227, 1954,
  [Stacks Project書誌](https://stacks.math.columbia.edu/bibliography/Yoneda-homology)。
  加群のホモロジー理論を主題とする一次資料で、その中の補題が後に米田の補題として
  一般圏論の中心定理になった。論文全体を現代の米田埋め込みだけへ還元しない。
* **[GRO57]** Alexander Grothendieck, “Sur quelques points d'algèbre homologique,”
  *Tôhoku Mathematical Journal*, Second Series 9(2), 119–183, 1957,
  [DOI: 10.2748/tmj/1178244839](https://doi.org/10.2748/tmj/1178244839)。アーベル圏と
  導来関手の一般理論を構築し、アーベル群の層を主要例として扱う一次資料。後のサイトと
  Grothendieckトポスの全理論を、この論文へ遡及的に帰属させない。
* **[KAN58]** Daniel M. Kan, “Adjoint Functors,” *Transactions of the American
  Mathematical Society* 87, 294–329, 1958,
  [DOI: 10.1090/S0002-9947-1958-0131451-0](https://doi.org/10.1090/S0002-9947-1958-0131451-0)。
  随伴関手と後にKan拡張と呼ばれる構成を導入した一次資料。現代の単位・余単位による
  定式化との記法差は [MAC98] と照合する。
* **[MAC63]** Saunders Mac Lane, “Natural Associativity and Commutativity,”
  *Rice University Studies* 49(4), 28–46, 1963,
  [原論文PDF](https://www.mscs.dal.ca/~selinger/papers/papers/graphical-bib/public/MacLane-natural-associativity-and-commutativity-1963.pdf)。
  自然な結合性・可換性とその整合条件を研究した一次資料。現在のモノイダル圏の定義全体や
  mathlibの正規化手続を同論文へそのまま遡及させない。
* **[EK66]** Samuel Eilenberg and G. M. Kelly, “Closed Categories,” in
  *Proceedings of the Conference on Categorical Algebra, La Jolla 1965*,
  Springer, 421–562, 1966,
  [DOI: 10.1007/978-3-642-99902-4](https://doi.org/10.1007/978-3-642-99902-4)。
  閉圏と内部homを体系化した一次資料。後の [KEL82] における豊穣圏論全体の定式化とは時期と範囲を区別する。
* **[KLE65]** Heinrich Kleisli, “Every Standard Construction Is Induced by a Pair
  of Adjoint Functors,” *Proceedings of the American Mathematical Society* 16,
  544–546, 1965,
  [DOI: 10.1090/S0002-9939-1965-0177024-4](https://doi.org/10.1090/S0002-9939-1965-0177024-4)。
  当時standard constructionなどと呼ばれた構造から随伴を構成する一次資料。
* **[EM65]** Samuel Eilenberg and John C. Moore, “Adjoint Functors and Triples,”
  *Illinois Journal of Mathematics* 9, 381–398, 1965,
  [DOI: 10.1215/ijm/1256068141](https://doi.org/10.1215/ijm/1256068141)。
  tripleとその代数の圏を随伴との関係から研究した一次資料。後代の “monad” という名称と
  現行記法は [MAC98] と区別して読む。
* **[BEC67]** Jonathan Mock Beck, *Triples, Algebras and Cohomology*, PhD thesis,
  Columbia University, 1967; reprinted in *Reprints in Theory and Applications of
  Categories* 2, 1–59, 2003,
  [TAC公開版](https://tac.mta.ca/tac/reprints/articles/2/tr2.pdf)。
  tripleによるコホモロジーと代数を展開する一次資料。2003年版の編集者序文が1964年草稿の
  流通を記録するため、原稿年、学位論文年、再刊年を区別する。現代のBeck型定理の諸版は
  仮定が異なるので、単一の現行定式化を無注釈で同論文へ帰属させない。
* **[LAM68]** Joachim Lambek, “A Fixpoint Theorem for Complete Categories,”
  *Mathematische Zeitschrift* 103, 151–161, 1968,
  [DOI: 10.1007/BF01110627](https://doi.org/10.1007/BF01110627)。
  圏論的な不動点定理を扱う一次資料。始代数の構造射が同型になる、現在Lambekの補題と
  呼ばれる主張を、後代のデータ型意味論だけへ限定して読まない。
* **[SGA1]** Alexander Grothendieck, *Revêtements étales et groupe fondamental
  (SGA 1)*, Lecture Notes in Mathematics 224, Springer, 1971,
  [Stacks Project書誌](https://stacks.math.columbia.edu/bibliography/SGA1)。第VI exposé
  “Catégories fibrées et descente” はファイバー圏、Cartesian射、降下を代数幾何の文脈で
  体系化する一次資料。セミナー実施時期と刊行年、および後の型理論的解釈を区別する。
* **[BEN85]** Jean Bénabou, “Fibered Categories and the Foundations of Naive
  Category Theory,” *Journal of Symbolic Logic* 50(1), 10–37, 1985,
  [DOI: 10.2307/2273784](https://doi.org/10.2307/2273784)。ファイバー圏を圏論の
  基礎づけと結びつけて展開する一次論文。Grothendieckの幾何学的使用と目的を区別して読む。
* **[SEE84]** R. A. G. Seely, “Locally Cartesian Closed Categories and Type
  Theory,” *Mathematical Proceedings of the Cambridge Philosophical Society*
  95(1), 33–48, 1984,
  [DOI: 10.1017/S0305004100061284](https://doi.org/10.1017/S0305004100061284)。
  局所デカルト閉圏とMartin-Löf型理論の対応を体系的に論じる一次論文。後続研究による
  coherence条件の修正や双圏同値の精密化を、原論文の主張と区別して読む。
* **[GIR87]** Jean-Yves Girard, “Linear Logic,” *Theoretical Computer Science*
  50(1), 1–102, 1987,
  [DOI: 10.1016/0304-3975(87)90045-4](https://doi.org/10.1016/0304-3975(87)90045-4)。
  線形論理を、乗法的・加法的・指数的結合子、線形否定、cut除去、coherent space意味論とともに
  導入した一次論文。後世の資源解釈だけへ論文全体を還元せず、証明論と意味論の構成を区別して読む。
* **[SEE89]** R. A. G. Seely, “Linear Logic, *-Autonomous Categories and Cofree
  Coalgebras,” in *Categories in Computer Science and Logic*, Contemporary
  Mathematics 92, 371–382, American Mathematical Society, 1989,
  [DOI: 10.1090/conm/092/1003210](https://doi.org/10.1090/conm/092/1003210)。
  *-自律圏と余自由余代数による線形論理の圏論モデルを論じる一次資料。後続研究で修正・精密化された
  Seely categoryの定義と、原論文の定式化を同一視しない。
* **[BEN95]** P. N. Benton, “A Mixed Linear and Non-Linear Logic: Proofs, Terms
  and Models,” in *Computer Science Logic, CSL ’94*, Lecture Notes in Computer
  Science 933, 121–135, Springer, 1995,
  [DOI: 10.1007/BFb0022251](https://doi.org/10.1007/BFb0022251)。
  デカルト閉な非線形世界と対称モノイダル閉な線形世界を随伴で結ぶLNL体系の一次論文。1994年の
  会議と1995年の選集刊行、および同題の長い技術報告を区別する。
* **[MOG91]** Eugenio Moggi, “Notions of Computation and Monads,” *Information
  and Computation* 93(1), 55–92, 1991,
  [DOI: 10.1016/0890-5401(91)90052-4](https://doi.org/10.1016/0890-5401(91)90052-4)。
  値と計算を区別する計算的ラムダ計算を導入し、複数の計算概念を強いモナドの圏論的意味論で
  統一した一次論文。1989年の会議論文と1991年の拡張誌上版、および後代の言語APIを区別する。
* **[PP03]** Gordon Plotkin and John Power, “Algebraic Operations and Generic
  Effects,” *Applied Categorical Structures* 11(1), 69–94, 2003,
  [DOI: 10.1023/A:1023064908962](https://doi.org/10.1023/A:1023064908962)。
  代数的演算とgeneric effectの対応を、強いモナドと豊穣圏論の設定で研究した一次論文。
  2001年の先行会議論文と、題名・範囲を同一視しない。
* **[PP13]** Gordon Plotkin and Matija Pretnar, “Handling Algebraic Effects,”
  *Logical Methods in Computer Science* 9(4), article 23, 2013,
  [DOI: 10.2168/LMCS-9(4:23)2013](https://doi.org/10.2168/LMCS-9(4:23)2013)。
  自由モデルと準同型によって例外処理を一般の代数的効果ハンドラへ拡張した一次論文。2009年の
  “Handlers of Algebraic Effects” 会議版と、題名・内容・刊行年を区別する。
* **[SGA4]** Michael Artin, Alexander Grothendieck, and Jean-Louis Verdier, eds.,
  *Théorie des topos et cohomologie étale des schémas*, Séminaire de Géométrie
  Algébrique du Bois-Marie 1963–1964, Lecture Notes in Mathematics 269, 270, 305,
  Springer, 1972–1973,
  [Tome 2, DOI: 10.1007/BFb0061319](https://doi.org/10.1007/BFb0061319)。サイト、トポス、
  降下、エタール・コホモロジーを展開する複数巻の基準的な一次資料。各 exposé の著者と
  巻を確認し、全内容を単著の一時点の定義として引用しない。
* **[LAW70]** F. William Lawvere, “Quantifiers and Sheaves,” in *Actes du
  Congrès International des Mathématiciens, Nice 1970*, vol. 1, 329–334,
  Gauthier-Villars, 1971。量化を再添字付けの随伴として捉え、層と論理を結ぶ一次資料。
  1970年の講演と1971年の会議録刊行を区別する。
* **[TIE72]** Myles Tierney, “Sheaf Theory and the Continuum Hypothesis,” in
  *Toposes, Algebraic Geometry and Logic*, Lecture Notes in Mathematics 274,
  13–42, Springer, 1972,
  [DOI: 10.1007/BFb0073963](https://doi.org/10.1007/BFb0073963)。層トポスの内部論理を
  集合論の独立性へ応用する一次資料。後代に整理された初等トポスの標準定義全体を、この論文だけへ帰属させない。

## 帰納・余帰納・不動点

* **[GTWW77]** Joseph A. Goguen, James W. Thatcher, Eric G. Wagner, and Jesse B. Wright,
  “Initial Algebra Semantics and Continuous Algebras,” *Journal of the ACM* 24(1),
  68–95, 1977,
  [DOI: 10.1145/321992.321997](https://doi.org/10.1145/321992.321997)。始代数意味論を
  連続代数と結び、代数的仕様とプログラム意味論へ展開した一次資料。Leanの帰納型生成機構や
  依存除去原理を、この論文の定式化とそのまま同一視しない。
* **[RUT00]** J. J. M. M. Rutten, “Universal Coalgebra: A Theory of Systems,”
  *Theoretical Computer Science* 249(1), 3–80, 2000,
  [CWI書誌・著者公開版](https://ir.cwi.nl/pub/48/)。状態遷移系、双模倣、終余代数を
  普遍余代数の枠組みで統一する基準的な研究論文。Leanの再帰定義機構の仕様ではない。
* **[SP82]** M. B. Smyth and G. D. Plotkin, “The Category-Theoretic Solution of
  Recursive Domain Equations,” *SIAM Journal on Computing* 11(4), 761–783, 1982,
  [DOI: 10.1137/0211062](https://doi.org/10.1137/0211062)。CPO上の連続写像の最小不動点を、
  順序豊穣圏上の連続関手と埋込みの圏へ拡張する一次論文。1979年の投稿と1982年の刊行を区別する。
* **[FRE91]** Peter J. Freyd, “Algebraically Complete Categories,” in *Category
  Theory: Proceedings of the International Conference Held in Como, Italy,
  July 22–28, 1990*, Lecture Notes in Mathematics 1488, 95–104, Springer, 1991,
  [会議録DOI: 10.1007/BFb0084207](https://doi.org/10.1007/BFb0084207)。代数的完備性を
  一般の圏論的条件として研究する一次資料。1990年の会議と1991年の刊行を区別する。
* **[GH04]** Nicola Gambino and Martin Hyland, “Wellfounded Trees and Dependent
  Polynomial Functors,” in *Types for Proofs and Programs, TYPES 2003*, Lecture
  Notes in Computer Science 3085, 210–225, Springer, 2004,
  [DOI: 10.1007/978-3-540-24849-1_14](https://doi.org/10.1007/978-3-540-24849-1_14)。
  W型を局所デカルト閉圏の依存多項式関手と結び、その始代数を研究する一次論文。本書の
  `Type` 上の一変数多項式関手は、この一般理論の全てを形式化するものではない。
* **[AMM25]** Jiří Adámek, Stefan Milius, and Lawrence S. Moss,
  *Initial Algebras and Terminal Coalgebras: The Theory of Fixed Points of Functors*,
  Cambridge Tracts in Theoretical Computer Science 62, Cambridge University Press, 2025,
  [DOI: 10.1017/9781108884112](https://doi.org/10.1017/9781108884112)。標準鎖による始代数・
  終余代数の構成、関手の不動点、完備半順序や距離空間との接続を研究書として追う文献。

帰納型、順序理論の最小不動点、関手の始代数は密接に関係しますが、存在定理の仮定と等号の
意味が異なります。同様に、余帰納的データ、最大不動点として定義した述語、終余代数による
振舞いの意味論を一つの実装機構として扱いません。[RUT00] は余代数的意味論、[AMM25] は
代数・余代数と不動点の一般理論を読むために用います。

## 標準研究書への読書経路

原典だけでは、現代の記法・定理配置・メタ理論を体系的に学ぶことは困難です。次の研究書は
原典の代用ではなく、現在の標準的定式化と研究語彙を獲得するために使います。

* **[GLT89]** Jean-Yves Girard, Yves Lafont, and Paul Taylor, *Proofs and Types*,
  Cambridge Tracts in Theoretical Computer Science 7, Cambridge University Press,
  1989, corrected reprint 1990,
  [著者公開PDF](https://www.paultaylor.eu/stable/prot.pdf)。自然演繹、正規化、
  単純型付きラムダ計算、System Fをproof theory側から読む標準文献。
* **[TAPL02]** Benjamin C. Pierce, *Types and Programming Languages*, MIT Press,
  2002, [出版社書誌](https://mitpress.mit.edu/9780262162098/types-and-programming-languages/)。
  構文、操作的意味論、型判断、保存・進行を論文標準の推論規則で学ぶための教科書。
* **[PFPL16]** Robert Harper, *Practical Foundations for Programming Languages*,
  2nd ed., Cambridge University Press, 2016,
  [DOI: 10.1017/CBO9781316576892](https://doi.org/10.1017/CBO9781316576892)。
  判断と規則を中心にプログラミング言語の静的・動的意味論を構成する研究書。第2版は
  type refinementsも扱う。
* **[LS86]** J. Lambek and P. J. Scott, *Introduction to Higher-Order Categorical
  Logic*, Cambridge Studies in Advanced Mathematics 7, Cambridge University Press,
  1986, [書誌情報](https://books.google.com/books/about/Introduction_to_Higher_Order_Categorical.html?id=rx5hQgAACAAJ)。
  型付きラムダ計算・高階論理とCartesian closed categoryの対応を学ぶ標準文献。
* **[JAC99]** Bart Jacobs, *Categorical Logic and Type Theory*, Studies in Logic and
  the Foundations of Mathematics 141, North-Holland, Elsevier, 1999,
  [著者書誌](https://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html)。ファイブレーションを統一概念として、
  述語論理・依存型理論・圏論的意味論を体系化する標準研究書。原典ではなく現代的定式化の参照に用いる。
* **[HOF97]** Martin Hofmann, “Syntax and Semantics of Dependent Types,” in
  Andrew M. Pitts and Peter Dybjer, eds., *Semantics and Logics of Computation*,
  79–130, Cambridge University Press, 1997,
  [DOI: 10.1017/CBO9780511526619.004](https://doi.org/10.1017/CBO9780511526619.004)。
  依存型構文と抽象的意味論、型形成子、外延的・内包的構成の関係を読む標準的な章。
* **[MAC98]** Saunders Mac Lane, *Categories for the Working Mathematician*,
  2nd ed., Graduate Texts in Mathematics 5, Springer, 1998。圏論の標準的な研究語彙と
  普遍構成を参照する文献。初版は1971年であり、版を区別する。
* **[KEL82]** G. M. Kelly, *Basic Concepts of Enriched Category Theory*, London
  Mathematical Society Lecture Note Series 64, Cambridge University Press, 1982;
  corrected reprint, *Reprints in Theory and Applications of Categories* 10, 1–136,
  2005, [TAC公開版](https://tac.mta.ca/tac/reprints/articles/10/tr10.pdf)。豊穣圏、
  豊穣化されたend・coend、Kan拡張を体系的に扱う研究書。1982年版と訂正を含む2005年再刊を区別する。
* **[MM92]** Saunders Mac Lane and Ieke Moerdijk, *Sheaves in Geometry and Logic:
  A First Introduction to Topos Theory*, Universitext, Springer, 1992。前層、篩、
  Grothendieck位相、層化、トポスを現代的な圏論の記法で結び直す標準研究書。SGA 4の
  一次資料としてではなく、定義間の同値と論理への接続を学ぶために用いる。
* **[LEI14]** Tom Leinster, *Basic Category Theory*, Cambridge Studies in Advanced
  Mathematics 143, Cambridge University Press, 2014,
  [DOI: 10.1017/CBO9781107360068](https://doi.org/10.1017/CBO9781107360068)。
  普遍性を随伴・表現可能関手・極限の三方向から読み直すための導入的研究書。

推奨順は一意ではありません。第4・11章の構文論から [TAPL02] または [PFPL16] へ、
第6–9章のproofs-as-termsから [GLT89] へ、第42–44章の普遍性から [LEI14]、その後
[MAC98] または [LS86] へ進む経路を本書の章末で示します。

## 二次的な歴史研究

一次文献だけでは用語の成立や受容史を記述できません。直観主義論理については
[Stanford Encyclopedia of Philosophy, “The Development of Intuitionistic Logic”](https://plato.stanford.edu/entries/intuitionistic-logic-development/)
を文献案内として利用します。二次資料は一次文献の代用ではなく、版、翻訳、呼称の
後代性を確認するために使います。

記号論理については [Stanford Encyclopedia of Philosophy, “Frege’s Logic”](https://plato.stanford.edu/entries/frege-logic/)、
集合論については [“The Early Development of Set Theory”](https://plato.stanford.edu/entries/settheory-early/)、
型理論については [“Intuitionistic Type Theory”](https://plato.stanford.edu/entries/type-theory-intuitionistic/)、
圏論については [“Category Theory”](https://plato.stanford.edu/entries/category-theory/) を、
帰属・用語・受容史を確認する入口として用います。

## 現行Leanの仕様を確認する資料

歴史的体系と現在の実装の差は、一次文献だけでなく実装側の現行仕様で確認します。

* **[LEAN-DTT]** Lean project, *Theorem Proving in Lean 4*, “Dependent Type Theory,”
  [公式文書](https://lean-lang.org/theorem_proving_in_lean4/Dependent-Type-Theory/)。
  Leanの依存関数型、宇宙階層、宇宙多相を説明する。歴史的CoCの仕様書ではない。
* **[LEAN-FAQ]** Lean project, “Is Lean just like Rocq?”, *Frequently Asked Questions*,
  [公式文書](https://lean-lang.org/faq/)。LeanとRocqの宇宙累積性、
  証明無関係性、再帰のkernel上の扱いなどの差を確認する現行資料。
* **[LEAN-REF]** Lean project, *The Lean Language Reference*,
  [公式文書](https://lean-lang.org/doc/reference/latest/)。関数型、`Prop`、宇宙、帰納型、
  商、elaborationを現行Lean 4の仕様として確認する。歴史的由来や一般の型理論の定義は
  このマニュアルだけから推論しない。
* **[LEAN-REC]** Lean project, *The Lean Language Reference*, “Recursive Definitions,”
  [公式文書](https://lean-lang.org/doc/reference/latest/Definitions/Recursive-Definitions/)。
  構造再帰、整礎再帰、部分不動点、帰納的・余帰納的述語、`partial` の論理上の差を確認する。
  圏論的な始代数・終余代数の一般理論はこの仕様だけから推論しない。
* **[MATHLIB]** Lean community, *Mathlib Documentation*,
  [CategoryTheory.Category.Basic](https://leanprover-community.github.io/mathlib4_docs/Mathlib/CategoryTheory/Category/Basic.html)。
  mathlibの圏、射の宇宙、型クラスによる圏構造の現行APIを確認する入口。圏論の数学的定義は
  先に定義と定理を数学的記法で理解し、API設計と区別して読む。

## 文献を読むときの検査項目

1. その文献の対象言語・メタ言語・基礎理論は何か。
2. `type`、`set`、`proposition`、`equality` がどの判断で導入されるか。
3. 等式は構文同一性、変換可能性、対象理論内の命題のどれか。
4. 原典の記法を現代記法へ翻訳した箇所で何が失われたか。
5. 定理は原典にあるのか、後世の再構成・名称なのか。
6. Lean形式化は同じ体系を実装するのか、概念だけを別体系内でモデル化するのか。
-/