Reading guide

Choose a route, inspect the prerequisite structure, or review the book's main theorems and terminology.

Choose a topic, compare routes, or continue from completed prerequisites.

Dependency map

Dependencies between 120 chapters flow from top to bottom. A → B means B imports A. Every layout shows the same prerequisite partial order. Topics with no dependency path may be interleaved. Hover to trace prerequisites; click to pin.

Layout: Edges: skeleton (transitive reduction) all direct imports include Milestones' references

Color key

Select a chapter to trace its prerequisites

Scroll the graph in both directions, or fit the whole graph for an overview.

The widely used Base.Prelude imports are omitted from the drawing but retained in chapter details. The skeleton preserves reachability, not every direct use of a definition. An omitted edge is not permission to delete an import. Learning stages do not make every chapter a serial step: finish the listed prerequisites before a converging chapter. Milestones is the opening preview and appears at the bottom here as the endpoint.

Milestones

This page gathers the book's proved endpoint results and offers a concise entrance to the routes that lead to them. Each entry states a theorem in ordinary mathematical language, then imports the exact Agda declaration that proves it.

{-# OPTIONS --cubical --safe --guardedness #-}

module Milestones where

Theorem 1. Under the excluded-middle assumption, the host-level V is a model of ZF.

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

Theorem 2. Under the host-level axiom-of-choice assumption, the host-level V is a model of ZFC.

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

Theorem 3. Under the excluded-middle assumption, the constructible universe L is a model of ZFC.

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

Theorem 4. Under the same excluded-middle assumption, the constructible universe L satisfies the generalized continuum hypothesis internally.

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

Glossary

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.
field: A named component of a record type, retrieved by the projection of the same name.
constructor: A primitive operation that builds an element of an inductive type or a record type.
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.
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.
underlying type: The type obtained by forgetting the additional property or structure packaged with it; for P : hProp ℓ, this is the first component ⟨ P ⟩.
empty type: The type with no constructors; since it has no element, it eliminates into any type.
propositional truncation: The operation sending a type to a proposition with the same inhabitedness, keeping that an element exists and forgetting which one.
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.
logical equivalence: Logical equivalence gives implications in both directions; for propositions, isProp promotes these maps to a type equivalence.
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 inverse laws.