Bedrock

Laying the groundwork for the metaphysics of 𝑉

A trilingual textbook of machine-checked set theory in Cubical Agda. Proving ZFC and GCH in the constructible universe L, assuming excluded middle.

• English: A trilingual textbook of machine-checked set theory in Cubical Agda. Proving ZFC and GCH in the constructible universe L, assuming excluded middle.
• 中文: 以 Cubical Agda 形式化构建集合论的三语交互式教科书。在排中律假设下，证明可构造宇宙 L 满足 ZFC 与 GCH。
• 日本語: Cubical Agda で集合論を形式化する三言語の対話型教科書。排中律の仮定のもとで、構成可能宇宙 L が ZFC と GCH を満たすことを証明する。

Reading this as a program? /llms.txt is the guide written for you: it lists every chapter, every machine-readable endpoint, and the plain-Markdown twin each chapter page carries.