import FormalLab.Foundation.TermsAndTypes import FormalLab.Foundation.Functions import FormalLab.Foundation.InductiveTypes import FormalLab.Foundation.UntypedLambdaCalculus import FormalLab.Foundation.Universes import FormalLab.Logic.Propositions import FormalLab.Logic.Connectives import FormalLab.Logic.Quantifiers import FormalLab.Logic.Equality import FormalLab.Logic.ProofSystems import FormalLab.TypeTheory.SimplyTypedLambdaCalculus import FormalLab.TypeTheory.StructuralRules import FormalLab.TypeTheory.OperationalSemantics import FormalLab.TypeTheory.RecursiveTypes import FormalLab.TypeTheory.TypeSafety import FormalLab.TypeTheory.Normalization import FormalLab.TypeTheory.SystemF import FormalLab.TypeTheory.LogicalRelations import FormalLab.TypeTheory.Parametricity import FormalLab.Mathematics.Sets import FormalLab.Mathematics.FunctionProperties import FormalLab.Mathematics.Relations import FormalLab.Mathematics.NaturalNumberInduction import FormalLab.Mathematics.Orders import FormalLab.Mathematics.Cardinality import FormalLab.Recursion.WellFounded import FormalLab.Recursion.Lattices import FormalLab.Recursion.FixedPoints import FormalLab.Recursion.CoinductivePredicates import FormalLab.Recursion.DomainTheory import FormalLab.TypeTheory.DependentTypes import FormalLab.TypeTheory.IdentityTypes import FormalLab.TypeTheory.PureTypeSystems import FormalLab.TypeTheory.SubtypesAndRefinements import FormalLab.TypeTheory.IndexedFamilies import FormalLab.TypeTheory.GeneralInductiveFamilies import FormalLab.TypeTheory.WTypes import FormalLab.TypeTheory.HomotopyTypeTheory import FormalLab.TypeTheory.Quotients import FormalLab.TypeTheory.TypeClasses import FormalLab.TypeTheory.TypeInference import FormalLab.CategoryTheory.InitialAndTerminal import FormalLab.CategoryTheory.Products import FormalLab.CategoryTheory.Coproducts import FormalLab.CategoryTheory.Categories import FormalLab.CategoryTheory.Functors import FormalLab.CategoryTheory.NaturalTransformations import FormalLab.CategoryTheory.Equivalences import FormalLab.CategoryTheory.Limits import FormalLab.CategoryTheory.RepresentableFunctors import FormalLab.CategoryTheory.YonedaLemma import FormalLab.CategoryTheory.Adjunctions import FormalLab.CategoryTheory.Monads import FormalLab.CategoryTheory.EndofunctorAlgebras import FormalLab.CategoryTheory.InitialAlgebras import FormalLab.CategoryTheory.EndofunctorCoalgebras import FormalLab.CategoryTheory.FinalCoalgebras import FormalLab.CategoryTheory.Presheaves import FormalLab.CategoryTheory.Sites import FormalLab.CategoryTheory.Sheaves import FormalLab.CategoryTheory.Monadicity import FormalLab.CategoryTheory.EndsAndCoends import FormalLab.CategoryTheory.KanExtensions import FormalLab.CategoryTheory.MonoidalCategories import FormalLab.CategoryTheory.EnrichedCategories import FormalLab.Bridges.InductionAndInitialAlgebras import FormalLab.Bridges.PolynomialFunctorsAndWTypes import FormalLab.Bridges.CoinductionAndFinalCoalgebras import FormalLab.Bridges.ThreeNotionsOfInfinity import FormalLab.Bridges.CartesianClosedCategories import FormalLab.Bridges.STLCCategoricalSemantics import FormalLab.Bridges.SlicesIndexedCategoriesAndFibrations import FormalLab.Bridges.LocallyCartesianClosedCategories import FormalLab.Bridges.DependentTypeCategoricalSemantics import FormalLab.Bridges.MonoidalClosedCategories import FormalLab.Bridges.LinearLogicAndResourceSemantics import FormalLab.Bridges.MonadsAndComputationalEffects import FormalLab.Bridges.ToposesAndCategoricalLogic import FormalLab.Bridges.RecursiveTypeSemantics import FormalLab.Appendix.Notation import FormalLab.Appendix.Terminology import FormalLab.Appendix.HistoricalSources import FormalLab.Appendix.ExerciseSolutions /-! # Formal Lab 本書は、論理・数学・型理論・圏論を、通常の数学的記述とLeanによる検査を往復しながら学ぶための 教科書です。初めから順に通読することも、後の目的別案内から必要な経路を選ぶこともできます。 各章は一つの主題を、問題となる具体例、定義と定理、形式化、研究史、問題の順に掘り下げます。 ## 本書が答える問い 数学の文を、Leanが検査できる型と項へどう翻訳するのか。その翻訳によって、命題、 述語、関数、関係、集合、ラムダ計算、依存型、篩型、構成計算（CoC）、普遍性、 双対性がどう一つの体系としてつながるのか。本書は操作の暗記ではなく、この二つの問いを 追います。 ## 読書契約 各章は編集用の前提一覧からではなく、既知の具体例に残る問題から始まります。導入本文を読み、 何がまだ定義されていないか、どの構成または証明でそれを解決するかを予想してください。 章末の「要点」は暗記項目ではなく、本文を閉じた後に自分で再構成できるかを確かめる索引です。 「問題」は定義の再生だけでなく、証明、反例、Leanでの実装、数学的記法とLean表現の相互翻訳、 文献読解を含みます。 定義と定理は、まず通常の数学的記法で変数、仮定、結論が分かるように述べます。その近くに置かれた Leanの宣言は、同じ内容を型と項として再構成したものです。二つを見比べれば、数式では省略されやすい 引数や束縛を発見でき、コードを隠せば数学的な定義と証明を自力で復元できます。kernel、elaborator、 tactic、暗黙引数などLeanの動作が結論に関係するときは、その箇所で観察できる働きと数学的内容への 影響を説明します。 ## 本書の構成 章番号は引用と参照の基準です。初めから通読すれば新しい概念を順に積み上げられます。既に知っている 内容がある場合や特定の主題を先に学びたい場合は、後の「目的別の読書案内」から必要な章を選べます。 ### 第I部　形式化の基礎 #### 第1章　型・項・定義・計算 `FormalLab.Foundation.TermsAndTypes` Leanで式を読むための最小単位を学びます。型判断、定義、定義的な計算、命題として証明する等式を 区別し、以後の全章で使う読み方を確立します。 #### 第2章　関数・適用・合成 `FormalLab.Foundation.Functions` 関数を入力から出力への規則として定め、ラムダ抽象、適用、部分適用、合成を数学的記法とLeanの型の 双方から読みます。 #### 第3章　帰納型・場合分け・再帰・構造体 `FormalLab.Foundation.InductiveTypes` 値を構成子から生成する帰納型を導入し、値を作る規則、場合分けで使う規則、再帰計算、複数の情報を 束ねる構造体を一つの原理から理解します。 #### 第4章　非型付きラムダ計算——束縛・代入・簡約 `FormalLab.Foundation.UntypedLambdaCalculus` 変数束縛、自由変数、捕獲回避代入、α同値、β簡約を定義します。Leanを対象言語の実装に使うことで、 Lean自身の関数と形式化されたラムダ項を区別します。 #### 第5章　宇宙階層と宇宙多相 `FormalLab.Foundation.Universes` 型自身の型を問うときに必要となる宇宙階層を扱います。宇宙レベルと宇宙多相が、一般的な定義を 安全に再利用する仕組みを明らかにします。 ### 第II部　命題と証明 #### 第6章　命題・証明・含意 `FormalLab.Logic.Propositions` 命題を証明が属する型として読み、仮定、結論、含意、証明項を導入します。真理値を計算することと、 証拠を構成することの違いを具体例から確かめます。 #### 第7章　命題論理と構成的・古典的推論 `FormalLab.Logic.Connectives` 連言、選言、否定、同値の証明が要求する情報を調べます。構成的に得られる結論と、排中律などの 古典原理を追加して得られる結論を分けます。 #### 第8章　述語・全称量化・存在量化 `FormalLab.Logic.Quantifiers` 対象によって変わる命題を述語として定義し、全称命題と存在命題の証明を依存関数・証人と証拠の組として 読みます。 #### 第9章　等式・代入・外延性・一意存在 `FormalLab.Logic.Equality` 等式の反射性、対称性、推移性と、等しいものを性質の中で置換する原理を学びます。定義的等しさ、 命題的等式、関数外延性、一意存在を区別します。 #### 第10章　自然演繹・シーケント計算・証明の正規化 `FormalLab.Logic.ProofSystems` 含意断片の自然演繹とシーケント計算を導出型として構成します。導入直後の除去を一段簡約し、 正規化とcut除去が要求する全体的な主張を、一段の変換から区別します。 ### 第III部　型付き計算の理論 #### 第11章　単純型付きラムダ計算——型判断を規則として読む `FormalLab.TypeTheory.SimplyTypedLambdaCalculus` 非型付きラムダ項へ型判断を与えます。文脈と導出木を定義し、型の付く項と付かない項、保存・進行・ 正規化という型システムの基本問題を見通します。 #### 第12章　弱化・交換・縮約・代入 `FormalLab.TypeTheory.StructuralRules` 型を添字に持つ変数と項を構成し、弱化・交換・縮約を型保存名前変更として実装します。捕獲を避ける 代入を変数から同じ型の項への写像として定め、保存定理が必要とする構造補題を準備します。 #### 第13章　操作的意味論・一段簡約・評価戦略 `FormalLab.TypeTheory.OperationalSemantics` 値呼びの一段簡約を推論関係と実行関数の二形で定義します。値、正規形、有限到達、発散を区別し、 名前呼びとの対照から評価戦略が選ぶredexの位置を明らかにします。 #### 第14章　再帰型・fold/unfold・型の無限展開 `FormalLab.TypeTheory.RecursiveTypes` 型変数を束縛する `μ` と捕獲回避置換を定義し、iso-recursive型の明示的なroll/unroll簡約が型を 保存することを証明します。equi-recursive型の型同値判断と構文上の等しさも区別します。 #### 第15章　保存・進行・型安全性 `FormalLab.TypeTheory.TypeSafety` 型保存を内在的な一段関係へ組み込み、標準形補題と進行定理を証明します。保存と進行から、閉じた 型付き項が行き詰まらないことを導き、停止や外部仕様とは異なる保証であることを確かめます。 #### 第16章　正規形・弱正規化・強正規化 `FormalLab.TypeTheory.Normalization` 正規形へ至る経路の存在と、全ての簡約列が有限であることを別々に定義します。自己ループの反例と `Acc` による強正規化を比較し、STLCの完全な正規化証明に必要な論理関係の構造を見通します。 #### 第17章　System Fとインプレディカティブ多相 `FormalLab.TypeTheory.SystemF` 型抽象・型適用・全称型を構文と型判断へ加え、多相恒等関数を一度構成して複数の型へ特殊化します。 インプレディカティブな型量化とLeanの宇宙多相を、量化対象と階層の違いから区別します。 #### 第18章　論理関係と基本補題 `FormalLab.TypeTheory.LogicalRelations` 左右に異なる型を持つ関係と、関数型に沿う関係保存を定義します。恒等・合成の保存証明から、 System Fの型判断全体に対する基本補題の構造を組み立てます。 #### 第19章　パラメトリシティとfree theorem `FormalLab.TypeTheory.Parametricity` 任意関係の保存から関数との可換性を導き、`∀X. X → X` 型の多相自己写像が恒等的であることを 一点関係によって証明します。効果やad-hoc多相が結論を変える境界も扱います。 ### 第IV部　数学の基本言語 #### 第20章　集合を述語として読む `FormalLab.Mathematics.Sets` 所属、包含、和、共通部分、補集合を論理式へ翻訳します。要素ごとの同値から集合の等式へ進む外延性を Leanの表現と数学的原理に分けて理解します。 #### 第21章　数学的関数とその性質 `FormalLab.Mathematics.FunctionProperties` 単射、全射、全単射、左逆、右逆、像、逆像を定義します。関数の式だけでなく始域と終域が性質を 決めることを学びます。 #### 第22章　関係・同値・順序 `FormalLab.Mathematics.Relations` 二項関係の反射性、対称性、反対称性、推移性を比較します。同値関係が等式そのものではなく、後の商を 構成するための同一視の規則であることを明確にします。 #### 第23章　自然数の再帰・場合分け・帰納法 `FormalLab.Mathematics.NaturalNumberInduction` 自然数の構成規則から、再帰による計算と帰納法による証明を導きます。定義展開で成立する等式と、 帰納仮定を必要とする定理を比較します。 #### 第24章　順序・上限・下限・極大原理 `FormalLab.Mathematics.Orders` 上界・下界、上限・下限、最大元・極大元を量化の違いから区別します。述語集合の包含順序を 具体例として任意和と任意共通部分の普遍的な性質を証明し、Zornの補題の仮定を分解します。 #### 第25章　有限性・可算性・基数・無限 `FormalLab.Mathematics.Cardinality` 型の大きさを単射と全単射で比較し、自然数と偶数の全単射を構成します。真偽値列に対する Cantorの対角線論法を証明し、基数とLeanの宇宙レベルを別の分類として扱います。 ### 第V部　再帰・不動点・無限 #### 第26章　整礎関係・整礎帰納法・停止する一般再帰 `FormalLab.Recursion.WellFounded` 接近可能性から整礎帰納法を導き、自然数値の測度で一般の状態上の再帰を正当化します。互除法では 第二引数の減少を証明し、停止性と返り値の数学的仕様を分けます。 #### 第27章　束・完備格子・単調作用素 `FormalLab.Recursion.Lattices` 述語集合の二項上限・下限から任意上限・下限へ進み、空族を含む完備性を証明します。単調作用素と 前不動点・後不動点を定義し、反単調な補集合を反例にします。 #### 第28章　最小・最大不動点とKnaster–Tarski定理 `FormalLab.Recursion.FixedPoints` 全前不動点の下限と全後不動点の上限を構成し、単調性から両者が不動点になることを証明します。 自然数生成作用素から、最小不動点の最小性が帰納法を与える仕組みを読み取ります。 #### 第29章　最大不動点・余帰納的述語・双模倣 `FormalLab.Recursion.CoinductivePredicates` 常時安全性を最大不動点として定義し、後不動点を使う余帰納原理を証明します。決定的遷移系の 双模倣作用素から、同じ観察を保ち続ける状態関係を構成します。 #### 第30章　領域理論・連続写像・再帰方程式 `FormalLab.Recursion.DomainTheory` 最下元を持つω-CPOとScott連続写像を定義します。最下元からの有限反復の上限が最小不動点になることを 証明し、平坦領域と有限燃料計算から部分性を情報の近似として読みます。 ### 第VI部　依存型と型システム #### 第31章　型族・依存関数型・依存対型 `FormalLab.TypeTheory.DependentTypes` 値によって型が変わる型族を導入します。Π型とΣ型から通常の関数・直積を特殊例として復元し、 論理的存在と計算データの違いを調べます。 #### 第32章　同一性型・輸送・外延性原理 `FormalLab.TypeTheory.IdentityTypes` 経路帰納法から輸送、通常の関数による等式の像、依存関数による輸送付きの像を導きます。判断的等しさ、 命題的等式、関数外延性、等式反映、一価性を別々の原理として整理します。 #### 第33章　純粋型システム・ラムダ・キューブ・構成計算 `FormalLab.TypeTheory.PureTypeSystems` 依存の許し方によって型体系を分類する純粋型システムとラムダ・キューブを学びます。構成計算とLeanを 歴史的系譜の中に置きながら、同一の体系とはみなしません。 #### 第34章　部分型と篩型 `FormalLab.TypeTheory.SubtypesAndRefinements` 値と、その値が条件を満たす証明を一つの項として扱います。Leanの部分型を具体例に、篩型という研究上の 広い概念との共通点と差異を確かめます。 #### 第35章　添字付き帰納族 `FormalLab.TypeTheory.IndexedFamilies` 構成子の結果型に添字を持たせ、長さなどの不変条件を型で保存します。パラメータと添字、依存パターン マッチ、部分型による表現との差を学びます。 #### 第36章　一般帰納族・除去規則・厳密正値性 `FormalLab.TypeTheory.GeneralInductiveFamilies` 自由変数の個数で索引づけた構文を評価・名前変更し、一般の依存除去原理を復元します。再帰変数の 極性を判定するコードから、関数入力側の負の出現を禁じる厳密正値性を理解します。 #### 第37章　W型・整礎木・多項式的帰納型 `FormalLab.TypeTheory.WTypes` 節点の形と子の位置族から整礎木を作り、foldで消費します。自然数とリストをW型として符号化し、 多項式の一層とのroll/unroll逆法則を証明して始代数への準備を整えます。 #### 第38章　高次同一性・一価性・ホモトピー型理論 `FormalLab.TypeTheory.HomotopyTypeTheory` 経路、ホモトピー、可縮なファイバー、型同値、一価性を順に定義します。真偽反転の自己同値を用いて、 Leanの証明無関連な `Eq` がHoTTの高次同一性をそのまま保持しないことを形式的に示します。 #### 第39章　商型とwell-definedness `FormalLab.TypeTheory.Quotients` 同値関係にある値を新しい型で同一視します。商から関数を定義するには代表元の選び方に依存しないことを 証明しなければならない理由を扱います。 #### 第40章　法則を持つ構造と型クラス探索 `FormalLab.TypeTheory.TypeClasses` データと法則を構造体に束ね、型クラスによって必要な構造を暗黙に渡す仕組みを学びます。数学的構造と Leanのインスタンス探索を区別します。 #### 第41章　型推論・単一化・双方向型付け `FormalLab.TypeTheory.TypeInference` 構文から型等式制約を生成し、occurs check付き単一化で未知型を解きます。型を出力する合成判断と 既知の型を入力する検査判断を分け、Leanのelaboratorとkernelの役割の差へ接続します。 ### 第VII部　圏論と普遍性 #### 第42章　始対象と終対象——零項の普遍性 `FormalLab.CategoryTheory.InitialAndTerminal` あらゆる対象への射、またはあらゆる対象からの射が一意であるという零項の普遍性を扱います。普遍対象が 一意な同型を除いて一意になる証明を学びます。 #### 第43章　積の普遍性 `FormalLab.CategoryTheory.Products` 直積を単なる対の構成ではなく、二本の射を一意に束ねる対象として特徴づけます。存在一意性による定義と、 写像集合の間の一対一対応を比較します。 #### 第44章　余積と双対性 `FormalLab.CategoryTheory.Coproducts` 余積を二本の射を一意に場合分けする対象として特徴づけます。積の定義で射を反転することから余積を導き、 双対性を逆関数と混同しないための最初の例を得ます。 #### 第45章　圏・射・反対圏・宇宙 `FormalLab.CategoryTheory.Categories` 対象、射、恒等射、合成と三つの法則から圏を定義します。自然数加法を一対象圏として実装し、一般の射を 関数と同一視できないこと、反対圏が逆射を追加しないこと、対象と射の宇宙が独立であることを学びます。 #### 第46章　関手——圏の構造を保つ写像 `FormalLab.CategoryTheory.Functors` 対象写像と射写像が恒等射と合成を保つことを定式化します。一対象圏の倍化関手、恒等関手、関手合成を 計算し、反変関手を反対圏からの通常の関手として理解します。 #### 第47章　自然変換と関手圏 `FormalLab.CategoryTheory.NaturalTransformations` 関手を各対象の成分射で比較し、全射に対する自然性を可換正方形として課します。恒等自然変換と垂直合成から、 関手を対象、自然変換を射とする関手圏を構成します。 #### 第48章　同型・自然同型・圏同値 `FormalLab.CategoryTheory.Equivalences` 対象の同型、関手の自然同型、圏同値を段階的に区別します。圏同値を往復関手と自然同型で定義し、 完全・忠実・本質的全射による判定条件と、等号より同型を使う理由を学びます。 #### 第49章　図式・錐・極限・余極限 `FormalLab.CategoryTheory.Limits` 対象と射の配置を図式として表し、錐の自然な脚と一意な媒介射から極限を定義します。終対象・積・等化子・ 引戻しを同じ形式に統一し、射を反転した余錐・余極限との双対性を導きます。 #### 第50章　hom関手・普遍元・表現可能関手 `FormalLab.CategoryTheory.RepresentableFunctors` 固定対象への全射を集めるhom関手を構成し、集合値反変関手がhom関手と自然同型になる条件を定義します。 表現の自然な全単射を普遍元と一意な分類射へ圧縮し、普遍構成との共通形式を明らかにします。 #### 第51章　米田の補題と米田埋め込み `FormalLab.CategoryTheory.YonedaLemma` hom関手から任意の反変関手への自然変換が、恒等射での一つの値から完全に復元されることを証明します。 hom関手間の自然変換から元の射を回収し、米田関手の完全忠実性を導きます。 #### 第52章　随伴——homの自然同型・単位・余単位 `FormalLab.CategoryTheory.Adjunctions` 随伴を二変数に自然なhom全単射として理解し、単位・余単位、転置公式、三角恒等式を相互に導きます。 右随伴を表現対象の関手的な選択として読み、圏同値との違いを明確にします。 #### 第53章　モナド・余モナド・Kleisli圏・Eilenberg–Moore圏 `FormalLab.CategoryTheory.Monads` 自己関手上の単位・乗法と三法則からモナドを定義し、Option型で成分計算を検査します。効果を持つ射を 合成するKleisli圏と、構造を解釈するEilenberg–Moore圏を比較し、余モナドとの双対性を扱います。 #### 第54章　自己関手の代数と代数準同型 `FormalLab.CategoryTheory.EndofunctorAlgebras` 一層分の構造を値へ畳み込む射 `F(A)→A` を自己関手代数として定義します。Option代数の具体例から、 構造を保つ代数準同型の可換正方形と代数圏を構成し、モナド代数との差を明確にします。 #### 第55章　始代数・fold・Lambekの補題 `FormalLab.CategoryTheory.InitialAlgebras` 自然数を `F(X)=1+X` の始代数として構成します。任意の代数へのfoldを定義し、準同型性と帰納法による 一意性を証明した後、始代数の構造射が同型になるLambekの補題を確認します。 #### 第56章　自己関手の余代数と余代数準同型 `FormalLab.CategoryTheory.EndofunctorCoalgebras` 状態を一段の観察へ展開する射 `S→F(S)` を余代数として定義します。停止し得るcountdown遷移を構成し、 観察を保つ準同型、余代数圏、代数との双対性、双模倣への入口を扱います。 #### 第57章　終余代数・anamorphism・振舞意味論 `FormalLab.CategoryTheory.FinalCoalgebras` ストリームを `F(X)=A×X` の終余代数として構成し、任意の状態機械から振舞いを生成するanamorphismと その一意性を証明します。双対Lambek補題と、終意味論による状態の同一視を学びます。 #### 第58章　前層――局所データを制限する反変関手 `FormalLab.CategoryTheory.Presheaves` 前層を反対圏からの関手として定義し、射と逆向きに進む制限写像の恒等・合成法則を検査します。 前層間の自然変換、定値前層、表現可能前層を比較し、貼り合わせをまだ要求しないことを明確にします。 #### 第59章　篩・Grothendieck位相・サイト `FormalLab.CategoryTheory.Sites` 終点を固定した射の述語から、前合成で閉じた篩を構成します。主篩、篩の引戻し、被覆篩の三公理を経て Grothendieck位相を定義し、圏と位相の組としてサイトを理解します。 #### 第60章　層条件・貼り合わせ・層化 `FormalLab.CategoryTheory.Sheaves` 被覆篩上の要素族、整合性、貼り合わせを定義し、分離性と層条件を存在・一意性へ分解します。層の圏を 前層圏の充満部分圏として構成し、層化を包含関手の左随伴として特徴づけます。 #### 第61章　比較関手・モナド性・Beckの定理 `FormalLab.CategoryTheory.Monadicity` 随伴からEilenberg–Moore圏への比較関手を構成し、右随伴がモナド的である条件を圏同値として定義します。 比較関手の三つの障害を分析し、Beck型定理が分裂対の余等化子へ還元する仕組みを学びます。 #### 第62章　end・coend・双自然性 `FormalLab.CategoryTheory.EndsAndCoends` 双関手の対角成分へ入る整合した射族をwedge、対角成分から出る射族をcowedgeとして定義し、その普遍対象として endとcoendを構成します。`Type` 値の場合にendが整合族の部分型、coendが生成関係による商型になることを確認し、 自然変換をhom双関手のendとして読み直します。 #### 第63章　Kan拡張——関手の普遍的な延長 `FormalLab.CategoryTheory.KanExtensions` 関手の定義域を別の圏へ広げる候補を自然変換で比較し、始対象として左Kan拡張、終対象として右Kan拡張を 定義します。前合成関手との左右の随伴、コンマ圏上の余極限・極限による各点公式、end・coendを使う計算法を 区別して理解します。 #### 第64章　モノイダル圏——テンソル積と整合性 `FormalLab.CategoryTheory.MonoidalCategories` 対象と射のテンソル積、単位対象、結合子、左右の単位子を導入し、五角形公理と三角形公理が括弧変更と単位除去を 整合させる仕組みを学びます。`Type` の直積を具体例として計算しつつ、一般のモノイダル積には複製や破棄の構造が 含まれないこと、整合性定理が構造射だけに適用されることを区別します。 #### 第65章　豊穣圏——hom集合を構造ある対象へ置き換える `FormalLab.CategoryTheory.EnrichedCategories` hom集合をモノイダル圏のhom対象へ置き換え、恒等射をテンソル単位からの一般化要素、合成をhom対象間の射として 再構成します。豊穣関手と豊穣自然変換、`Type`-豊穣圏と通常圏の対応、自然変換の型とそれを表現する豊穣hom対象の 存在条件を区別します。前順序とLawvere距離も同じ公理の異なる値圏として読みます。 ### 第VIII部　型・計算・圏を結ぶ #### 第66章　帰納型・帰納法・始代数——三つの生成原理を接続する `FormalLab.Bridges.InductionAndInitialAlgebras` 自然数の零と後者を、帰納型の構成子、固定した終域への再帰、入力に依存する帰納法、`F(X)=1+X` の始代数という 四つの観点から比較します。型族の全空間 `Σn,P(n)` へのfoldから依存帰納を回収し、従属和と等式輸送という 追加構造が必要になる理由、不動点同型だけでは始性も帰納法も得られない理由を明確にします。 #### 第67章　W型・多項式関手・自由代数——形と位置から帰納構造を作る `FormalLab.Bridges.PolynomialFunctorsAndWTypes` 形 `a:A` と位置族 `B(a)` から `P(X)=Σa.B(a)→X` を多項式関手として構成し、W型がその始代数になることを foldの存在とW帰納法による一意性から証明します。変数を葉として加えた木について、生成元写像の一意延長としての 自由代数性と、`Q_X(Y)=X+P(Y)` の始代数性を照合し、不動点・始代数・自由代数を区別します。 #### 第68章　余帰納法・双模倣・最大不動点・終余代数——関係と振舞いを接続する `FormalLab.Bridges.CoinductionAndFinalCoalgebras` 決定的ストリーム系について、状態対上の最大不動点としての双模倣と、終余代数への一意な準同型が与える振舞意味論を 接続します。終振舞いの等しい状態対が後不動点になることと、双模倣から全有限位置の観察一致が従うことを証明し、 最大不動点・不動点同型・終性・振舞等価がそれぞれ異なる主張であることを整理します。 #### 第69章　無限の三つの意味——基数・尽きない観察・無限図式 `FormalLab.Bridges.ThreeNotionsOfInfinity` 型の要素数としての無限、任意の有限時刻まで続けられる観察、無限個の対象を持つ図式を、量化対象の違いから 比較します。有限状態で尽きない交代列を作る機械、無限状態なのに一つの振舞いしか持たない機械、可算図式なのに 一点しか持たない極限を構成し、有限prefixの逆系とストリームの対応へ進みます。 #### 第70章　デカルト閉圏——積・指数対象・カリー化 `FormalLab.Bridges.CartesianClosedCategories` 有限積に加えて、`Hom(A×X,B)≃Hom(X,B^A)` を自然に実現する指数対象を導入します。型の圏で評価射、カリー化、 β・η則を計算し、一般圏では `A×- ⊣ A⇒-` という随伴と表現可能性へ移します。デカルト閉性と一般の モノイダル閉性を区別し、複製・破棄が積構造に由来することも確認します。 #### 第71章　単純型付きラムダ計算の圏論的意味論——判断を射へ移す `FormalLab.Bridges.STLCCategoricalSemantics` STLCの型を対象、文脈を有限積、型判断を文脈対象から型対象への射として解釈します。`Type` の標準モデルでは 変数を射影、適用を関数適用、抽象をカリー化として計算し、名前変更と弱化の意味保存を証明します。一般の デカルト閉圏では適用を評価射、抽象を内部homへのカリー化へ移し、β・η則、代入と合成、健全性と完全性を それぞれ区別します。 #### 第72章　スライス圏・添字圏・ファイブレーション——変化する文脈の上で対象を運ぶ `FormalLab.Bridges.SlicesIndexedCategoriesAndFibrations` `Type` の引戻しを部分型として構成し、その普遍性から型族の再添字付けを読み取ります。一般圏ではスライス圏、 選ばれた引戻し関手、ファイバー圏、Cartesian持ち上げを順に導入し、反変添字圏とファイブレーションが Grothendieck構成を介して対応する理由を明らかにします。依存型の代入を再添字付けとして読むための基盤です。 #### 第73章　局所デカルト閉圏——依存積を再添字付けの右随伴として捉える `FormalLab.Bridges.LocallyCartesianClosedCategories` 型族について依存和、再添字付け、依存積の三随伴 `Σ_f⊣f⁎⊣Π_f` を明示的なhom同値として証明します。 一般圏では指数化可能射、選ばれた引戻し、依存カリー化へ移り、各スライスがデカルト閉であるという定義と 全ての射に沿う依存積の存在を結びます。通常のデカルト閉性と局所デカルト閉性も区別します。 #### 第74章　依存型理論の圏論的意味論——文脈・型・項・代入を再構成する `FormalLab.Bridges.DependentTypeCategoricalSemantics` `Type` の標準モデルで文脈、型族、依存項、代入、文脈拡張を実装し、置換則とΠ・Σのβη則を証明します。 一般圏では型を表示射、項を切断、型の代入を引戻し、依存和を表示射の合成、依存積を右随伴として解釈します。 外延的同一性型と、高次経路を保持する内包的同一性型に必要な追加構造も区別します。 #### 第75章　モノイダル閉圏——内部hom・評価・自己豊穣化 `FormalLab.Bridges.MonoidalClosedCategories` 各対象 `A` に対する随伴 `A⊗-⊣[A,-]` から、評価・余評価、カリー化のβη則、 `Hom(A,B)≃Hom(I,[A,B])`、内部カリー化を構成します。内部恒等射と内部合成が圏の自己豊穣化を与えることを Leanで検査し、左右の閉性、組紐による移送、デカルト閉圏に固有の複製・破棄を区別して線形型へ接続します。 #### 第76章　線形論理・線形型——仮定を資源として追跡する `FormalLab.Bridges.LinearLogicAndResourceSemantics` 弱化・縮約を無条件に許さない小さな線形シーケント計算を定義し、テンソル右規則の文脈分割、cut、線形含意を Leanで構成します。対称モノイダル閉圏による乗法的意味論、加法的結合子、*-自律圏による双対、指数様相 `!` に 必要な余モナドと可換余モノイド、デカルト閉な非線形世界とのLNL随伴を段階的に区別します。 #### 第77章　モナドと計算効果——値から計算を分離して合成する `FormalLab.Bridges.MonadsAndComputationalEffects` 例外・状態・非決定性について `pure`・`bind` と三法則を計算し、効果付き関数をKleisli射として合成します。 値呼び意味論に必要な強さと評価順序、自由な選択木、代数的演算、ハンドラをEilenberg–Moore代数と比較し、 操作的意味論との健全性・完全性・適切性を区別します。 #### 第78章　トポスと圏論的論理——部分対象を真理値で分類する `FormalLab.Bridges.ToposesAndCategoricalLogic` `Type` の述語から部分対象分類子の引戻し普遍性へ進み、部分対象関手の表現可能性を証明します。前層では篩、 層では閉篩が内部真理値になることをLeanの現行APIで検査し、冪対象、Heyting論理、量化随伴、 Kripke–Joyal意味論、幾何学的射へ展開します。初等トポスとGrothendieckトポスも明確に区別します。 #### 第79章　再帰型の意味論——構文・近似・関手不動点を接続する `FormalLab.Bridges.RecursiveTypeSemantics` 再帰型構文、Scott連続作用素の値の不動点、関手の不動点対象、始代数・終余代数を区別してから接続します。 `F(X)=1+X` の有限段階、roll/unroll、負の再帰出現、代数的完備性と代数的コンパクト性をLeanで検査します。 最後に表示の存在、健全性、適切性、完全抽象性が別々の定理であることを明確にします。 ## 目的別の読書案内 ### 篩型を理解したい 第1・2・3章で型、関数、帰納型を確認し、第6・8・9章で命題、述語、等式を学びます。続いて第5章の 宇宙と第31章の依存型を経て、第34章へ進みます。単純型付きラムダ計算から型体系全体の見取り図も得たい 場合は、第4・11・33章を併読してください。 ### ラムダ計算から構成計算まで進みたい 第1〜4章で項、束縛、代入、簡約を学び、第11章で型判断を導入します。第5章と第31章で宇宙と依存型を 理解した後、第33章でラムダ・キューブと構成計算を体系的に位置づけます。 ### 数学の証明をLeanで学びたい 第1〜3章の後、第6〜9章で命題論理と量化・等式を学び、第20〜23章へ進みます。この経路では集合、 関数、関係、帰納法を、通常の数学的証明とLeanの証明項を往復しながら学べます。 ### 普遍性と双対性から圏論へ入りたい 第1〜3章、第5章、第9章を確認してから、第42〜44章で始対象・終対象、積、余積の普遍性を具体的に 学びます。続く第45〜65章で一般の圏、関手、自然変換、圏同値、極限、表現可能性、米田、随伴、モナド、 始代数・終余代数、前層・層へ進みます。普遍性を既に知っていれば第45章から始められます。 ### 前層・サイト・層を理解したい 第45・46章で圏、反対圏、関手を学んだ後、第58章の前層へ進みます。第59章の篩とサイトは第45章から 独立に読めます。この二経路を第60章で合流させ、整合族、貼り合わせ、層化を学びます。米田による層条件も 理解したい場合は、第47章の自然変換と第50・51章の表現可能性・米田の補題を併読してください。 ### end・coendとKan拡張を理解したい 第45〜49章で圏、関手、自然変換、圏同値、極限・余極限を学んでから、第62章へ進みます。Kan拡張は 第52章の随伴と第49章の極限・余極限を直前提として第63章で学べます。end・coendはKan拡張の定義上の 前提ではありませんが、各点公式を別の形で計算する方法を理解するには第62章を先に読むと有効です。 ### テンソル積とモノイダル圏を理解したい 第45〜47章で圏、関手、自然変換を学んでから、第64章へ進みます。集合の直積による例を普遍性からも理解したい 場合は第43章と第49章を併読してください。第64章ではデカルト積に固有の射影・複製と、一般のテンソル積が持つ 結合・単位の構造を分離します。 ### 豊穣圏を理解したい 第45〜47章で通常の圏・関手・自然変換を確認し、第64章でモノイダル圏のテンソル積、単位子、結合子を学んでから 第65章へ進みます。第65章そのものは通常圏を定義上の前提としませんが、通常の圏論との比較を理解するために 第45〜47章を推奨します。豊穣自然変換のhom対象をendとして読むには第49章と第62章も併読してください。 ### モノイダル閉圏と内部homを理解したい 第52章で随伴、第64章でテンソル積と整合性を学んでから第75章へ進みます。内部homを関数型の一般化として先に 計算したい場合は、第2・43・70章で関数、積、指数対象を確認して第75章前半を読み、その後に第45〜52・64章を 補えます。内部homが豊穣hom対象になる構成まで追う場合は第65章も併読してください。 ### 線形論理と線形型を理解したい 第10章で自然演繹・シーケント計算・構造規則を確認し、第11章で型判断を学びます。圏論的意味論まで追う場合は 第52・64・75章で随伴、モノイダル圏、内部homを確認して第76章へ進みます。第76章前半の導出と変数使用回数は 第10・11章から直接読めるので、その後に圏論側を補って資源意味論へ戻る経路も取れます。 ### モナドと計算効果を理解したい 第13章で値呼びの操作的意味論、第46・47・53章で関手・自然変換・モナドを学んでから第77章へ進みます。 例外と状態の具体計算を先に理解したい場合は、第2・13章から第77章前半へ直接進み、その後に第45〜53章を補って Kleisli圏、強いモナド、Eilenberg–Moore代数、代数的ハンドラを読み直せます。 ### トポスと圏論的論理を理解したい 第45〜52章で圏、関手、自然変換、極限、表現可能性、米田、随伴を学び、第58〜60章で前層、篩、層を確認します。 第70章のデカルト閉圏を経て第78章へ進むと、部分対象分類子、冪対象、内部論理、量化随伴を一つの流れで読めます。 述語から先に具体像を得たい場合は、第6〜9・20章から第78章前半へ進み、その後に圏論側を補えます。 ### 再帰型の意味論を理解したい 第14章でiso-recursive型とequi-recursive型、第27〜30章で完備格子、不動点、領域理論を学びます。圏論側は 第46・54〜57章で関手、代数・余代数、始代数・終余代数を確認して第79章へ進みます。構文から先に読みたい場合は、 第13・14・30章から第79章前半へ進み、その後に圏論側を補って代数的コンパクト性まで読み直せます。 ### 帰納型・帰納法・始代数の関係を理解したい 第3章で構成子と再帰、第23章で自然数帰納法、第31章で従属和、第36章で一般の帰納族と厳密正値性を学びます。 第46章の関手、第54章の自己関手代数、第55章の始代数を経て第66章へ進むと、非依存foldと依存帰納の差、および 両者を全空間によって接続する際に必要な構造を一つずつ確認できます。第37章のW型を一般の多項式関手の始代数へ 進め、生成元上の自由代数まで理解するには、続けて第67章を読みます。 ### W型・多項式関手・自由代数を理解したい 第31・36章で依存型と一般帰納族を確認し、第37章で形と位置からW型を構成します。第46・54・55章で関手、 自己関手代数、始代数を学んだ後、第66章でfoldと帰納法の論理的な差を整理してから第67章へ進みます。 自然数とリストの一層を多項式表示へ戻す具体例から始めるなら、第37章から第67章へ直接進むこともできます。 ### 余帰納法・双模倣・終余代数を理解したい 第27・28章で完備格子と不動点を学び、第29章で最大不動点による余帰納的述語と双模倣へ進みます。圏論側は 第46章の関手、第56章の自己関手余代数、第57章の終余代数を読みます。第68章では二経路を合流させ、決定的 ストリーム系について最大双模倣と終余代数への像の等しさが一致する条件と証明を確認します。 ### 無限という語の異なる意味を整理したい 第25章で基数・可算性・対角線論法、第29章で最大不動点と余帰納、第49章で図式・極限、第57章で終余代数を 学びます。第68章で双模倣と終振舞いを接続してから第69章へ進むと、要素数、任意有限時刻の観察、無限図式という 三つの量化を具体的な反例で分離し、有限prefixの逆極限としてストリームを読むことができます。 ### デカルト閉圏と指数対象を理解したい 第43章で積の普遍性、第49章で極限、第50章で表現可能性、第52章で随伴を学んでから第70章へ進みます。 カリー化を型と関数の具体例から先に理解したい場合は、第2・11章を確認して第70章前半を読み、その後に 第45・46・47・52章を補って一般圏のhom同値と随伴へ戻る経路も取れます。 ### 単純型付きラムダ計算の圏論的意味論を理解したい 第11章で型判断、第12章で名前変更・弱化・代入を学び、第43章で積、第50章で表現可能性、第52章で随伴を 確認してから、第70・71章へ進みます。第71章前半の `Type` モデルは第11・12章から直接読めます。そこで 変数・適用・抽象の計算像を得てから第45〜52章と第70章を補い、一般のデカルト閉圏で同じ対応を読み直せます。 ### スライス圏・添字圏・ファイブレーションを理解したい 第31章で型族と依存対、第45〜49章で圏・関手・自然変換・圏同値・引戻しを学んでから第72章へ進みます。 型族の再添字付けを具体例から先に得たい場合は、第31章から第72章前半の `Type` における引戻しへ直接進み、 その後に第45〜49章を補ってスライス圏とCartesian持ち上げを読み直すこともできます。 ### 局所デカルト閉圏と依存積を理解したい 第31章で依存関数型・依存対型、第43・49・52章で積・引戻し・随伴を学び、第70章でデカルト閉圏を確認します。 続いて第72章でスライス圏と再添字付けを理解してから第73章へ進みます。型族の計算を先に見たい場合は、第31章から 第73章前半の `Σ_f⊣f⁎⊣Π_f` へ直接進み、その後に一般圏の指数化可能射へ戻れます。 ### 依存型理論の圏論的意味論を理解したい 第31・32章で型族、Π・Σ、同一性型と輸送を学び、第72章で表示射・引戻し・ファイブレーション、第73章で 三随伴と局所デカルト閉圏を確認してから第74章へ進みます。`Type` の標準モデルから入りたい場合は、第31・32章から 第74章前半へ直接進み、その後に第72・73章を補って表示射と切断による一般圏の解釈へ戻れます。 ## 付録 * `FormalLab.Appendix.Notation` — 数学的記法・判断・推論規則とLean表現の対照 * `FormalLab.Appendix.Terminology` — 日英用語集と訳語の方針 * `FormalLab.Appendix.HistoricalSources` — 研究史と注釈付き一次文献・研究書 * `FormalLab.Appendix.ExerciseSolutions` — 全問題のヒントと解説付き解答 ## 読み方 定義では右辺を隠して型だけを読み、どの入力から何を作るかを日本語に戻します。 定理では仮定と結論を分け、自分の証明を考えてから本体を読みます。`#check` は型の観察、 `#eval` は計算の観察です。読後問題に答えられない場合は、直前提だけを戻って確認します。 このルートは教材だけをimportします。mathlibの動作確認用 `FormalLab.Environment` は、 教材の概念グラフへ不要な依存を入れないため意図的に含めていません。 -/