Bedrock

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 target is a full mechanization of L ⊨ GCH, with the cumulative hierarchy V realised as a higher inductive type. The full treatment is in the Charter.

This site is generated from literate Agda. The development has no substantial content yet; the modules below are examples that exercise the rendering framework. Browse them from the sidebar, or in the import list below.

{-# OPTIONS --cubical --safe --guardedness #-}
module Everything where

import HelloWorld
import Example.Naturals
import Example.Doubling