Prelude

In this book, set theory is the object theory and cubical type theory is the metatheory: we construct models of set theory, interpret their sentences and prove their properties within cubical type theory. Agda checks the constructions and proofs, while the Cubical library supplies their basic vocabulary. We call this working environment the host. A host type or function therefore belongs to the metatheory, not to the objects inside a set-theoretic model.

This chapter introduces that vocabulary through its mathematical meaning and use. There is no need to memorize every symbol: later chapters import these notions together from Base.Prelude, and you can return here whenever a definition needs refreshing.

Reading guide

Read the prose first; the code immediately below gives it a precise form. A definition with a type signature and defining equations automatically displays ∎ at its end.

Choose a route in the interactive contents, or use the dependency graph to see how chapters depend on one another. Each chapter's learning route lists its direct prerequisites and optional next chapters.

Hover over a marked name or expression to see its type; names in the popup can be explored in the same way.

Keywords and syntax symbols offer brief explanations and links to the official Agda manual, while terms lead back to where they are first introduced. Basic vocabulary leads first to its explanation in this chapter; to explore a library definition further, follow the visible Cubical imports to its source.

With these pointers in hand, we turn to the mathematical notions collected in this module.

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. The source expression ℓ-suc ℓ appears on this site as the compact ℓ-suc ℓ; hovering reveals the original code. 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 )

The identity function id gives a simple example of a definition that works uniformly at every universe level. For an arbitrary level ℓ and type A : Type ℓ, it accepts an element of A and returns that same element:

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

The level and the type are implicit arguments, so callers normally supply only the element. Since that element already has the result type A, the defining equation simply returns it without inspecting how it was constructed.

id x = x

Moving between 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 a record type that wraps an element of the original type A. Given a : A, the function lift produces lift a : Lift ℓ A. Conversely, given b : Lift ℓ A, 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 )

Basic types

The next four constructions organize the data used throughout the book. They let us describe outputs that vary with their inputs, package related data together, distinguish alternatives, and give names to the components of a larger package. Each construction will receive its precise name and form below.

Π 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.

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.

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 _,_. For a pair p, write p .fst and p .snd to extract its first and second components. After a single-letter name, the page displays these compactly as p .fst and p .snd; hovering reveals the original Agda spelling.

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

The code block below defines two binding forms for Σ types. It shows only the precedence declaration at first; readers who want the implementation can expand the rest. In Σ[ x ∶ A ] B x, the first component's type is explicit; in Σ[ x ] B x, Agda infers it. Both construct the same dependent-pair type.

infix  Σ[]-syntax Σ[∶]-syntax

Σ[]-syntax : ∀ {ℓ ℓ'} {A : Type ℓ}
  → (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
Σ[]-syntax {A = A} B = Σ A B

Σ[∶]-syntax : ∀ {ℓ ℓ'} {A : Type ℓ}
  → (B : A → Type ℓ') → Type (ℓ-max ℓ ℓ')
Σ[∶]-syntax = Σ[]-syntax

syntax Σ[∶]-syntax {A = A} (λ x → B) = Σ[ x ∶ A ] B
syntax Σ[]-syntax (λ x → B) = Σ[ x ] B

Sum types

The sum type A ⊎ B is an inductive type whose elements come in two forms. An element a : A gives inl a : A ⊎ B, while an element b : B gives inr b : A ⊎ B. These operations are its constructors, with rules

Thus a sum value records both which side was chosen and the element supplied on that side. Pattern matching can recover both pieces of information. The eliminator ⊎-rec handles the two constructors separately: one branch consumes an A, the other consumes a B, and both branches must produce the same target type.

open import Cubical.Data.Sum public
  using ( _⊎_; inl; inr )
  renaming ( rec to ⊎-rec )

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.

Equality and paths

In ordinary mathematics, $x = y$ asserts that two objects are equal. Here we write this assertion as x ≡ y: for two elements x and y of A, it is a type whose elements are proofs of their equality.

We reserve = for judgmental equality, where the type system identifies two expressions by its definition and computation rules, as in id x = x. In a defining equation, this = plays the role often written $\mathrel{:=}$; judgmental equality also includes the consequences of computation. It is a judgment made by the type system, not itself a type in which we must supply a proof. By contrast, x ≡ y is a type, and p : x ≡ y supplies a proof of equality, playing the role of a proved $x = y$ in ordinary mathematics. When x and y are judgmentally equal, the constant path refl introduced below proves x ≡ y; a path between them does not in general make them judgmentally equal.

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.

cong applies a function to a path. Given a function f : A → B and a path p : x ≡ y between its inputs, it constructs a path cong f p : f x ≡ f y between its outputs. Thus, fixing f gives a function from paths to paths:

Here both outputs lie in the same type B. The diagram shows how f sends the endpoints x and y to f x and f y, while cong f sends the path between them to a path between their images. cong₂ is the corresponding operation for a function of two inputs.

transport turns a path between types into a function between their elements. Given types A and B in the same universe and a path p : A ≡ B, it constructs a function transport p from A to B. Thus, fixing p gives a function from elements to elements:

Here the types themselves are the endpoints of the path. The diagram shows how transport turns this path into a function, which sends an element a : A to transport p a : B. The path p supplies the equality of types; transport p performs the movement of elements.

subst turns a path between inputs of a type family into a function between the corresponding types. Given a type family B : A → Type ℓ and a path p : x ≡ y, it constructs a function subst B p from B x to B y. Thus, fixing B and p gives a function from elements to elements:

Here the path joins the inputs x and y, while the elements being moved belong to B x and B y. The diagram shows how subst B p sends u : B x to subst B p u : B y. subst2 is the corresponding operation for a type family with two inputs: a path in each input moves data to the type at the new pair.

These three operations fit together in the following diagram. Each box represents a type, named at the top; the points inside represent its elements. Arrows between boxes are functions between those types. From x ≡ y to B x → B y, we can apply subst B directly, or first apply cong B and then transport.

funExt turns pointwise equality into equality of functions: if f x ≡ g x for every x, then f ≡ g.

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; subst2; 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. Conventionally, the h stands for homotopy. In this book, it can also serve as a reminder of the host: an h-set is a type satisfying isSet in the host, not a set of the set theory introduced later. 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.

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

The two axes in the figure are independent: lifting a type to another universe preserves its homotopy level. The function isOfHLevelLift transfers the corresponding certificate to Lift A. Its first argument specifies the homotopy level: 0 for contractibility, 1 for propositionhood and 2 for being an h-set. Thus, given h : isProp A, the term isOfHLevelLift 1 h proves isProp (Lift A); given h : isSet A, the term isOfHLevelLift 2 h proves isSet (Lift A). This number specifies an equality property, not the target universe of Lift.

open import Cubical.Foundations.HLevels public using ( isOfHLevelLift )

Type equivalence

Paths compare elements of a common type. To compare types themselves, possibly in different universes, we use A ≃ B. This says that a map preserves the information in their elements and paths. The condition is stronger than having functions in both directions: those functions must recover what they started with, in the sense made precise below.

For types A and B, A ≃ B is a dependent pair. Its first component is a map f : A → B; its second component is a certificate depending on f. To read this certificate, we first need the following definition.

For a fixed b : B, the fibre of f over b is the dependent pair type:

An element of the fibre has two components. The first is a candidate preimage a : A; the second is a path f a ≡ b witnessing that this candidate really maps to b. An empty fibre means that b has no preimage. Elements of a fibre that cannot be identified by a path represent substantively different ways to return from b to A.

open import Cubical.Foundations.Equiv public using ( _≃_ )

The animation assumes that every fibre is contractible: there is a centre and a family of paths connecting each dependent pair in the fibre to that centre.

This notion should be distinguished from an isomorphism, which explicitly presents maps f : A → B and g : B → A and the two round-trip laws: paths g (f a) ≡ a for every a : A and f (g b) ≡ b for every b : B. The constructor uses the order iso f g s r, where s : (b : B) → f (g b) ≡ b and r : (a : A) → g (f a) ≡ a. The two notions are related as follows: iso packages those data as Iso A B, and isoToEquiv converts the result into A ≃ B. Explicit maps make isomorphisms convenient for constructing examples, while the cubical library uses equivalences as the common interface for transporting type structure.

open import Cubical.Foundations.Isomorphism public using ( Iso; iso; isoToEquiv )

Given e : A ≃ B, we can use the equivalence in either direction. The function equivFun e : A → B is its first component; invEq e : B → A recovers a preimage using the contractibility certificate. The two composites return their inputs up to paths. In particular, when A and B are propositions, these functions convert a proof on either side into a proof on the other.

open import Cubical.Foundations.Equiv public using ( equivFun; invEq )

An equivalence also preserves the paths between its elements. Write f = equivFun e. For x y : A, congEquiv e gives the equivalence

Its forward map is cong f: it applies the function to a path. Its inverse, invEq (congEquiv e), recovers a path between the original elements from a path between their images. Thus an equivalence lets us both send paths forward and recover them; cong for an arbitrary function only supplies the forward operation.

open import Cubical.Foundations.Equiv.Properties public using ( congEquiv )

Finally, equivalence preserves homotopy levels, just as Lift does. If h : isProp A, then isOfHLevelRespectEquiv 1 e h proves isProp B; if h : isSet A, then isOfHLevelRespectEquiv 2 e h proves isSet B. The index 0 likewise transfers contractibility. Here the certificate follows the equivalence from A to B, even when their universes differ.

open import Cubical.Foundations.HLevels public using ( isOfHLevelRespectEquiv )

We can therefore construct a convenient presentation with Iso, convert it with isoToEquiv, and use the resulting equivalence to move elements, paths and homotopy-level certificates.

Propositions

The next constructions isolate types that express statements rather than arbitrary data. We first characterize propositionhood, then form the universe of propositions, control existential information by truncation, assemble propositions with logical operations, and finally use proposition-valued predicates to describe classes.

Propositionhood

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.

Four closure principles recur later in the book:

• 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.
• isProp→ is the non-dependent specialization of isPropΠ. If B is a proposition, then the function type A → B is a proposition, with no propositionhood requirement on its source type A.
• isPropΣ handles dependent pairs. If A and every B x are propositions, then Σ[ x ∶ A ] B x is also a proposition.
• isProp× is the non-dependent specialization of isPropΣ. If A and B are propositions, then a pair consisting of a proof of each is again a proposition: any two such pairs are equal componentwise.

open import Cubical.Foundations.HLevels public
  using ( isPropΠ; isProp→; isPropΣ; isProp× )

Propositionhood also controls equality between proof-carrying dependent pairs. If every possible second component is a proposition, Σ≡Prop says that two such pairs are equal as soon as their first components are equal. Their certificates contain no further distinguishable choice, so equality of the underlying objects determines equality of the complete packages.

open import Cubical.Data.Sigma public using ( Σ≡Prop )

The universe of propositions

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.

The proposition universe is itself an h-set. isSetHProp allows propositions to differ, while ensuring that equality proofs between propositions contain no distinguishable higher structure.

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

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 notation ⟨ P ⟩isProp extracts the certificate that this underlying type satisfies isProp.

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 ⟩. The examples below show an empty underlying type and an inhabited one: both carry a propositionhood certificate.

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

⟨_⟩isProp : ∀ {ℓ} (P : hProp ℓ) → isProp ⟨ P ⟩
⟨ P ⟩isProp = P .snd

Propositional truncation

A type may contain more information than a proposition should retain. The propositional truncation ∥ A ∥₁ records that A has an element while deliberately forgetting which element it is. It is a higher inductive type, abbreviated HIT: its generators include not only points but also paths between points. The point constructor ∣_∣₁ sends each a : A to ∣ a ∣₁ : ∥ A ∥₁; the path constructor squash₁ identifies every two elements of the truncation. Its defining rules are

Consequently ∥ A ∥₁ is always a proposition, even when A carries distinguishable data.

By the mere existence of an element of A, we mean an element of ∥ A ∥₁, without specifying an element of A. Likewise, saying that an x : A satisfying P x merely exists means that ∥ Σ[ x ∶ A ] P x ∥₁ has an element. When P x is a proposition, this truncated type underlies the logical existential quantification ∃[ x ∶ A ] P x introduced below.

There are two standard ways to use a truncated value. The recursor rec₁ may expose a representative only while constructing a target already known to be a proposition; this restriction prevents a hidden choice from escaping as ordinary data.

The map map₁ applies a function A → B under the truncation and returns another truncated value.

import Cubical.HITs.PropositionalTruncation as PT
open PT public
  using ( ∥_∥₁; ∣_∣₁; squash₁ )
  renaming ( rec to rec₁; map to map₁ )

Logical operations

The proposition universe is closed under the usual logical operations. The following subsections construct these operations from the type formers already introduced and explain when propositional truncation is required.

Truth

The unit type represents trivial evidence. Its zero-level form in Type₀ is written ⊤₀, and ⊤* {ℓ} is its lift to an arbitrary universe level ℓ. Their unique elements are written tt and tt*. Since any two elements of a unit type are equal, isProp⊤* certifies that ⊤* is a proposition.

open import Cubical.Data.Unit public
  using ( tt; tt* )
  renaming ( Unit to ⊤₀; Unit* to ⊤*; isPropUnit* to isProp⊤* )

The true proposition ⊤ and the unit type express the same trivial truth at two different levels of structure. The unit type is the underlying type of ⊤; pairing ⊤* with its propositionhood certificate isProp⊤* packages it as a proposition at any required universe level. Thus truth lies in the proposition universe because its underlying unit type is inhabited and all its elements are equal.

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

Falsity

The empty type represents impossibility. Its zero-level form in Type₀ is written ⊥₀, and ⊥* {ℓ} is its lift to an arbitrary universe level ℓ. Neither has elements or constructors. If a branch of an argument nevertheless yields x : ⊥*, that branch's assumptions cannot hold, and x may be eliminated into any type:

The eliminators ⊥₀-rec and ⊥*-rec do not compute an element of A from actual data. They say that there is no constructor case to handle. The certificates isProp⊥ for ⊥₀ and isProp⊥* for ⊥* are 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⊥* )
  renaming ( ⊥ to ⊥₀; rec to ⊥₀-rec; rec* to ⊥*-rec )

open import Cubical.Data.Empty.Properties 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. Thus falsity lies in the proposition universe because its underlying empty type has no elements, so all its elements are vacuously equal.

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

Universal quantification

For a family of propositions P : A → hProp ℓ', universal quantification is the Π type introduced above: a proof is a dependent function that supplies a proof of P x for every x : A. The form ∀[ x ] P x lets Agda infer the type of x, while ∀[ x ∶ A ] P x displays it explicitly. No propositional truncation is needed. Each P x is a proposition, so any two dependent functions agree pointwise and are equal by function extensionality; this is the closure property isPropΠ.

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

Implication

P ⇒ Q is implication. Its evidence is a function taking each proof of P to a proof of Q, so implication is the non-dependent special case of the universal quantification just introduced. No propositional truncation is needed: because Q is a proposition, any two such functions agree at every input, and function extensionality makes the functions equal. Thus the function type itself is already a proposition, regardless of how many proofs P has.

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

Negation

Negation is the special implication ¬ P from P to the empty type underlying falsity: it says that any proof of P would yield an impossibility. Unlike general binary implication, negation remains at the universe level of P. Its closure under propositionhood can be read directly from two earlier certificates. First, isProp⊥ says that the zero-level empty target type is a proposition. Then isProp→ says that a function type is a proposition whenever its target type is, without requiring its source type to be a proposition. Applying it to isProp⊥ therefore proves that the type underlying ¬ P is a proposition. No propositional truncation is needed.

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

Propositional extensionality

Mutual implication between propositions is called logical equivalence. Propositional extensionality turns it into equality inside the proposition universe. Mutual implication packages two instances of the implication introduced above: one function from P to Q and one from Q to P. This package uses a product, the non-dependent case of a Σ type. ⇔toPath turns the two functions into a path P ≡ Q. No propositional truncation is involved: since P and Q are propositions, their individual proofs carry no distinguishable data, so the two implications already express everything needed for their equality. The resulting path type is itself a proposition because hProp is a set.

open import Cubical.Functions.Logic public using ( ⇔toPath )

Existential quantification

Existential quantification begins with the Σ type introduced above. Its dependent pairs contain both a witness x : A and a proof of P x. Even though every P x is a proposition, the witnesses in A may be distinguishable, so this Σ type need not be a proposition. The notation therefore applies propositional truncation: ∃[ x ] P x lets Agda infer the type of the witness, while ∃[ x ∶ A ] P x states it explicitly, and both forget which witness was chosen while retaining that some witness exists. Existential quantification therefore needs truncation because its untruncated evidence contains an arbitrary element of A, whereas the preceding universal quantification and implication do not.

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

Conjunction

The corresponding non-dependent case of the Σ construction is conjunction. For propositions P and Q, a proof of P ⊓ Q is a pair containing one proof of P and one proof of Q. Unlike the general existential quantification above, no propositional truncation is needed. Since each component is already a proposition, any two first components are equal and any two second components are equal, so the two pairs are equal; this is exactly the closure property isProp×. The conjunction therefore remains a proposition while retaining both of its proofs, and its universe level is the maximum of the two input levels.

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

Disjunction

The other binary operation is disjunction, P ⊔ Q. Before truncation, its evidence has the sum type introduced above: inl p records a proof p of P, while inr q records a proof q of Q. Even when P and Q are propositions, this sum need not be a proposition. If both sides hold, its left and right constructors still record distinguishable choices. Disjunction therefore applies propositional truncation to the sum. It forgets the chosen constructor and the proof carried by it, retaining only that at least one side holds. The truncation is what makes disjunction proposition-valued.

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

Classes and membership

A proposition that depends on an object can select exactly those objects for which it holds. In set theory, a collection determined in this way by a property is called a class.

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 an already specified type.

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 _∈ᶜ_ )

A class also determines a host type of its members, Σ[ x ∶ A ] (x ∈ᶜ M). Its elements pair an object x with evidence that it satisfies M; this is not a set representing M inside the object theory. If A is an h-set, the Cubical lemma isSetΣSndProp shows that this Σ-type is also an h-set, since the underlying type of each M x is a proposition. We expose the lemma as isSetClass.

open import Cubical.Foundations.HLevels public
  using () renaming ( isSetΣSndProp to isSetClass )

More inductive types

The remaining basic data types illustrate several forms of induction. A decision records evidence for one of two answers, Booleans provide two bare labels, natural numbers support recursion, and the indexed families Fin and Vec record numerical bounds in their types.

Decidability

To decide a type A is to give evidence that determines whether A has an inhabitant. A positive answer carries an inhabitant a : A; a negative answer carries a refutation n : A → ⊥₀, showing that any proposed inhabitant would lead to impossibility. The inductive type Dec A packages exactly these two answers. Its constructors obey the rules

Thus yes a records the positive answer together with its witness, while no n records the negative answer together with its refutation. Unlike propositional disjunction, Dec A is not truncated: a program may inspect which constructor was returned and use the evidence it carries. Constructing a decision for a particular finite comparison can be entirely constructive. The classical principle introduced in a later chapter is stronger because it supplies such a decision uniformly for every proposition at a chosen universe level.

For an arbitrary type A, Dec A need not be a proposition: two positive decisions can carry distinguishable inhabitants of A. If A is a proposition, however, isPropDec proves that its decisions are propositions too. Positive witnesses are then equal, negative answers are equal because refutations are proposition-valued, and a positive answer cannot coexist with a negative one.

open import Cubical.Relation.Nullary public
  using ( Dec; yes; no; isPropDec )

An existing decision can also be converted. To obtain Dec B from Dec A, we need a function f : A → B for the positive case and a function g : (A → ⊥₀) → (B → ⊥₀) for the negative case. Then mapDec f g performs the conversion: it sends yes a to yes (f a) and no n to no (g n). The positive function alone is insufficient, since a refutation of A does not in general refute B. A function r : B → A supplies the missing negative conversion as λ n b → n (r b).

open import Cubical.Relation.Nullary public using ( mapDec )

Booleans

The inductive type Bool has exactly two constructors, true and false. Unlike the constructors of a general sum, neither constructor carries further data. Their construction rules are

Consequently, defining a function out of Bool amounts to giving one result for true and one for false. Booleans are useful when a computation must return one of two distinguishable labels, as in a finite test or a mask. They should not be confused with the propositions truth and falsity introduced above: true and false are two values of the ordinary data type Bool, rather than proofs of propositions.

open import Cubical.Data.Bool public using ( Bool; true; false )

Natural numbers

The natural numbers ℕ form an inductive type with the original Agda constructors zero : ℕ and suc : ℕ → ℕ. The first gives a natural number directly; the second takes n : ℕ to suc n : ℕ. Their 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.

Agda also lets us write the closed ℕ values zero, suc zero and suc (suc zero) as the numeric literals 0, 1 and 2, respectively. With a variable, the raw expression suc (suc (suc n)) can instead appear here in compact form as suc (suc (suc n)); hovering over that notation still reveals the original Agda code.

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.

Addition _+_ combines two natural-number sizes and is used throughout the syntax chapters to compute the number of available variables after contexts are extended or combined.

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

Finite indices

Fin is a family of inductive types indexed by natural numbers. Agda allows constructor overloading: the constructors of Fin share the names zero and suc with those of ℕ. 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.

For elements of Fin 3, the original expressions zero, suc zero and suc (suc zero) appear in compact form as zero, suc zero and suc (suc zero). Hovering shows the original constructor expression and its explicitly marked type.

The function toℕ forgets the bound and reads a finite index as a natural number. This forgetful map preserves the numerical position while its result no longer carries the bound in its type.

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

Vectors

A vector Vec A n is a list of elements of A whose length is part of its type. When both parameters are single letters, the website displays this type as Vec A n, read as the power of A with exponent n. This is only a display convention: hovering or tapping reveals the original Agda code. 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.

For a short vector written out in full, the website displays a ∷ b ∷ c ∷ [] as a ∷ b ∷ c ∷ []. Hovering or tapping this bracket notation reveals the original constructors and the type. An expression such as a ∷ v, whose tail is not written out, retains its original form.

These indices make the standard vector operations carry useful guarantees. An out-of-range lookup cannot be stated because its index must inhabit Fin n.

The figure below uses finite indices to select positions in a length-three vector.

The function map applies one function to every entry without changing the length.

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

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, Σ types represent dependent pairs, and sum types distinguish values constructed from either of two input types;
• record types flatten nested Σ types through named fields and constructors;
• Lift moves types between universe levels;
• path types represent equality; transport, subst and its two-argument generalization subst2 move data along paths;
• homotopy levels describe the equality structure retained by a type, while propositionhood is preserved by Π types, Σ types and products; Σ≡Prop reduces equality of proof-carrying dependent pairs to equality of their first components;
• type equivalence A ≃ B means that every fibre of a map is contractible; Iso constructs it from explicit maps and round-trip laws, and the equivalence carries elements, paths and homotopy levels between types;
• hProp is the universe of propositions, isSetHProp describes its equality structure, and ⟨_⟩ extracts the statement of a proposition;
• propositional truncation ∥ A ∥₁ retains whether A is inhabited while forgetting its particular witness; rec₁ eliminates it into propositions and map₁ maps it to another truncation;
• truth and falsity, conjunction and disjunction, implication and negation, and universal and existential quantification provide the logical operations on the proposition universe; propositional extensionality turns implications in both directions into equality of propositions;
• a class is a predicate valued in the universe of propositions, and _∈ᶜ_ expresses class membership;
• Dec A retains either an inhabitant of A or a refutation, while uniform decisions for arbitrary propositions require an additional principle;
• Bool is the two-element data type whose constructors true and false provide distinguishable computational labels;
• ℕ supplies natural numbers and addition, Fin n supplies indices below n, and Vec A n supplies length-indexed sequences with bounded lookup and length-preserving map;

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