Prelude

When studying set theory, we talk about sets and their elements, relations between sets, and functions from one set to another. A definition tells us what an object is, a theorem states a property it has, and a proof explains why that property holds. In this book, set theory is the object theory and cubical type theory is the metatheory: within cubical type theory, we construct models of set theory, interpret its sentences, and prove that these models satisfy the relevant axioms and theorems.

We write and check these constructions and proofs with the Agda proof assistant. Agda provides the formal language and its checking mechanisms, cubical type theory supplies the mathematical foundation for this formalisation, and the Cubical library collects definitions and theorems developed on that foundation. We call this Cubical Agda environment, which supports the formalisation of the object theory, the host. Thus, later references to a type in the host, a function in the host, or a host-level construction concern the metatheory rather than objects inside a model of set theory.

To read these developments, we first need to become acquainted with the basic vocabulary of the host.

This chapter begins with the basic notions of that language. We will meet them one at a time, considering both what they mean and how they are used in mathematical statements and proofs. There is no need to remember every symbol at once. As the same notions recur in later chapters, their uses will become more familiar; when needed, this chapter provides a place to return to their meanings.

Traceable vocabulary

To make such references easier, we first explain where these basic notions come from and how to find their definitions.

In later chapters, you will see statements containing import near the beginning. They specify which names the chapter imports from which modules, identifying the concepts and results used in the arguments that follow. When a name is unfamiliar, these statements tell you where it comes from; clicking the name takes you to its definition.

The basic vocabulary collected in this chapter is an exception to this convention. These notions occur so frequently throughout the book that we gather them in Base.Prelude, which later chapters import as a whole without listing each name again. Here we list the selected definitions from the Cubical library and explain the meanings and uses needed to read this book, without developing each construction and proof inside the library. For further study, you can follow the name links to the original definitions or consult the Cubical library's documentation and learning materials on cubical type theory.

Before introducing this vocabulary, we explain two short lines of code:

• The first line specifies the options Agda uses to check this chapter.
  Expand option details

  • --cubical enables language support for cubical type theory.
  • --safe enables safe mode, which prohibits declaring unproved axioms and bypassing checks such as termination checking. Theorems that need additional assumptions can still be stated, but those assumptions must appear explicitly as parameters or premises.
  • --guardedness enables checking associated with corecursive definitions. Such definitions can describe objects whose content continues to unfold, such as infinite sequences; the check constrains recursion so that the required content can be produced progressively. On a first reading, it is enough to know that this is an Agda setting for checking such definitions; its technical details can wait.
• The second line gives the module corresponding to this chapter its name. Here Base.Prelude is the basic vocabulary module mentioned above. Later chapters use this name to import the vocabulary collected here, and the content following where forms the body of the module.

{-# OPTIONS --cubical --safe --guardedness #-}
module Base.Prelude where

With the two lines now identified, and the module body located after where, we can begin to explore the notions one at a time.

Universe levels

Type theory must distinguish the sizes of types. A type that quantifies over all types would contain itself, so the host sorts types into universes Type ℓ, one for each level ℓ : Level. Algebraically, universe levels form a join-semilattice with a bottom element, equipped with a successor operator: ℓ-zero is the bottom element, ℓ-suc is the successor operator and ℓ-max is the binary join. Each universe is itself a type:

Whenever the book surveys a totality such as "all sets" or "all propositions", the attached level records how large that totality is taken to be.

open import Cubical.Foundations.Prelude public
  using ( Type; Level; ℓ-zero; ℓ-suc; ℓ-max )

Π types

Many constructions later in the book need to provide data depending on each object. A Π type expresses this basic relationship.

Given a type A and a type B x for each x : A, we form the Π type:

An element of a Π type is called a dependent function. Given a dependent function f, it assigns to every x : A an element f x of B x. Because the type of the result depends on the input x, only after fixing the input do we know the type in which the corresponding output must lie.

When B does not depend on x, every output lies in the same type, and the dependent function specialises to an ordinary function:

An ordinary function gives an output in the same type for every input; a Π type gives, for every x, data belonging to the corresponding type B x.

Σ types

Many constructions later in the book need to keep a particular object together with a piece of data that depends on it. A Σ type expresses this basic relationship.

Given a type A and a type B x for each x : A, we form the Σ type:

An element of a Σ type is called a dependent pair. It is built in two steps: choose a : A, then choose an element b of B a; the resulting pair is written (a , b). We call a the first component and b the second component. Because the type of the second component depends on a, only after fixing the first component do we know the type in which the second must lie.

When B does not depend on x, every second component lies in the same type, and the dependent pair specialises to an ordinary product:

An ordinary product places two independent elements together; a Σ type places a particular a together with data belonging to the corresponding type B a. Dependent pairs are built with _,_, fst extracts the first component, and snd extracts the second.

A Π type handles "for every x, give data depending on x"; a Σ type handles "choose an x, and keep it together with data depending on it".

The second component may itself be a proof of a property of the first. This book calls a proof carried together with an object so that later reasoning may use the property a certificate. A certificate remains an ordinary Agda proof; the name emphasizes its role in the dependent pair.

open import Cubical.Data.Sigma public
  using ( Σ; Σ-syntax; _×_; _,_; fst; snd )

Record types

A record type can be understood as syntactic sugar for several nested Σ types. For example, suppose we want to package an element a : A, an element b : B a depending on a, and a proof c : C a b depending on both. The corresponding nested type is:

Its elements have the shape:

In Agda, the keyword record begins the declaration of such a type, after which its components are given field names. Constructing an element of the record requires a value for every field. A record declaration may also use the keyword constructor to name this operation; that name is the record type's constructor. The constructor accepts the field values in dependency order and assembles them into one record. If three fields correspond to a, b and c, a constructor named mkR can present the construction in the flat form:

This carries the same data as the nested Σ value (a , (b , c)), without exposing the nesting. Field names act as projections that retrieve the corresponding components directly. One therefore need not remember the depth of a component or repeatedly compose fst and snd. Records preserve the dependent structure of nested Σ types while presenting larger packages through a clearer, flat interface. The Agda documentation on record types describes their declaration, construction and projections in detail.

Moving between universe levels

The Agda type universes used here are not cumulative. An element of Type ℓ does not automatically become an element of Type (ℓ-suc ℓ); moving a type between levels requires the explicit operation Lift.

Lift ℓ A is itself a record type. It has one field, lower : A, which stores an element of the original type A; its constructor is lift. Given a : A, the constructor produces lift a : Lift ℓ A. Conversely, given b : Lift ℓ A, the field projection lower b retrieves the stored element of A.

The functions lift and lower are mutually inverse between A and Lift ℓ A. Two equations state the two directions separately:

The first says that packaging an element and immediately retrieving it returns the original element. The second says that retrieving an element from a lifted record and packaging it again returns the original record. Thus Lift changes the universe in which a type is presented and the representation of its elements, without adding or losing mathematical information.

More precisely, if A lives in Type ℓ₁, then Lift ℓ₂ A lives in Type (ℓ-max ℓ₁ ℓ₂). If either universe level is already above the other, ℓ-max keeps it; otherwise it gives a common universe level large enough for both. Hence Lift does not raise a type by a fixed number of levels. It places the type in a universe large enough for the levels at hand.

A type can always be copied upward in this way, but there is in general no way to move one down.

open import Cubical.Foundations.Prelude public
  using ( Lift; lift; lower )

Equality and paths

In ordinary mathematical language, x = y is a proposition asserting that two objects are equal. In type theory, propositions are represented by types, so equality is represented by a type as well. For two elements x and y of A, x ≡ y is the type corresponding to the proposition that x and y are equal, and its elements are proofs of that equality.

In cubical type theory, such an equality proof is called a path from x to y, and x ≡ y is called a path type. A path is therefore not another relation alongside equality: paths are the equality proofs used in this book, and path types are how the book represents equality. A path has a source and a target, so its direction can be reversed and paths can be joined end to end. The basic operations below arise from this structure.

• refl is a path from an element to itself and gives reflexivity of equality.
• sym reverses a path; a path from x to y thereby becomes a path from y to x.
• _∙_ composes paths whose endpoints meet; a path from x to y followed by one from y to z gives a path from x to z.
• cong says that functions preserve equality: equal inputs are sent to equal outputs. cong₂ is the corresponding binary operation.
• funExt turns pointwise equality into equality of functions: if f x ≡ g x for every x, then f ≡ g.
• transport moves an element along a path between types; subst moves data depending on x along x ≡ y to data depending on y.

For example, given a function f : A → B, the action of cong can be summarized as:

This says that f can act on an equality path, turning equality between inputs into equality between outputs.

Paths are themselves elements of a type, so two paths can in turn be equal. Equality structure can therefore continue to higher levels: we may ask not only whether two elements are equal, but also whether their equality proofs are equal. The next section introduces a hierarchy that measures how many such levels of equality structure a type retains.

For further details on path types in Cubical Agda, see the Cubical chapter of the Agda 2.8.0 manual. This section uses only the basic properties needed for the constructions that follow.

open import Cubical.Foundations.Prelude public
  using ( _≡_; refl; sym; _∙_; cong; cong₂; transport; subst; funExt )

Homotopy levels

Paths are themselves elements of types, so new paths can in turn relate paths. Homotopy levels classify types by how much distinguishable structure remains in these equality proofs. They do not measure the size of a type: universe levels handle size, whereas homotopy levels concern how elements and their equality proofs can be distinguished.

• isContr A: A is contractible. This requires a chosen centre in A and, for every x : A, a path from the centre to x. Thus A must be inhabited, and every element is equal to the chosen centre, so no two elements can be distinguished by equality. This book reads the data carried by isContr as unique existence: the centre supplies existence, and the paths from the centre to every element supply uniqueness.
• isProp A: A is a proposition. This requires any two elements of A to be equal. It neither chooses a centre nor requires A to be inhabited; it says only that if proofs of A exist, no distinction remains between them. A proposition may therefore have no proof or have a proof, but it cannot have two distinguishable proofs.
• isSet A: A is an h-set. The prefix marks a notion of the host: an h-set is a type satisfying isSet, not a set of the set theory being modelled. The condition does not require every two elements of A to be equal. Instead, it requires the path type between any two elements to be a proposition. Elements of A may differ, and paths may connect some of them; but once the same source and target are fixed, any two such paths are equal. Distinctions may remain among elements, while no further distinguishable structure remains among their equality proofs.
• isProp→isSet: every proposition is an h-set. If A satisfies isProp, then it also satisfies isSet. This is an upward movement in homotopy level: it leaves A unchanged and derives the weaker condition that any two equality paths are equal from the stronger condition that any two elements are equal. It resembles the universe-level movement performed by Lift, since both let the same mathematical object meet a requirement at a higher level. They act on different axes, however. Lift changes the universe in which a type is presented and produces an equivalent record copy; isProp→isSet changes neither the type nor its universe, but derives one equality property from another.

open import Cubical.Foundations.Prelude public
  using ( isProp; isSet; isContr; isProp→isSet )

The universe of propositions

In cubical type theory, a proposition is a type satisfying isProp. This condition makes any two elements of the type equal, so the type retains only the logical information of whether a proof exists, without distinguishing different proofs. An element of the type proves the corresponding proposition; without such an element, the proposition has not yet been proved.

To keep a proposition together with the fact that it is a proposition, the Cubical library uses hProp ℓ. This is the type of all propositions at universe level ℓ: in other words, hProp ℓ is the universe of propositions at that level. A P : hProp ℓ has two components:

• The first component is the underlying type: the type expressing the proposition, namely the statement of the proposition itself.
• The second component is the certificate that this type satisfies isProp.

Thus P : hProp ℓ represents a proposition, but does not say that the proposition has already been proved. Its certificate says only that the first component is a proposition; it does not say that the first component has an element.

Two basic properties of the proposition universe recur later in the book:

• isSetHProp says that hProp ℓ is itself an h-set. Propositions may still differ, but equality proofs between propositions contain no distinguishable higher structure.
• isPropΠ says that propositions are closed under Π types. If every B x is a proposition, then (x : A) → B x is also a proposition. Universally quantifying a family of propositions therefore produces another proposition.

open import Cubical.Foundations.HLevels public
  using ( hProp; isSetHProp; isPropΠ )

The projection ⟨_⟩ extracts the statement of a proposition. For P : hProp ℓ, ⟨ P ⟩ is its first component; to prove the proposition expressed by P, we must construct an element of ⟨ P ⟩. The propositionhood certificate remains in the second component P .snd.

An object P packages the statement of a proposition together with its propositionhood certificate, so it can be passed as a function argument, returned as a function result or stored in a record field. When we need to state or prove the proposition, we extract the corresponding type through ⟨ P ⟩.

open import Cubical.Foundations.Structure public
  using ( ⟨_⟩ )

Logical operations

The proposition universe is closed under the usual logical operations. The two logical constants are truth and falsity. Truth ⊤ is the proposition that always has an element; the library supplies it polymorphically at every universe level.

open import Cubical.Functions.Logic public using ( ⊤ )

Falsity is built from a type representing impossibility. The empty type ⊥* has no elements and no constructors. If a branch of an argument nevertheless yields x : ⊥*, that branch's assumptions cannot hold, and x may be eliminated into any type:

This principle does not compute an element of A from actual data. It says that there is no constructor case to handle. The certificate isProp⊥* is immediate for the same reason: there are no two elements whose equality would have to be proved.

open import Cubical.Data.Empty public
  using ( ⊥*; isProp⊥* )

The false proposition ⊥ and the empty type express the same impossibility at two different levels of structure. The empty type is the underlying type of ⊥; pairing ⊥* with its propositionhood certificate isProp⊥* packages it as a proposition at any required universe level.

⊥ : ∀ {ℓ} → hProp ℓ
⊥ = ⊥* , isProp⊥*

For propositions P and Q, P ⊓ Q is their conjunction. Its certificates contain a proof of each proposition, and its universe level is the maximum of the two input levels.

open import Cubical.Functions.Logic public using ( _⊓_ )

P ⊔ Q is disjunction. A sum would remember which side supplied the proof, so the library applies propositional truncation and retains only that at least one side holds.

open import Cubical.Functions.Logic public using ( _⊔_ )

P ⇒ Q is implication. A certificate is a function taking every proof of P to a proof of Q; because Q is a proposition, this function type is a proposition as well.

open import Cubical.Functions.Logic public using ( _⇒_ )

¬ P is negation: it says that a proof of P would entail the false proposition ⊥. Its meaning therefore combines implication with falsity. Unlike binary implication, negation remains at the universe level of P.

open import Cubical.Functions.Logic public using ( ¬_ )

For a family of propositions P : A → hProp ℓ', ∀[ x ∶ A ] P x is universal quantification: a certificate supplies a proof of P x for every x : A. Writing the type after ∶ keeps the domain of quantification visible.

open import Cubical.Functions.Logic public using ( ∀[]-syntax; ∀[∶]-syntax )

∃[ x ] P x is existential quantification. A dependent pair would retain both a witness x : A and its proof of P x; propositional truncation forgets which witness was chosen and retains only that one exists.

open import Cubical.Functions.Logic public using ( ∃[]-syntax; ∃[∶]-syntax )

The next section considers propositions that vary with an object.

Classes and membership

Here class means a class in the sense of set theory, not a type in type theory. Throughout this book, class refers to the former and type to the latter. The two are closely related in the formalization, but they are not the same notion. A type determines which terms may be its elements; a class selects, by a property, the objects that satisfy it from a domain already given.

This collection of objects under consideration is the class's domain. When it is written A, the domain is a type A whose elements are all the objects currently being classified. Calling A a domain says only that a variable x : A may range over these objects; it does not equip A with membership, operations or any other structure. Later, when we construct a model of set theory, we add a set-theoretic membership relation to A. It then also becomes the carrier of the model, and its elements play the role of sets in that model.

A class over a domain A is represented by a function:

For each x : A, the proposition M x says that x has the property specified by the class M. Thus M does not send x to another object that is collected somewhere. It assigns a proposition to each x, and the objects satisfying that proposition are precisely the objects belonging to the class.

This explains why we can discuss classes before introducing sets. A class here is a predicate defined in the metatheory. It requires only a domain and the universe of propositions; it neither presupposes that sets have been defined in the object theory nor asserts that the class itself is a set. Once later chapters equip the domain with a set-theoretic structure, such classes can describe the sets in the model that satisfy a chosen property.

Class membership is written x ∈ᶜ M and read "x belongs to the class M". Its meaning is the proposition that M assigns to x:

To prove x ∈ᶜ M is therefore to construct a proof of ⟨ M x ⟩. The superscript ᶜ marks this as class membership. It distinguishes this host-level predicate from the membership relation between sets that later chapters interpret in a model of set theory: the former says whether an object satisfies a property, whereas the latter is a relation in the object language.

open import Cubical.Foundations.Powerset public
  using () renaming ( _∈_ to _∈ᶜ_ )

Natural numbers

The natural numbers ℕ form an inductive type generated by two constructors. The constructor zero is an element of ℕ; the constructor suc takes any n : ℕ to another element suc n : ℕ. The rules are

Every element of ℕ is generated from these constructors. Its induction principle accordingly has a case for zero and a step that passes from n to suc n.

To define a function from ℕ by recursion, it is therefore enough to give its value at zero and to give the value at suc n from the value already obtained at n.

open import Cubical.Data.Nat public
  using ( ℕ; zero; suc )

Finite indices

Fin is a family of types indexed by natural numbers. The type Fin zero has no constructors. At an index suc n, the constructor zero gives an element directly, while suc sends each element of Fin n to an element of Fin (suc n). These constructors obey the rules

Consequently Fin n has exactly n elements: none when n is zero, and one new element together with a copy of every element of Fin n when the index is suc n.

open import Cubical.Data.FinData public
  using ( Fin; zero; suc )

Vectors

A vector Vec A n is a list of elements of A whose length is part of its type. Its two constructors are expressed by the rules

The constructor [] produces an element of Vec A zero. Given a : A and v : Vec A n, the constructor _∷_ produces a ∷ v : Vec A (suc n). Thus the natural-number index is determined together with the vector. The function lookup has type Fin n → Vec A n → A; its shared index requires its two arguments to have the same n.

open import Cubical.Data.Vec public
  using ( Vec; []; _∷_; lookup )

The identity function

The identity function id accepts an element and returns that same element unchanged. Its type is:

id : ∀ {ℓ} {A : Type ℓ} → A → A

Here ℓ is an arbitrary universe level and A is an arbitrary type at that level. Since the signature imposes no further condition on A, id applies to an element of any type.

id x = x

The input x already has the result type A, so it can be returned directly. The definition neither changes x nor inspects how it was constructed.

Recap

This chapter introduced the host-level vocabulary used throughout the book:

• Type and Level describe type universes and their levels;
• Π types represent dependent functions, and Σ types represent dependent pairs;
• record types flatten nested Σ types through named fields and constructors;
• Lift moves types between universe levels;
• path types represent equality, and homotopy levels describe the equality structure retained by a type;
• hProp is the universe of propositions, and ⟨_⟩ extracts the statement of a proposition;
• truth and falsity, conjunction and disjunction, implication and negation, and universal and existential quantification provide the logical operations on the proposition universe;
• a class is a predicate valued in the universe of propositions, and _∈ᶜ_ expresses class membership;
• ℕ, Fin and Vec are respectively an inductive type and two families indexed by natural numbers;
• ⊥* is the empty type, and id is the identity function.

Together these notions form the basic formal language adopted in this book.