English · 中文 · 日本語

Typecheck Status: early Agda cubical Content: CC BY-NC-SA 4.0 Code: AGPL-3.0-only REUSE status

Laying the groundwork for the metaphysics of V.

A machine-checked development, in Cubical Agda, of the set theory underlying contemporary questions about the universe of sets: forcing, inner models, and the structure of V.

The immediate, self-contained target is a full mechanization of

L ⊨ GCH, where L is the constructible hierarchy built over the cumulative hierarchy V realised as a higher inductive type. This is a semantic theorem internal to the host.

The content is Gödel's 1938 result, but the route is not the textbook one, and not one anyone has taken for GCH. It is the right first stone because it exercises the entire base layer the rest of the project needs: a deeply embedded first-order language, the cumulative hierarchy, L, and the dual-semantics machinery. And it commits from line one to the host-language-maximalist approach described below. Getting it right calibrates the infrastructure everything else will stand on.

Beyond that first stone, the long-term aim is to push mechanized set theory past where it currently stops. Existing forcing formalizations end at Cohen (1963); the goal is to reach results from this century: forcing as a tool for studying the multiverse, the definability of ground models, the mantle, and the broader question of whether V has a determinate structure at all.

These are goals, not promises. Each will be claimed here only when it is checked.

The aim is not to settle the metaphysics of V but to lay verified groundwork for it: mechanizing the theorems that arbitrate the debate, such as ground-model definability, the mantle, and generic absoluteness, is groundwork in the literal sense.

The one choice everything follows from is host-language maximalism: rather than transcribing the textbook ZF axioms and bending the proof assistant around them, every notion is reconstructed in type-theory-native idiom, so the host does the speaking and the deep-embedded Formula is what gets studied. This can look like the opposite of grounding, but a proof assistant offers rigor, not a reductive base, and rigor is independent of the metatheory's strength; maximalism is what makes the checking attainable, and its cost is declared openly.

The groundwork is also neutral: set-theoretic geology gives both universism and multiversism the rigorous footing each has lacked, and parameterises the dispute by the strength of the infinity axiom assumed, so the project takes no side.

The full treatment is in the Charter.

Cubical type theory is the frontier of contemporary type theory: the foundations of mathematics worked out in the present tense. The metaphysics of V is the most classical branch of the same inquiry, the oldest question of what the mathematical universe is. Carrying the most classical of foundational questions into the most contemporary of foundations is not a constraint to be tolerated but one of the things this project is for; the contrast between the two is deliberate.

The choice earns its keep as well: the cumulative hierarchy V is realised here as a higher inductive type, which cubical makes computational rather than postulated. But the deeper reason is the contrast itself.

Bedrock is the deepest ground model; whether one exists at all is a delicate, large-cardinal-sensitive question (Usuba's theorem). The name also reads in the ordinary sense: the groundwork beneath an inquiry. Both meanings are intended.

Everything in this project is produced with AI assistance, and every line of it, this document included, is reviewed word by word by the author.

The development typechecks against the following pinned toolchain:

make check and the site build run on Python 3.11+; developer tooling (the reuse linter) is pinned in requirements-dev.txt and installed into a local virtual environment by make venv (run once per clone). Every push is typechecked against these versions by GitHub Actions.

AI agents work from AGENTS.md; human contributors, start with CONTRIBUTING.md.

Bedrock is multi-licensed; per-file terms are declared in REUSE.toml and verified by reuse lint. In short:

• CC BY-NC-SA 4.0 : the maths, prose, and brand assets (src/, docs/, README, site/static/assets/).
• AGPL-3.0-only : all other first-party code and config, including the vendored 1lab front-end.
• OFL-1.1 : the self-hosted web fonts (site/static/fonts/).

Full texts are in LICENSES/; NOTICE has the third-party attributions and the AGPL section 13 corresponding-source statement.

© 2026 choukh (choukyuhei@gmail.com).