読書案内

学習ルートを選び、前提関係を確認し、マイルストーンと用語を振り返ります。

主題を選び、ルートを比較し、修了した前提から進めます。

読書案内 · 依存マップ

依存マップ

120 章の依存関係を上から下へ表示。A → B は B が A を import することを表します。どの配置も同じ前提関係の半順序を示し、依存経路のない主題は交互に学べます。

辺：
色の凡例

章を選択して前提を確認

図は縦横にスクロールできます。全体表示に切り替えると概観できます。

広く使われる Base.Prelude の辺は図から省略し、章の詳細には残します。 骨格は到達関係を保ちます。省略された辺の import が不要とは限りません。学習段階は全章を直列に並べるものではありません。合流する章へ進む前に、表示された前提を終えてください。冒頭の予告 Milestones は、この図では終点として下部に置きます。

マイルストーン

このページでは、本書で証明された到達点をまとめ、そこへ至る読書ルートへの簡潔な入口も示します。各項目はまず通常の数学書の言葉で定理を述べ、その後にそれを証明する Agda の宣言を直接インポートします。

{-# OPTIONS --cubical --safe --guardedness #-}

module Milestones where

定理1 排中律の仮定のもとで、ホストレベルの V は ZF のモデルです。

open import V.Model public using ( V⊨ZF )

定理2 ホストレベルの選択公理の仮定のもとで、ホストレベルの V は ZFC のモデルです。

open import V.Model public using ( V⊨ZFC )

定理3 排中律の仮定のもとで、構成可能宇宙 L は ZFC のモデルです。

open import L.Model public using ( L⊨ZFC )

定理4 同じ排中律の仮定のもとで、構成可能宇宙 L は内部的に一般連続体仮説を満たします。

open import L.GCH.Theorem public using ( L⊨GCH )

用語集

用語は本書で最初に現れる順に並んでいます。用語を選ぶと、最初の導入箇所を振り返れます。

対象理論
メタ理論の中で表現され研究される理論。本書では集合論を指す。
メタ理論
対象理論を表現し研究するための理論。本書では立方型理論を指す。
ホスト
対象理論の形式化を支える Cubical Agda の環境。
宇宙レベル
型宇宙 Type ℓ の大きさを表す添字 ℓ。ホモトピーレベルや構成可能階層の一つの層とは異なる。
Π 型
結果の型が入力に応じて変わりうる依存関数型。
依存関数
Π 型の元。各入力に対し、その入力に対応する型の元を与える。
Σ 型
第二成分の型が第一成分に依存しうる依存対型。
依存対
Σ 型の元。選ばれた第一成分と、対応する型に属するデータの組。
第一成分
依存対で先に選ばれる元であり、fst で取り出す。
第二成分
型が第一成分に依存しうる依存対のもう一方の元であり、snd で取り出す。
証明書
後の議論でその性質を使えるよう、対象とともに携える証明。
フィールド
レコード型の名前付きの成分であり、同名の射影で取り出せる。
構成子
帰納型やレコード型の元を直接作り出す基本の操作。
射影
対から成分を、レコードからフィールドを取り出す操作。
パス
型の二つの元の間の等しさの証明。始点と終点を持ち、逆向きにも、つなぎ合わせることもできる。
ホモトピーレベル
要素とその等しさの証明に区別できる構造がどれだけ残るかによる型の分類。
可縮
選ばれた中心を持ち、すべての元が中心とパスで結ばれる型。
一意存在
存在と一意性を合わせた概念。本書では可縮型で表し、その中心が必要な証人を与える。
命題
任意の二つの元が等しい型であり、証明が存在するかどうかだけを保つ。
h-集合
等しさの型がすべて命題である型。元は互いに異なりうるが、同じ二元が等しいことの証明は互いに一致する。
基礎型
型とともに収められた性質や構造を忘れて得られる型。P : hProp ℓ については第一成分 ⟨ P ⟩ である。
空型
構成子を持たない型。元が存在しないので、任意の型へ消去できる。
命題的切り詰め
型を、要素の有無が同じ命題へ送る操作。要素があることは保ち、それがどれであったかは忘れる。
クラス
与えられた論域上の述語。本書では、その論域から命題の宇宙への関数として表す。
論域
変数が動く型。論域と呼ぶだけでは、関係、演算、その他の構造は加わらない。
台
構造の対象を担い、その関係や演算が定義される基礎の型。
論理的同値
論理的同値は両方向の含意を与え、命題については isProp によってそれらの写像を型同値へ高められる。
型同値
型同値 A ≃ B は、各ファイバーが可縮である写像であり、逆写像と二つの往復パスはこの条件から導かれる。
ファイバー
写像 f : A → B の b : B 上のファイバーは依存対型 Σ (a : A) (f a ≡ b) であり、その要素は原像と、それが b へ写ることを示すパスからなる。
同型
同型は順写像、逆写像、および二つの逆法則を明示的に与える。