Prelude

Every chapter of this book is literate Agda: the prose and the machine-checked code it explains live in the same file, commentary first, code right after. This opening chapter sets the table. It first lays down one discipline that fixes how the book is read (every name is traceable to its source), then re-exports, from the cubical library, the small host-language vocabulary the whole development stands on. Nothing is proved here; skim it now, and return when a symbol looks unfamiliar.

Traceable names

One machine-enforced convention is stated up front, because it changes how the book is read: every import lists exactly the names it takes. A chapter's import block therefore doubles as its precise list of prerequisites, and "where does this name come from" always has a visible answer on the page. The deliberate exception is the book's two designated hubs, this chapter and the next: they are opened wholesale, so a name not listed in any import comes from a hub.

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

module Base.Prelude where

The host vocabulary

The re-exports follow, one import at a time; before each, what it brings and why the book wants it.

The host organises its types into a tower of Tarski-style universes with explicit levels. Level is the type of the levels themselves, with its arithmetic

ℓ-zero, ℓ-suc, ℓ-max; Type ℓ is the universe at level ℓ, and it is itself a type one floor up, in Type (ℓ-suc ℓ). Whenever the book surveys a totality ("all sets", "all propositions"), this level bookkeeping is what says how large a totality is being surveyed.

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

_≡_ is the path type, the host's equality, and these are its everyday tools: refl (reflexivity), sym (symmetry), _∙_ (composition of paths), cong and cong₂ (every function respects equality), transport and subst (carrying an inhabitant along a path), and funExt (pointwise equal functions are equal).

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

The h-level predicates grade a type by how much equality structure it carries:

isProp (any two inhabitants are equal), isSet (equality itself is a proposition), isContr (exactly one inhabitant, up to a path), and

isProp→isSet connecting them. isContr is how this book says unique existence, a load-bearing choice explained in the Charter.

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

Lift makes a copy of a type at a higher universe level: the standard patch when something lives one floor too low. lift and lower shuttle elements between the type and its copy, and are mutually inverse; the asymmetry is at the level of types, where the traffic is one-way: a type can always be copied upward, but there is no general way to move one down. (The exception is propositions: the classical boundary chapter will show that excluded middle buys exactly the downward direction.)

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

hProp packages a type with a proof that it is a proposition: the type of truth values on the classical side of this book. The two accompanying facts deserve spelling out. isSetHProp says that hProp is itself a set: by univalence, a path between two propositions is the same thing as a bi-implication between them, and that is itself a proposition, so equality of propositions carries no structure beyond truth. This is the fact that qualifies hProp as a type of truth values in the next chapter (the isSetΩ field will demand exactly it).

isPropΠ says that propositions are closed under Π types: if B x is a proposition for every x, then (x : A) → B x is one too. It is the reason a universally quantified truth value is again a truth value.

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

⟨_⟩ (read "the underlying type of") projects the underlying type back out of an hProp; for P : hProp ℓ the proposition-hood proof is just

P .snd, and the book gives it no separate name.

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

One derived notation rides along. A class over a carrier A is a propositional predicate A → hProp ℓ, and x ∈ᶜ M (read "x belongs to the class M") is exactly ⟨ M x ⟩: the library's powerset membership under a marked name. The superscript ᶜ says class, keeping the notation apart from the object-level memberships to come, which denote sets rather than host-level predicates.

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

Dependent pairs: Σ with its Σ-syntax sugar, the plain product

_×_, the pairing _,_, and the projections fst and

snd. A Σ type is how the book bundles a thing with a property of it.

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

The natural numbers ℕ, with zero and suc. They index everything finite, first of all the number of free variables of a formula.

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

Vectors: Vec A n is a list of exactly n elements of A, built with [] and _∷_ and queried with lookup. Vectors are the raw material of variable environments, coming in Part 1.

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

Fin n is the type with exactly n elements; it will serve as the type of variables of an n-variable formula. Its constructors overload zero and

suc, and the type checker disambiguates.

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

Finally, the level-polymorphic empty type ⊥*, with isProp⊥*. Note the star: this is a host-layer type, at whatever level is needed, not the truth value ⊥ of the next chapter.

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

One definition of the book's own closes the chapter, and it is the smallest imaginable: the level-polymorphic identity function. It earns hub residence as the book's canonical constant interpretation: a constant standing for the very set it names is precisely id.

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

Recap

In scope from here on: universes, paths, h-levels, hProp with ⟨_⟩ and the class membership ∈ᶜ, pairs, ℕ, Vec, Fin,

⊥*, and the identity id. This chapter proves nothing, defines only id, and the logic symbols are deliberately absent: every notion of the book is introduced in the chapter where it first earns its keep, and the logic arrives with the truth algebra, next.