# Bedrock

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

Bedrock is a machine-checked development, in Cubical Agda, of the set theory behind
contemporary questions about the universe of sets. Two results are proved and both are
re-exported by the chapter `Origin`: `L⊨ZFC` and `L⊨GCH`, the constructible universe
as a model of ZFC and as a model in which the generalized continuum hypothesis holds.
Besides their universe parameter, each requires only excluded middle at `LEM (ℓ-suc ℓ)`.
The long-term aim is forcing, set-theoretic geology, the definability of ground models
and the mantle.

The project is host-language maximalist: every set-theoretic notion is rebuilt in
type-theory-native idiom rather than transcribed from the textbook ZF axioms, and the
deeply embedded first-order `Formula` is used only where syntax is itself the object of
study. Every file typechecks under Agda 2.8.0 with the cubical 0.9 library and the
`--safe` flag, so nothing here is postulated.

This site is the development published as a trilingual mathematics textbook. One chapter
is one Agda module. The displayed Agda is the formal content; the prose around it is the
exposition, written in English, Chinese and Japanese from a single master. The reading
order is a dependency order: a chapter's prerequisites are the modules it imports.


## How to read this site

The homepage presents the overview chapter and interactive contents. Its initial HTML contains the chapter prose and code; tabs, graphs, search and hover require JavaScript. Use the chapter list below or reading-routes.json for actual addresses, not guessed module filenames.

Each chapter has a Markdown mirror linked from its HTML head and footer. Replace the .html extension with .md (do not append it). The mirror contains chapter prose and original fenced code, including setup hidden behind source popups in HTML; interactive controls are not mirrored. Referenced non-literate library pages may have HTML only.

Cite a named definition anchor when possible. #sec-N and #p-N identify headings and prose blocks in the current edition; numeric code anchors are compiler source offsets. Positional anchors can change after edits. Quote the selected text as well, and verify it at the target. Markdown mirrors do not reproduce HTML token/paragraph anchor IDs.

Read original code before inferring assumptions, universe levels or a theorem’s scope. Hover text and search snippets are navigation aids, not substitutes for the declaration.

## Machine-readable endpoints

These are static files. CORS headers are supplied for hosts that support the generated _headers file.

- [llms.txt](https://bedrock.institute/llms.txt): Start here: chapter addresses, Markdown mirrors and source guidance.
- [en/reading-routes.json](https://bedrock.institute/en/reading-routes.json): Chapter graph with page/anchor addresses, prerequisites and routes.
- [en/terms.json](https://bedrock.institute/en/terms.json): Glossary labels, recaps and introduction links.
- [search-content.json](https://bedrock.institute/search-content.json): Full search across all published languages: chapters, headings, prose, terms and internal/external code. Each entry has kind, lang and href; resolve href inside /<lang>/, using any published edition for lang="*".
- [en/search.json](https://bedrock.institute/en/search.json): Legacy chapter/identifier index, not the complete full-text search.
- [sitemap.xml](https://bedrock.institute/sitemap.xml): Published chapter pages and language alternatives.
- [robots.txt](https://bedrock.institute/robots.txt): Public crawl policy.

Optional semantic sidecars: `/en/types/<Module>.json`. Numeric anchor keys map to HTML-valued types; `$names` maps anchors to names and `$expressions` holds available expression ranges and types. coverage depends on compiler evidence. Missing entries do not imply a type. Do not treat HTML strings as plain source.

## Source

- [https://github.com/BedrockInstitute/Bedrock](https://github.com/BedrockInstitute/Bedrock): the repository. A chapter master is at `src/<Module path>.lagda.md`.
- [https://github.com/BedrockInstitute/Bedrock/blob/main/README.md](https://github.com/BedrockInstitute/Bedrock/blob/main/README.md): the project overview, build instructions and repository structure.
- [https://github.com/BedrockInstitute/Bedrock/blob/main/docs/en/CHARTER.md](https://github.com/BedrockInstitute/Bedrock/blob/main/docs/en/CHARTER.md): the charter, the full methodological statement behind host-language maximalism.

## Chapters, in reading order

Links point at the Markdown mirrors. Published language segments: en, zh, ja. Replace the language segment for another edition, and `.md` with `.html` for the page a human reads. A chapter that is not read at the page its own name gives says where it is read.

- [1. Origin](https://bedrock.institute/en/index.md) (`Origin`, Preview), read at https://bedrock.institute/en/index.html#milestones: The book's proved endpoint results, with routes leading to each theorem.
- [2. Prelude](https://bedrock.institute/en/Base.Prelude.md) (`Base.Prelude`, Foundations)
- [3. Impredicativity](https://bedrock.institute/en/Base.Impredicativity.md) (`Base.Impredicativity`, Foundations)
- [4. The classical boundary](https://bedrock.institute/en/Base.Classical.md) (`Base.Classical`, Foundations)
- [5. Choice](https://bedrock.institute/en/Base.Choice.md) (`Base.Choice`, Foundations)
- [6. The object language](https://bedrock.institute/en/FOL.Syntax.md) (`FOL.Syntax`, First-order logic)
- [7. Structures](https://bedrock.institute/en/FOL.ZFStructure.md) (`FOL.ZFStructure`, First-order logic)
- [8. Semantics](https://bedrock.institute/en/FOL.Semantics.md) (`FOL.Semantics`, First-order logic)
- [9. The Lévy hierarchy](https://bedrock.institute/en/FOL.LevyHierarchy.md) (`FOL.LevyHierarchy`, First-order logic)
- [10. Absoluteness](https://bedrock.institute/en/FOL.Absoluteness.md) (`FOL.Absoluteness`, First-order logic)
- [11. Models of ZF and ZFC](https://bedrock.institute/en/FOL.ZFModel.md) (`FOL.ZFModel`, First-order logic)
- [12. Mapping constants](https://bedrock.institute/en/FOL.Manipulation.ConstantMapping.md) (`FOL.Manipulation.ConstantMapping`, First-order logic)
- [13. Variable renaming](https://bedrock.institute/en/FOL.Manipulation.Renaming.md) (`FOL.Manipulation.Renaming`, First-order logic)
- [14. Constant relabelling](https://bedrock.institute/en/FOL.Manipulation.Relabelling.md) (`FOL.Manipulation.Relabelling`, First-order logic)
- [15. Relativization](https://bedrock.institute/en/FOL.Manipulation.Relativization.md) (`FOL.Manipulation.Relativization`, First-order logic)
- [16. Constant bounding](https://bedrock.institute/en/FOL.Manipulation.ConstantBounding.md) (`FOL.Manipulation.ConstantBounding`, First-order logic)
- [17. Constants by occurrence](https://bedrock.institute/en/FOL.Manipulation.ConstantOccurrences.md) (`FOL.Manipulation.ConstantOccurrences`, First-order logic)
- [18. Parameter abstraction](https://bedrock.institute/en/FOL.Manipulation.ParameterAbstraction.md) (`FOL.Manipulation.ParameterAbstraction`, First-order logic)
- [19. Syntax as sets](https://bedrock.institute/en/FOL.Coding.md) (`FOL.Coding`, First-order logic)
- [20. The cumulative hierarchy](https://bedrock.institute/en/V.Hierarchy.md) (`V.Hierarchy`, The ambient hierarchy)
- [21. Small truth values in the cumulative hierarchy](https://bedrock.institute/en/V.Smallness.md) (`V.Smallness`, The ambient hierarchy)
- [22. The cumulative hierarchy models ZF and ZFC](https://bedrock.institute/en/V.Model.md) (`V.Model`, The ambient hierarchy)
- [23. Coding inside the cumulative hierarchy](https://bedrock.institute/en/V.Coding.md) (`V.Coding`, The ambient hierarchy)
- [24. Definable subsets of a set](https://bedrock.institute/en/L.Definability.md) (`L.Definability`, Constructible stages and the axioms)
- [25. The constructible hierarchy and universe](https://bedrock.institute/en/L.Constructible.md) (`L.Constructible`, Constructible stages and the axioms)
- [26. Ordinal closure and finite ordinals](https://bedrock.institute/en/L.Ordinal.md) (`L.Ordinal`, Constructible stages and the axioms)
- [27. Von Neumann rank](https://bedrock.institute/en/L.Rank.md) (`L.Rank`, Constructible stages and the axioms)
- [28. Ordinals are linearly ordered by membership](https://bedrock.institute/en/L.Ordinal.Linear.md) (`L.Ordinal.Linear`, Constructible stages and the axioms)
- [29. Locating ordinals in the constructible hierarchy](https://bedrock.institute/en/L.Ordinal.Stages.md) (`L.Ordinal.Stages`, Constructible stages and the axioms)
- [30. The index of the least constructible stage](https://bedrock.institute/en/L.Stage.md) (`L.Stage`, Constructible stages and the axioms)
- [31. The basic axioms](https://bedrock.institute/en/L.Axioms.Basic.md) (`L.Axioms.Basic`, Constructible stages and the axioms)
- [32. Separation and replacement, bounded](https://bedrock.institute/en/L.Axioms.Separation.md) (`L.Axioms.Separation`, Constructible stages and the axioms)
- [33. Existential reflection into a constructible stage](https://bedrock.institute/en/L.ExistentialReflection.md) (`L.ExistentialReflection`, Constructible stages and the axioms)
- [34. Reflection for an arbitrary formula](https://bedrock.institute/en/L.FormulaReflection.md) (`L.FormulaReflection`, Constructible stages and the axioms)
- [35. Separation and replacement, in full](https://bedrock.institute/en/L.Axioms.Full.md) (`L.Axioms.Full`, Constructible stages and the axioms)
- [36. The power set in L](https://bedrock.institute/en/L.Axioms.Power.md) (`L.Axioms.Power`, Constructible stages and the axioms)
- [37. From ambient formulas to formulas over L](https://bedrock.institute/en/L.Absoluteness.md) (`L.Absoluteness`, Constructible stages and the axioms)
- [38. The numeral chain](https://bedrock.institute/en/L.Axioms.Numerals.md) (`L.Axioms.Numerals`, Constructible stages and the axioms)
- [39. The axiom of infinity in L](https://bedrock.institute/en/L.Axioms.Infinity.md) (`L.Axioms.Infinity`, Constructible stages and the axioms)
- [40. Formulas for singletons and pairs](https://bedrock.institute/en/L.Coding.PairFormulas.md) (`L.Coding.PairFormulas`, Internal coding: expressions and domains)
- [41. Finite environments as set-coded graphs](https://bedrock.institute/en/L.Coding.Environment.md) (`L.Coding.Environment`, Internal coding: expressions and domains)
- [42. Coding formulas over the constructible model](https://bedrock.institute/en/L.Coding.Model.md) (`L.Coding.Model`, Internal coding: expressions and domains)
- [43. Formula expressions for coded recursion](https://bedrock.institute/en/L.Coding.Expressions.md) (`L.Coding.Expressions`, Internal coding: expressions and domains)
- [44. Subcode-closed domains](https://bedrock.institute/en/L.Coding.Closure.md) (`L.Coding.Closure`, Internal coding: expressions and domains)
- [45. Rank descent through coded pairs](https://bedrock.institute/en/L.Coding.Descent.md) (`L.Coding.Descent`, Internal coding: expressions and domains)
- [46. Constructible codes and subformula trees](https://bedrock.institute/en/L.Coding.CodeConstructibility.md) (`L.Coding.CodeConstructibility`, Internal coding: expressions and domains)
- [47. Closure under subformulas](https://bedrock.institute/en/L.Coding.SubformulaClosure.md) (`L.Coding.SubformulaClosure`, Internal coding: expressions and domains)
- [48. The set of fixed-length environments](https://bedrock.institute/en/L.Coding.EnvironmentSet.md) (`L.Coding.EnvironmentSet`, Internal coding: tables and uniform satisfaction)
- [49. Satisfaction by recursion on formulas](https://bedrock.institute/en/L.Coding.Satisfaction.md) (`L.Coding.Satisfaction`, Internal coding: tables and uniform satisfaction)
- [50. Satisfaction and the recursion value](https://bedrock.institute/en/L.Coding.SatisfactionBridge.md) (`L.Coding.SatisfactionBridge`, Internal coding: tables and uniform satisfaction)
- [51. Satisfaction tables over subformulas](https://bedrock.institute/en/L.Coding.SatisfactionTable.md) (`L.Coding.SatisfactionTable`, Internal coding: tables and uniform satisfaction)
- [52. Agreement of environment sets](https://bedrock.institute/en/L.Coding.EnvironmentAgreement.md) (`L.Coding.EnvironmentAgreement`, Internal coding: tables and uniform satisfaction)
- [53. Closing a code slot under its seven constructors](https://bedrock.institute/en/L.Coding.SlotClosure.md) (`L.Coding.SlotClosure`, Internal coding: tables and uniform satisfaction)
- [54. Recognizing well-formed constructor keys](https://bedrock.institute/en/L.Coding.CodeShape.md) (`L.Coding.CodeShape`, Internal coding: tables and uniform satisfaction)
- [55. Recovering formulas from codes](https://bedrock.institute/en/L.Coding.FormulaRecovery.md) (`L.Coding.FormulaRecovery`, Internal coding: tables and uniform satisfaction)
- [56. Numerals in a successor-closed ordinal stage](https://bedrock.institute/en/L.Coding.NumeralBound.md) (`L.Coding.NumeralBound`, Internal coding: tables and uniform satisfaction)
- [57. Quantifying over coded pairs and finite formula families](https://bedrock.institute/en/L.Coding.Quantification.md) (`L.Coding.Quantification`, Internal coding: tables and uniform satisfaction)
- [58. Internalizing recursive definitions in L](https://bedrock.institute/en/L.Recursion.md) (`L.Recursion`, Internal coding: tables and uniform satisfaction)
- [59. Graphs of recursive definitions](https://bedrock.institute/en/L.Recursion.Graph.md) (`L.Recursion.Graph`, Internal coding: tables and uniform satisfaction)
- [60. The environment tower](https://bedrock.institute/en/L.Coding.EnvironmentTower.md) (`L.Coding.EnvironmentTower`, Internal coding: tables and uniform satisfaction)
- [61. The set of all formula codes](https://bedrock.institute/en/L.Coding.CodeSet.md) (`L.Coding.CodeSet`, Internal coding: tables and uniform satisfaction)
- [62. Describing the closed domain of formula codes](https://bedrock.institute/en/L.Coding.CodeDomain.md) (`L.Coding.CodeDomain`, Internal coding: tables and uniform satisfaction)
- [63. Describing the satisfaction table](https://bedrock.institute/en/L.Coding.SatisfactionClauses.md) (`L.Coding.SatisfactionClauses`, Internal coding: tables and uniform satisfaction)
- [64. The alphabet of formula codes](https://bedrock.institute/en/L.Coding.CodeAlphabet.md) (`L.Coding.CodeAlphabet`, Internal coding: tables and uniform satisfaction)
- [65. Reading and validating the satisfaction clauses](https://bedrock.institute/en/L.Coding.SatisfactionClauseSemantics.md) (`L.Coding.SatisfactionClauseSemantics`, Internal coding: tables and uniform satisfaction)
- [66. Pinning recursion on a subcode-closed domain](https://bedrock.institute/en/L.Coding.PinnedRecursion.md) (`L.Coding.PinnedRecursion`, Internal coding: tables and uniform satisfaction): Recursion pinned to a subcode-closed index set
- [67. The satisfaction graph formula](https://bedrock.institute/en/L.Coding.SatisfactionGraph.md) (`L.Coding.SatisfactionGraph`, Internal coding: tables and uniform satisfaction)
- [68. Uniform satisfaction over all codes](https://bedrock.institute/en/L.Coding.UniformSatisfaction.md) (`L.Coding.UniformSatisfaction`, Internal coding: tables and uniform satisfaction)
- [69. A formula for the definable power set](https://bedrock.institute/en/L.Coding.DefinablePowerSet.md) (`L.Coding.DefinablePowerSet`, Internal coding: tables and uniform satisfaction)
- [70. A sequence for the constructible hierarchy](https://bedrock.institute/en/L.Coding.HierarchySequence.md) (`L.Coding.HierarchySequence`, Internal coding: tables and uniform satisfaction)
- [71. The constructible hierarchy inside L](https://bedrock.institute/en/L.Hierarchy.md) (`L.Hierarchy`, Internal coding: tables and uniform satisfaction)
- [72. The first stage meeting a set](https://bedrock.institute/en/L.Choice.FirstIntersectionStage.md) (`L.Choice.FirstIntersectionStage`, The canonical well-order and Choice)
- [73. Strict well-orders and least-element search](https://bedrock.institute/en/L.WellOrder.Base.md) (`L.WellOrder.Base`, The canonical well-order and Choice)
- [74. Well-orders on finite stages](https://bedrock.institute/en/L.Choice.FiniteStageOrders.md) (`L.Choice.FiniteStageOrders`, The canonical well-order and Choice)
- [75. Canonical names for successor-stage members](https://bedrock.institute/en/L.Choice.CanonicalNames.md) (`L.Choice.CanonicalNames`, The canonical well-order and Choice)
- [76. Well-orders on all stages](https://bedrock.institute/en/L.Choice.StageOrders.md) (`L.Choice.StageOrders`, The canonical well-order and Choice)
- [77. Formulas for name comparison](https://bedrock.institute/en/L.Choice.NameComparison.md) (`L.Choice.NameComparison`, The canonical well-order and Choice)
- [78. An internal table of stage orders](https://bedrock.institute/en/L.Choice.OrderTable.md) (`L.Choice.OrderTable`, The canonical well-order and Choice)
- [79. Adequacy of the stage-order description](https://bedrock.institute/en/L.Choice.StageOrderAdequacy.md) (`L.Choice.StageOrderAdequacy`, The canonical well-order and Choice)
- [80. Adequacy of name comparison](https://bedrock.institute/en/L.Choice.NameComparisonAdequacy.md) (`L.Choice.NameComparisonAdequacy`, The canonical well-order and Choice)
- [81. The limit-stage order inside L](https://bedrock.institute/en/L.Choice.LimitStageOrder.md) (`L.Choice.LimitStageOrder`, The canonical well-order and Choice)
- [82. An internal family of earliest-disagreement relations](https://bedrock.institute/en/L.Choice.EarliestDisagreement.md) (`L.Choice.EarliestDisagreement`, The canonical well-order and Choice)
- [83. The internal stage-order relation](https://bedrock.institute/en/L.Choice.InternalWellOrder.md) (`L.Choice.InternalWellOrder`, The canonical well-order and Choice): The internal canonical well-order
- [84. Choice by a transversal](https://bedrock.institute/en/L.Choice.Transversal.md) (`L.Choice.Transversal`, The canonical well-order and Choice)
- [85. The constructible universe models ZFC](https://bedrock.institute/en/L.Model.md) (`L.Model`, The canonical well-order and Choice)
- [86. Small presentations of sets](https://bedrock.institute/en/V.Presentation.md) (`V.Presentation`, Ordinals, injections and cardinals)
- [87. Ordinal indices, the Gödel pair order, and finite indices](https://bedrock.institute/en/L.Ordinal.SquareLaw.md) (`L.Ordinal.SquareLaw`, Ordinals, injections and cardinals)
- [88. Coded injections](https://bedrock.institute/en/L.Coding.Injection.md) (`L.Coding.Injection`, Ordinals, injections and cardinals)
- [89. Cardinals and coded injections inside L](https://bedrock.institute/en/L.Cardinal.md) (`L.Cardinal`, Ordinals, injections and cardinals)
- [90. Turning a definable injection into an internal code](https://bedrock.institute/en/L.DefinableInjection.md) (`L.DefinableInjection`, Ordinals, injections and cardinals)
- [91. Composition and inclusion of coded injections](https://bedrock.institute/en/L.InjectionComposition.md) (`L.InjectionComposition`, Ordinals, injections and cardinals)
- [92. The generalized continuum hypothesis inside L](https://bedrock.institute/en/L.GCH.md) (`L.GCH`, Ordinals, injections and cardinals)
- [93. Cantor–Schröder–Bernstein for small presentations](https://bedrock.institute/en/V.CantorBernstein.md) (`V.CantorBernstein`, Ordinals, injections and cardinals)
- [94. Cantor–Schröder–Bernstein inside L](https://bedrock.institute/en/L.CantorBernstein.md) (`L.CantorBernstein`, Ordinals, injections and cardinals)
- [95. Collapsing a transitive well-founded relation](https://bedrock.institute/en/L.Mostowski.md) (`L.Mostowski`, Ordinals, injections and cardinals)
- [96. An ordinal L-cardinal above every L-cardinal](https://bedrock.institute/en/L.CardinalAbove.md) (`L.CardinalAbove`, Ordinals, injections and cardinals)
- [97. Assembling GCH from four internal bounds](https://bedrock.institute/en/L.GCH.Assembly.md) (`L.GCH.Assembly`, Proving GCH)
- [98. An internal graph of uniform satisfaction](https://bedrock.institute/en/L.Coding.SatisfactionGraphSet.md) (`L.Coding.SatisfactionGraphSet`, Proving GCH)
- [99. Soundness and completeness of the closed code domain](https://bedrock.institute/en/L.Coding.CodeDomainAdequacy.md) (`L.Coding.CodeDomainAdequacy`, Proving GCH)
- [100. A Δ₀ description of the satisfaction table](https://bedrock.institute/en/L.GCH.SatisfactionDescription.md) (`L.GCH.SatisfactionDescription`, Proving GCH)
- [101. A Δ₀ description of the definable power set](https://bedrock.institute/en/L.GCH.DefinablePowerSetDescription.md) (`L.GCH.DefinablePowerSetDescription`, Proving GCH)
- [102. Adequate stages for the GCH argument](https://bedrock.institute/en/L.GCH.AdequateStages.md) (`L.GCH.AdequateStages`, Proving GCH)
- [103. ω-recursion inside the constructible universe](https://bedrock.institute/en/L.GCH.OmegaRecursion.md) (`L.GCH.OmegaRecursion`, Proving GCH): Iterating a definable step through ω
- [104. The Mostowski collapse](https://bedrock.institute/en/V.Collapse.md) (`V.Collapse`, Proving GCH)
- [105. Building and collapsing a Skolem hull](https://bedrock.institute/en/L.GCH.SkolemHull.md) (`L.GCH.SkolemHull`, Proving GCH)
- [106. A Δ₀ description of the constructible hierarchy](https://bedrock.institute/en/L.GCH.HierarchyDescription.md) (`L.GCH.HierarchyDescription`, Proving GCH)
- [107. Transferring structure through condensation](https://bedrock.institute/en/L.GCH.CondensationTransfer.md) (`L.GCH.CondensationTransfer`, Proving GCH)
- [108. Ordinals below a successor cardinal inject into its base](https://bedrock.institute/en/L.GCH.BelowSuccessorCardinal.md) (`L.GCH.BelowSuccessorCardinal`, Proving GCH)
- [109. Constructing order types inside L](https://bedrock.institute/en/L.GCH.OrderType.md) (`L.GCH.OrderType`, Proving GCH)
- [110. Choosing a cardinal representative for an ordinal](https://bedrock.institute/en/L.GCH.CardinalRepresentative.md) (`L.GCH.CardinalRepresentative`, Proving GCH)
- [111. The square law for infinite L-cardinals](https://bedrock.institute/en/L.GCH.CardinalSquareLaw.md) (`L.GCH.CardinalSquareLaw`, Proving GCH)
- [112. The least-witness map inside a constructible stage](https://bedrock.institute/en/L.GCH.LeastWitnessMap.md) (`L.GCH.LeastWitnessMap`, Proving GCH): Least witnesses form a definable map
- [113. Injecting the successor cardinal into the power set](https://bedrock.institute/en/L.GCH.SuccessorIntoPowerSet.md) (`L.GCH.SuccessorIntoPowerSet`, Proving GCH)
- [114. Coding finite sequences below an infinite ordinal](https://bedrock.institute/en/L.GCH.FiniteSequenceCoding.md) (`L.GCH.FiniteSequenceCoding`, Proving GCH)
- [115. The counting tools for infinite constructible stages](https://bedrock.institute/en/L.GCH.StageCountingTools.md) (`L.GCH.StageCountingTools`, Proving GCH)
- [116. Locating the hull and its collapse inside L](https://bedrock.institute/en/L.GCH.ConstructibleHull.md) (`L.GCH.ConstructibleHull`, Proving GCH)
- [117. Counting a Skolem hull from a counted start](https://bedrock.institute/en/L.GCH.HullCounting.md) (`L.GCH.HullCounting`, Proving GCH)
- [118. Injecting an infinite constructible stage into its index](https://bedrock.institute/en/L.GCH.StageInjection.md) (`L.GCH.StageInjection`, Proving GCH)
- [119. Bounded subsets appear at controlled stages](https://bedrock.institute/en/L.GCH.BoundedSubset.md) (`L.GCH.BoundedSubset`, Proving GCH)
- [120. The constructible universe satisfies GCH](https://bedrock.institute/en/L.GCH.Theorem.md) (`L.GCH.Theorem`, Proving GCH)

## Other editions

- [Chinese (zh)](https://bedrock.institute/zh/index.html): the same book. Chapter mirrors are at `/zh/<Module>.md`.
- [Japanese (ja)](https://bedrock.institute/ja/index.html): the same book. Chapter mirrors are at `/ja/<Module>.md`.