---
homepage_title: "Bedrock"
tagline: "Laying the groundwork for the metaphysics of 𝑉"
title: "Origin"
module: Origin
lang: en
site: "Bedrock"
description: "The book's proved endpoint results, with routes leading to each theorem."
stage: "Preview"
reading_order: 1
canonical: https://bedrock.institute/en/index.html
html: index.html#milestones
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Origin.lagda.md
prerequisites: []
routes: []
translations: [https://bedrock.institute/zh/index.md, https://bedrock.institute/ja/index.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


```agda
{-# OPTIONS --cubical --safe --guardedness #-}
module Origin where
```

# Origin

Origin joins the beginning of the book to its end: first a reason for the journey, then the results to which its proofs lead.

## Preface

Bedrock develops machine-checked set theory in Cubical Agda, as groundwork for questions about the universe of sets. Its first completed goal is that the constructible universe satisfies ZFC and GCH. The chapters build the language, models and proofs needed to reach these results; the milestones below give a view of the destination before the journey begins.

The guiding choice is to express mathematics in the host language wherever possible, using a deeply embedded first-order language when formulas themselves are the objects of study. Cubical type theory also lets us construct the cumulative hierarchy as a higher inductive type. This is a choice of mathematical foundation, not a claim that the metatheory is weaker than the theories it studies.

Beyond this first goal lie questions about forcing, inner models and the structure of 𝑉. They motivate the project, but are not results claimed by this book. The purpose is to provide verified groundwork for those questions.

## Milestones

**Theorem 0** `SetChoice` implies `LEM`, which in turn implies `ΩResizing`.

```agda
open import Base.Choice public using ( SetChoice→LEM )
open import Base.Classical public using ( LEM→ΩResizing )
```

**Theorem 1** Assuming `ΩResizing`, the HIT cumulative hierarchy [V](V.Hierarchy.html#𝒮ᵥ) is a model of [ZF](FOL.ZFModel.html#isZFModel).

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

**Theorem 2** Assuming `SetChoice`, the HIT cumulative hierarchy [V](V.Hierarchy.html#𝒮ᵥ) is a model of [ZFC](FOL.ZFModel.html#isZFCModel).

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

**Theorem 3** Assuming `LEM`, the constructible universe [L](L.Constructible.html#𝒮ʟ) is a model of [ZFC](FOL.ZFModel.html#isZFCModel).

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

**Theorem 4** Assuming `LEM`, the constructible universe [L](L.Constructible.html#𝒮ʟ) satisfies the [generalized continuum hypothesis](L.GCH.html#GCHStatement) internally.

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