Bedrock

A machine-checked development of set theory in Cubical Agda. The constructible universe L is proved to model ZFC and to satisfy GCH.

• English: A machine-checked development of set theory in Cubical Agda. The constructible universe L is proved to model ZFC and to satisfy GCH.
• 中文: 用 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.