BedrockBedrock
Laying the groundwork for the metaphysics of 𝑉
A trilingual textbook of machine-checked set theory in Cubical Agda. Proving ZFC and GCH in the constructible universe L, assuming excluded middle.
Begin with the main theorems, then choose a reading route or inspect their prerequisites.
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.
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 is a model of ZF.
open import V.Model public using ( V⊨ZF )
Theorem 2 Assuming SetChoice, the HIT cumulative hierarchy V is a model of ZFC.
open import V.Model public using ( V⊨ZFC )
Theorem 3 Assuming LEM, the constructible universe L is a model of ZFC.
open import L.Model public using ( L⊨ZFC )
Theorem 4 Assuming LEM, the constructible universe L satisfies the generalized continuum hypothesis internally.
open import L.GCH.Theorem public using ( L⊨GCH )
{-# OPTIONS --cubical --safe --guardedness #-}
module Origin whereopen import Base.Choice public using ( SetChoice→LEM )open import Base.Classical public using ( LEM→ΩResizing )open import V.Model public using ( V⊨ZF )
open import V.Model public using ( V⊨ZFC )open import L.Model public using ( L⊨ZFC )open import L.GCH.Theorem public using ( L⊨GCH )Choose a topic, compare routes, or continue from completed prerequisites.
Interactive contents · Dependency graphGlossary
The terms are ordered by their first appearance in the book. Select a term to revisit its introduction.
- object theory
- The theory being represented and studied inside the metatheory; in this book, set theory.
- metatheory
- The theory in which the object theory is represented and studied; here, cubical type theory.
- host
- The Cubical Agda environment that supports the formalisation of the object theory.
- universe level
- The size index ℓ of a type universe Type ℓ; it is distinct from a homotopy level and from a layer of the constructible hierarchy.
- Π type
- A dependent function type whose result type may vary with its input.
- dependent function
- An element of a Π type: it assigns to every input an element of the type corresponding to that input.
- Σ type
- A dependent pair type whose second component's type may depend on its first component.
- dependent pair
- An element of a Σ type: a chosen first component together with data belonging to the corresponding type.
- first component
- The element chosen first in a dependent pair, extracted by fst.
- second component
- The element of a dependent pair whose type may depend on the first component, extracted by snd.
- certificate
- A proof carried together with an object so that later reasoning may use the property it establishes.
- precedence
- The rule for grouping operators when parentheses are omitted; it does not change which expressions are legal.
- sum type
- An inductive type A ⊎ B whose values retain whether they came from A or B and the value from that side.
- inductive type
- A type generated by specified constructors, whose elements are analyzed by the corresponding induction principle.
- constructor
- A primitive operation that builds an element of an inductive type or a record type.
- record type
- A type that groups values into named fields; the type of a later field may depend on earlier fields.
- field
- A named component of a record type, retrieved by the projection of the same name.
- projection
- An operation that retrieves one component from a pair or one field from a record.
- path
- An equality proof between two elements of a type; it has a source and a target, and can be reversed and composed.
- judgmental equality
- Equality recognized by the type system's definition and computation rules, written = here; it is a judgment, not a path type.
- homotopy level
- A classification of types by how much distinguishable structure remains among their elements and equality proofs.
- contractible
- A type with a chosen centre to which every element is joined by a path.
- unique existence
- Existence together with uniqueness; here it is represented by a contractible type whose centre supplies the witness.
- proposition
- A type any two of whose elements are equal, so that it retains only whether a proof exists.
- h-set
- A type whose equality types are propositions: elements may differ, but any two proofs that they are equal agree.
- type equivalence
- An equivalence A ≃ B is a map with contractible fibres; an inverse and both round-trip paths follow from this condition.
- fibre
- The fibre of f : A → B over b : B is the dependent pair type Σ (a : A) (f a ≡ b), whose elements are preimages together with paths witnessing their images.
- isomorphism
- An isomorphism explicitly supplies forward and inverse maps together with the two round-trip laws.
- round-trip law
- A law stating that going there and back recovers the input up to a path. For f : A → B and g : B → A, the two laws are g (f a) ≡ a and f (g b) ≡ b, for every input.
- underlying type
- The type obtained by forgetting the additional property or structure packaged with it; for P : hProp ℓ, this is the first component ⟨ P ⟩.
- propositional truncation
- The operation sending a type to a proposition with the same inhabitedness, keeping that an element exists and forgetting which one.
- higher inductive type (HIT)
- An inductive type whose generators may include paths and higher paths as well as points.
- mere existence
- Existence expressed by propositional truncation: ∥ A ∥₁ says that A has an element without specifying one; for a predicate P, ∥ Σ[ x ∶ A ] P x ∥₁ says that a witness merely exists.
- empty type
- The type with no constructors; since it has no element, it eliminates into any type.
- logical equivalence
- Logical equivalence gives implications in both directions; for propositions, isProp promotes these maps to a type equivalence.
- class
- A predicate on a given domain, represented here as a function from that domain to the universe of propositions.
- domain
- The type over which variables range; calling it a domain adds no relation, operation or other structure.
- carrier
- The underlying type of objects on which the relations and operations of a structure are defined.
- propositional resizing
- Propositional resizing replaces each proposition by a type-equivalent representative at a chosen universe level.
- Ω-resizing
- Ω-resizing presents an entire proposition universe by a type in a chosen universe level.
- choice for set-valued families
- For an h-set X and a family B of h-sets, pointwise mere inhabitation implies the mere existence of a dependent function choosing in every B x. SetChoice requires both X and each B x to be h-sets.
- set quotient
- A / R has points [ a ], paths induced by R a b, and a constructor making it an h-set. For a proposition-valued equivalence relation, a path between classes also yields the relation.
- object language
- The formal language whose terms and formulas describe set-theoretic claims; their meaning is supplied separately.
- term
- A written expression referring to one object, built here from a constant name or a variable position.
- constant name
- A symbol selected from K for a term; its denoted object is not fixed by the syntax alone.
- constant domain
- The type K of constant names available when building a term or formula; it need not be a model's carrier.
- context
- The finite list of variable positions currently available to an expression; n is its length.
- variable position
- A numbered slot available in the current context, represented by an element of Fin n.
- formula
- A written claim built from atomic comparisons, connectives and quantifiers; syntax alone does not say whether it holds.
- atomic formula
- A formula formed directly by comparing two terms with membership or equality, before connectives or quantifiers are added.
- quantifier
- A syntax form for every or some object; its body receives one new variable position.
- bound variable
- A variable occurrence whose object is supplied by an enclosing quantifier.
- free variable
- A variable occurrence not supplied by the quantifier under discussion; its value comes from the outer context.
- de Bruijn indexing
- Representing variables by the number of binders between their occurrence and the binder they refer to, instead of storing names.
- bounded quantifier
- A quantifier ranging over members of a set named by a term, rather than over every object.
- sentence
- A formula with no free variables; it may still contain constant names.
- parameter-free
- A formula without constant names, written here with the empty constant domain; it may still have free variables.
- environment
- A vector assigning a carrier element to each available variable position. Its length agrees with the context length of the term or formula.
- constant interpretation
- A function ι : K → S assigning a carrier element to each constant name. It remains fixed when quantifiers extend the variable environment.
- term evaluation
- The carrier value ⟦ t ⟧ γ of a term: a constant is read through ι, and a variable through its position in γ.
- satisfaction
- With a structure and constant interpretation fixed, γ ⊨ φ is the proposition that φ holds under the variable assignment γ; its interpretation is not itself a decision of truth.
- isomorphism of structures
- A bijection between the carriers that preserves and reflects the structure's relations; here the relation is membership.
No matching terms.