Formal Lab

第1・2・3章で型、関数、帰納型を確認し、第6・8・9章で命題、述語、等式を学びます。続いて第5章の 宇宙と第31章の依存型を経て、第34章へ進みます。単純型付きラムダ計算から型体系全体の見取り図も得たい 場合は、第4・11・33章を併読してください。

第1〜4章で項、束縛、代入、簡約を学び、第11章で型判断を導入します。第5章と第31章で宇宙と依存型を 理解した後、第33章でラムダ・キューブと構成計算を体系的に位置づけます。

第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章の表現可能性・米田の補題を併読してください。

第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章も併読してください。

第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章を読みます。

第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章を補って表示射と切断による一般圏の解釈へ戻れます。