---
title: "Prelude"
module: Base.Prelude
lang: en
site: "Bedrock"
description: "Prelude"
stage: "Foundations"
reading_order: 2
canonical: https://bedrock.institute/en/Base.Prelude.html
html: Base.Prelude.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/Base/Prelude.lagda.md
prerequisites: []
routes: [common-foundations]
translations: [https://bedrock.institute/zh/Base.Prelude.md, https://bedrock.institute/ja/Base.Prelude.md]
agent_guide: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


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

# 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](index.html#reading-explorer), or use the [dependency graph](index.html#dependency-map) 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:

<div class="single-line-code" data-note="This reader-facing line is Agda-like pseudocode, not a formal Agda code block. It is closer to code than a traditional mathematical display, but it is not promised to compile on its own. In formal precision, it lies between a conventional mathematical display and complete Agda code."><code>Type ℓ : Type (ℓ-suc ℓ)</code></div>

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.

```agda
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:

```agda
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.

```agda
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:

<div class="single-line-code"><code>`lower (lift a) ≡ a`</code></div>

<div class="single-line-code"><code>`lift (lower b) ≡ b`</code></div>

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 <span class="prose-annotation-target">there is in general no way to move one down</span><aside class="prose-annotation-note">Propositions (types satisfying `isProp`) are the exception: the <a href="Base.Classical.html">Classical Boundary</a> chapter will show that excluded middle provides exactly the downward direction for them.</aside>.

```agda
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:

<div class="single-line-code"><code>`(x : A) → B x`</code></div>

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:

<div class="single-line-code"><code>`A → B`</code></div>

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:

<div class="single-line-code"><code>`Σ[ x ∶ A ] B x`</code></div>

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:

<div class="single-line-code"><code>`A × B = Σ[ _ ∶ A ] B`</code></div>

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.

```agda
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.

<!-- outcrop:agda-preview-lines=1 -->

```agda
infix 2 Σ[]-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
```

<figure class="book-diagram type-comparison" id="fig-pi-sigma" aria-describedby="fig-pi-sigma-caption">
<div class="type-comparison-panels">
<div class="diagram-panel type-comparison-panel">

$$f : \prod_{x:A} B(x)$$

$$\begin{array}{rcl}
x_1 : A & \longmapsto & f(x_1) : B(x_1) \\[8pt]
x_2 : A & \longmapsto & f(x_2) : B(x_2) \\[4pt]
\vdots & & \vdots
\end{array}$$

</div>
<div class="diagram-panel type-comparison-panel">

$$(a,b) : \sum_{x:A} B(x)$$

<div class="sigma-pair">
<svg viewBox="0 0 320 130" aria-hidden="true" focusable="false">
<path class="diagram-guide" d="M75 35 L154 98 M245 35 L166 98"/>
</svg>
<span class="sigma-component sigma-first">$a : A$</span>
<span class="sigma-component sigma-second">$b : B(a)$</span>
<span class="sigma-component sigma-result">$(a,b)$</span>
</div>

</div>
</div>
<figcaption id="fig-pi-sigma-caption">

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"

</figcaption>
</figure>

### 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

$$\frac{a:A}{\operatorname{inl}\,a:A\mathbin{\uplus}B}\qquad\frac{b:B}{\operatorname{inr}\,b:A\mathbin{\uplus}B}$$

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.

$$\mathsf{\uplus\text{-}rec}:(A\to C)\to(B\to C)\to A\mathbin{\uplus}B\to C$$

$$\mathsf{\uplus\text{-}rec}\;f\;g\;x=
\begin{cases}
f(a), & x=\operatorname{inl}\,a,\\
g(b), & x=\operatorname{inr}\,b
\end{cases}$$

```agda
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:

<div class="single-line-code"><code>`Σ[ a ∶ A ] Σ[ b ∶ B a ] C a b`</code></div>

Its elements have the shape:

<div class="single-line-code"><code>`(a , (b , c))`</code></div>

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:

<div class="single-line-code"><code>`mkR a b c`</code></div>

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](https://agda.readthedocs.io/en/v2.8.0/language/record-types.html) 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.

<figure class="book-diagram type-comparison path-figure" id="fig-path-operations" aria-describedby="fig-path-operations-caption">
<div class="path-operations">
<section class="diagram-panel path-operation">
<div class="path-stage" style="aspect-ratio:240/190">
<svg viewBox="0 0 240 190" aria-hidden="true" focusable="false">
<circle class="diagram-point" cx="120" cy="95" r="4"/>
</svg>
<span class="path-label" style="left:50%;top:31.5789%">$\operatorname{refl}_x$</span>
<span class="path-label" style="left:50%;top:62.6316%">$x$</span>
</div>
<div class="path-signature">

$$\begin{gathered}\operatorname{refl}_x : x\equiv x\end{gathered}$$

</div>

`refl` is a path from an element to itself and gives reflexivity of equality.

</section>
<section class="diagram-panel path-operation">
<div class="path-stage" style="aspect-ratio:240/190">
<svg viewBox="0 0 240 190" aria-hidden="true" focusable="false">
<path class="diagram-path" d="M35 55 Q120 0 205 55 M35 148 Q120 100 205 148"/><circle class="diagram-point" cx="35" cy="55" r="4"/><circle class="diagram-point" cx="205" cy="55" r="4"/><circle class="diagram-point" cx="35" cy="148" r="4"/><circle class="diagram-point" cx="205" cy="148" r="4"/>
</svg>
<span class="path-label" style="left:7.5%;top:28.9474%">$x$</span>
<span class="path-label" style="left:92.9167%;top:28.9474%">$y$</span>
<span class="path-label" style="left:50%;top:7.36842%">$p$</span>
<span class="path-label" style="left:7.5%;top:77.8947%">$y$</span>
<span class="path-label" style="left:92.9167%;top:77.8947%">$x$</span>
<span class="path-label" style="left:50%;top:87.3684%">$\operatorname{sym}\,p$</span>
<span class="path-label" style="left:50%;top:47.8947%">$\Big\downarrow\mathrlap{\;{\scriptstyle\operatorname{sym}}}$</span>
</div>
<div class="path-signature">

$$\begin{gathered}p:x\equiv y,\quad\operatorname{sym}\,p:y\equiv x\end{gathered}$$

</div>

`sym` reverses a path; a path from `x` to `y` thereby becomes a path from `y` to `x`.

</section>
<section class="diagram-panel path-operation">
<div class="path-stage" style="aspect-ratio:240/190">
<svg viewBox="0 0 240 190" aria-hidden="true" focusable="false">
<path class="diagram-path" d="M35 110 L120 45 L205 110 M35 110 Q120 179 205 110"/><circle class="diagram-point" cx="35" cy="110" r="4"/><circle class="diagram-point" cx="120" cy="45" r="4"/><circle class="diagram-point" cx="205" cy="110" r="4"/>
</svg>
<span class="path-label" style="left:7.5%;top:57.8947%">$x$</span>
<span class="path-label" style="left:50%;top:12.6316%">$y$</span>
<span class="path-label" style="left:92.9167%;top:57.8947%">$z$</span>
<span class="path-label" style="left:27.9167%;top:34.7368%">$p$</span>
<span class="path-label" style="left:73.3333%;top:34.7368%">$q$</span>
<span class="path-label" style="left:50%;top:87.8947%">$p\mathbin{\cdot}q$</span>
</div>
<div class="path-signature">

$$\begin{gathered}p:x\equiv y,\quad q:y\equiv z\\[3pt]p\mathbin{\cdot}q:x\equiv z\end{gathered}$$

</div>

`_∙_` 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`.

</section>
</div>
<figcaption id="fig-path-operations-caption">

Three basic path operations: reflexivity, reversal and composition

</figcaption>
</figure>

`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:

<div class="single-line-code"><code>`cong f : x ≡ y → f x ≡ f y`</code></div>

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.

<figure class="book-diagram type-comparison path-figure" id="fig-path-cong" aria-describedby="fig-path-cong-caption">
<div class="diagram-panel path-single">

$$f : A\to B,\qquad p:x\equiv y$$

<div class="path-stage path-cong-stage" style="aspect-ratio:360/240">
<svg viewBox="0 0 360 240" aria-hidden="true" focusable="false">
<path class="diagram-path" d="M55 60 Q180 5 305 60 M55 185 Q180 130 305 185"/>
<path class="diagram-map-line" d="M55 72 V165 M305 72 V165"/>
<path class="diagram-map-tip" d="M51 158 L55 165 L59 158 M301 158 L305 165 L309 158"/><circle class="diagram-point" cx="55" cy="60" r="4"/><circle class="diagram-point" cx="305" cy="60" r="4"/><circle class="diagram-point" cx="55" cy="185" r="4"/><circle class="diagram-point" cx="305" cy="185" r="4"/>
</svg>
<span class="path-label" style="left:15.2778%;top:15.4167%">$x:A$</span>
<span class="path-label" style="left:84.7222%;top:15.4167%">$y:A$</span>
<span class="path-label" style="left:50%;top:6.25%">$p$</span>
<span class="path-label" style="left:10.8333%;top:48.75%">$f$</span>
<span class="path-label" style="left:89.4444%;top:48.75%">$f$</span>
<span class="path-label" style="left:15.2778%;top:90%">$f(x):B$</span>
<span class="path-label" style="left:84.7222%;top:90%">$f(y):B$</span>
<span class="path-label" style="left:50%;top:56.25%">$\operatorname{cong}\,f\,p$</span>
</div>
</div>
<figcaption id="fig-path-cong-caption">

`cong`: a function sends a path to a path between the images of its endpoints

</figcaption>
</figure>

`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:

<div class="single-line-code"><code>`transport p : A → B`</code></div>

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.

<figure class="book-diagram type-comparison structural-figure" id="fig-type-transport" aria-describedby="fig-type-transport-caption">
<div class="diagram-panel type-comparison-panel">

$$p : A\equiv B$$

<div class="transport-scene">
<div class="diagram-space transport-fiber">

$$a : A$$

</div>
<div class="transport-edge">

$$\xmapsto{\;\operatorname{transport}\,p\;}$$

</div>
<div class="diagram-space transport-fiber">

$$b : B$$

</div>
<div class="transport-family" aria-hidden="true"></div>
<div class="transport-construction">

$$\Big\uparrow\mathrlap{\;{\scriptstyle\operatorname{transport}}}$$

</div>
<div class="transport-family" aria-hidden="true"></div>
<div class="diagram-space transport-base">

$$A : \operatorname{Type}_{\ell}$$

</div>
<div class="path-connection">
<svg viewBox="0 0 120 54" aria-hidden="true" focusable="false">
<path class="diagram-path" d="M8 35 H112"/>
<circle class="diagram-point" cx="8" cy="35" r="3.5"/>
<circle class="diagram-point" cx="112" cy="35" r="3.5"/>
</svg>
<span class="path-connection-label">$p$</span>
</div>
<div class="diagram-space transport-base">

$$B : \operatorname{Type}_{\ell}$$

</div>
</div>

$$b := \operatorname{transport}\,p\,a$$

</div>
<figcaption id="fig-type-transport-caption">

`transport`: a path between types gives a function between their elements

</figcaption>
</figure>

`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:

<div class="single-line-code"><code>`subst B p : B x → B y`</code></div>

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.

<figure class="book-diagram type-comparison structural-figure" id="fig-path-transport" aria-describedby="fig-path-transport-caption">
<div class="diagram-panel type-comparison-panel">

$$B : A \to \operatorname{Type}_{\ell}, \qquad p : x \equiv y$$

<div class="transport-scene">
<div class="diagram-space transport-fiber">

$$u : B(x)$$

</div>
<div class="transport-edge">

$$\xmapsto{\;\operatorname{subst}\,B\,p\;}$$

</div>
<div class="diagram-space transport-fiber">

$$v : B(y)$$

</div>
<div class="transport-family" aria-hidden="true"></div>
<div></div>
<div class="transport-family" aria-hidden="true"></div>
<div class="diagram-space transport-base">

$$x : A$$

</div>
<div class="path-connection">
<svg viewBox="0 0 120 54" aria-hidden="true" focusable="false">
<path class="diagram-path" d="M8 35 H112"/>
<circle class="diagram-point" cx="8" cy="35" r="3.5"/>
<circle class="diagram-point" cx="112" cy="35" r="3.5"/>
</svg>
<span class="path-connection-label">$p$</span>
</div>
<div class="diagram-space transport-base">

$$y : A$$

</div>
</div>

$$v := \operatorname{subst}\,B\,p\,u$$

</div>
<figcaption id="fig-path-transport-caption">

`subst`: a path between indices gives a function between the corresponding types

</figcaption>
</figure>

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

<figure class="book-diagram type-comparison path-figure" id="fig-subst-factorization" aria-describedby="fig-subst-factorization-caption">
<div class="diagram-panel path-single">

$$B : A \to \operatorname{Type}_{\ell}, \qquad x,y:A$$

<div class="path-stage subst-factorization" style="aspect-ratio:640/475">
<svg viewBox="0 0 640 475" aria-hidden="true" focusable="false">
<rect class="diagram-space-shape" x="15" y="15" width="235" height="135"/>
<rect class="diagram-space-shape" x="390" y="15" width="235" height="135"/>
<rect class="diagram-space-shape" x="15" y="295" width="610" height="155"/>
<path class="diagram-map-line" d="M262 87 H378 M152 163 L216 281 M488 163 L424 281"/>
<path class="diagram-map-tip" d="M371 83 L378 87 L371 91 M209 277 L216 281 L216 273 M424 273 L424 281 L431 277"/>
<path class="diagram-path" d="M140 390 Q320 350 500 390"/>
<circle class="diagram-point" cx="132.5" cy="93" r="4"/>
<circle class="diagram-point" cx="507.5" cy="93" r="4"/>
<circle class="diagram-point" cx="140" cy="390" r="4"/>
<circle class="diagram-point" cx="500" cy="390" r="4"/>
</svg>
<span class="path-label" style="left:20.7031%;top:9.05263%">$x\equiv y$</span>
<span class="path-label" style="left:79.2969%;top:9.05263%">$B(x)\equiv B(y)$</span>
<span class="path-label" style="left:50%;top:68%">$B(x)\to B(y)$</span>
<span class="path-label" style="left:20.7031%;top:25.0526%">$p$</span>
<span class="path-label" style="left:79.2969%;top:25.0526%">$\operatorname{cong}\,B\,p$</span>
<span class="path-label" style="left:50%;top:12.8421%">$\operatorname{cong}\,B$</span>
<span class="path-label" style="left:20.3125%;top:47.7895%">$\operatorname{subst}\,B$</span>
<span class="path-label" style="left:79.8438%;top:47.7895%">$\operatorname{transport}$</span>
<span class="path-label" style="left:21.875%;top:88.6316%">$\operatorname{subst}\,B\,p$</span>
<span class="path-label" style="left:78.125%;top:88.6316%">$\operatorname{transport}\,(\operatorname{cong}\,B\,p)$</span>
</div>

</div>
<figcaption id="fig-subst-factorization-caption">

For each input `p`, the two routes give functions of the same type `B x → B y`. The blue line represents a path between these functions. The proof is omitted here

</figcaption>
</figure>

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

<figure class="book-diagram type-comparison path-figure" id="fig-path-funext" aria-describedby="fig-path-funext-caption">
<div class="diagram-panel path-single">

$$f,g : A\to B$$

<div class="funext-scene">
<div class="diagram-space funext-family">

$$h : \prod_{x:A}\bigl(f(x)\equiv g(x)\bigr)$$

<div class="funext-samples">
<span class="funext-value">$f(x_1)$</span>
<div class="path-connection">
<svg viewBox="0 0 120 54" aria-hidden="true" focusable="false">
<path class="diagram-path" d="M8 35 H112"/>
<circle class="diagram-point" cx="8" cy="35" r="3.5"/>
<circle class="diagram-point" cx="112" cy="35" r="3.5"/>
</svg>
<span class="path-connection-label">$h(x_1)$</span>
</div>
<span class="funext-value">$g(x_1)$</span>
<span class="funext-value">$f(x_2)$</span>
<div class="path-connection">
<svg viewBox="0 0 120 54" aria-hidden="true" focusable="false">
<path class="diagram-path" d="M8 35 H112"/>
<circle class="diagram-point" cx="8" cy="35" r="3.5"/>
<circle class="diagram-point" cx="112" cy="35" r="3.5"/>
</svg>
<span class="path-connection-label">$h(x_2)$</span>
</div>
<span class="funext-value">$g(x_2)$</span>
<span class="funext-value">$\vdots$</span>
<div></div>
<span class="funext-value">$\vdots$</span>
</div>
</div>
<div class="funext-map">
<span class="funext-right">$\xmapsto{\operatorname{funExt}}$</span>
<span class="funext-down">$\Big\downarrow\mathrlap{\;{\scriptstyle\operatorname{funExt}}}$</span>
</div>
<div class="diagram-space funext-result">
<div class="path-stage" style="aspect-ratio:240/150">
<svg viewBox="0 0 240 150" aria-hidden="true" focusable="false">
<path class="diagram-path" d="M35 88 Q120 12 205 88"/><circle class="diagram-point" cx="35" cy="88" r="4"/><circle class="diagram-point" cx="205" cy="88" r="4"/>
</svg>
<span class="path-label" style="left:14.5833%;top:74.6667%">$f$</span>
<span class="path-label" style="left:85.4167%;top:74.6667%">$g$</span>
<span class="path-label" style="left:50%;top:20%">$\operatorname{funExt}\,h$</span>
</div>

$$\operatorname{funExt}\,h : f\equiv g$$

</div>
</div>
</div>
<figcaption id="fig-path-funext-caption">

`funExt`: paths at every input together give a path between functions

</figcaption>
</figure>

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](https://agda.readthedocs.io/en/v2.8.0/language/cubical.html). This section uses only the basic properties needed for the constructions that follow.

```agda
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.

<figure class="book-diagram type-comparison hlevel-comparison" id="fig-hlevel-distinction" aria-describedby="fig-hlevel-distinction-caption">
<div class="hlevel-panels">
<section class="diagram-panel hlevel-panel">

$$\operatorname{isContr}(A)$$

<div class="hlevel-assumptions">

$$c,x,y : A$$

</div>
<div class="hlevel-stage">
<svg viewBox="0 0 240 150" aria-hidden="true" focusable="false">
<path class="diagram-path" d="M55 75 L180 35 M55 75 L180 115"/>
<circle class="diagram-centre-ring" cx="55" cy="75" r="11"/>
<circle class="diagram-point" cx="55" cy="75" r="4"/>
<circle class="diagram-point" cx="180" cy="35" r="4"/>
<circle class="diagram-point" cx="180" cy="115" r="4"/>
</svg>
<span class="hlevel-label" style="left:22.9167%;top:66.6667%">$c$</span>
<span class="hlevel-label" style="left:75%;top:10%">$x$</span>
<span class="hlevel-label" style="left:75%;top:91.3333%">$y$</span>
<span class="hlevel-label" style="left:47.5%;top:26%">$h(x)$</span>
<span class="hlevel-label" style="left:47.5%;top:75.3333%">$h(y)$</span>
</div>
<div class="hlevel-definition">

$$c : A,\quad h : \prod_{x:A}(c\equiv x)$$

</div>

<p class="hlevel-note">A type with a chosen centre to which every element is joined by a path.</p>

</section>
<div class="hlevel-link">
<span class="hlevel-link-right">$\Longrightarrow$</span>
<span class="hlevel-link-down">$\Downarrow$</span>
</div>
<section class="diagram-panel hlevel-panel">

$$\operatorname{isProp}(A)$$

<div class="hlevel-assumptions">

$$x,y : A$$

</div>
<div class="hlevel-stage">
<svg viewBox="0 0 240 150" aria-hidden="true" focusable="false">
<path class="diagram-path" d="M40 85 Q120 10 200 85"/>
<circle class="diagram-point" cx="40" cy="85" r="4"/>
<circle class="diagram-point" cx="200" cy="85" r="4"/>
</svg>
<span class="hlevel-label" style="left:16.6667%;top:73.3333%">$x$</span>
<span class="hlevel-label" style="left:83.3333%;top:73.3333%">$y$</span>
<span class="hlevel-label" style="left:50%;top:19.3333%">$h(x,y)$</span>
</div>
<div class="hlevel-definition">

$$h : \prod_{x,y:A}(x\equiv y)$$

</div>

<p class="hlevel-note">A proposition may therefore have no proof or have a proof, but it cannot have two distinguishable proofs.</p>

</section>
<div class="hlevel-link">
<span class="hlevel-link-right">$\Longrightarrow$</span>
<span class="hlevel-link-down">$\Downarrow$</span>
</div>
<section class="diagram-panel hlevel-panel">

$$\operatorname{isSet}(A)$$

<div class="hlevel-assumptions">

$$x,y : A,\quad p,q : x\equiv y$$

</div>
<div class="hlevel-stage">
<svg viewBox="0 0 240 150" aria-hidden="true" focusable="false">
<path class="diagram-higher-path" d="M35 75 Q120 0 205 75 Q120 150 35 75 Z"/>
<path class="diagram-path" d="M35 75 Q120 0 205 75 M35 75 Q120 150 205 75"/>
<circle class="diagram-point" cx="35" cy="75" r="4"/>
<circle class="diagram-point" cx="205" cy="75" r="4"/>
</svg>
<span class="hlevel-label" style="left:6.66667%;top:50%">$x$</span>
<span class="hlevel-label" style="left:93.3333%;top:50%">$y$</span>
<span class="hlevel-label" style="left:50%;top:15.3333%">$p$</span>
<span class="hlevel-label" style="left:50%;top:85.3333%">$q$</span>
<span class="hlevel-label" style="left:50%;top:50%">$p\equiv q$</span>
</div>
<div class="hlevel-definition">

$$h : \prod_{x,y:A}\operatorname{isProp}(x\equiv y)$$

</div>

<p class="hlevel-note">A type whose equality types are propositions: elements may differ, but any two proofs that they are equal agree.</p>

</section>
</div>
<figcaption id="fig-hlevel-distinction-caption">

A chosen centre, equality of elements, equality of paths: these conditions become successively weaker

</figcaption>
</figure>

**`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.

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

<figure class="book-diagram type-comparison structural-figure" id="fig-universe-homotopy" aria-describedby="fig-universe-homotopy-caption">
<div class="diagram-panel type-comparison-panel level-scene">

<p class="type-comparison-title"><strong>Universe levels</strong></p>

<div class="diagram-space level-copy">

$$\operatorname{Lift}\,\ell_2\,A : \operatorname{Type}_{\ell\text{-max}(\ell_1,\ell_2)}$$

</div>
<div class="level-lift">

$$\Big\uparrow\mathrlap{\;{\scriptstyle\operatorname{Lift}\,\ell_2}}$$

</div>
<div class="diagram-space level-fixed">

$$A : \operatorname{Type}_{\ell_1}$$

<p class="type-comparison-title"><strong>Homotopy levels</strong></p>

<div class="level-properties">
<div class="level-property">

$$\operatorname{isContr}(A)$$

</div>
<div class="level-implication">

$$\Longrightarrow$$

</div>
<div class="level-property">

$$\operatorname{isProp}(A)$$

</div>
<div class="level-implication">

$$\Longrightarrow$$

</div>
<div class="level-property">

$$\operatorname{isSet}(A)$$

</div>
</div>
</div>
</div>
<figcaption id="fig-universe-homotopy-caption">

`Lift` changes the universe in which a type is presented and produces a record copy carrying the same data; `isProp→isSet` changes neither the type nor its universe, but derives one equality property from another

</figcaption>
</figure>

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

```agda
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:

<div class="single-line-code"><code>`Σ[ a ∶ A ] (f a ≡ b)`</code></div>

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

```agda
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.

<figure class="book-diagram path-figure fiber-general" id="fig-fiber-general" aria-describedby="fig-fiber-general-caption">
<div class="diagram-framed">

$$F_b=\sum_{a:A}\bigl(f(a)\equiv b\bigr)$$

<div class="path-stage fiber-fan-stage" style="aspect-ratio:680/460">
<svg viewBox="0 0 680 460" aria-hidden="true" focusable="false">
<rect class="diagram-space-shape" x="10" y="20" width="660" height="115"/>
<rect class="diagram-space-shape" x="10" y="185" width="660" height="250"/>
<g class="fiber-bundle" data-fiber="0" data-center-path="M120 390 C80 352 80 289 120 235">
<path class="diagram-map-line fiber-moving-map" d="M48 102 L48 225"/>
<path class="diagram-map-tip fiber-moving-tip" d="M44 218 L48 225 L52 218"/>
<path class="diagram-map-line fiber-moving-map" d="M96 102 L96 225"/>
<path class="diagram-map-tip fiber-moving-tip" d="M92 218 L96 225 L100 218"/>
<path class="diagram-map-line fiber-moving-map" d="M144 102 L144 225"/>
<path class="diagram-map-tip fiber-moving-tip" d="M140 218 L144 225 L148 218"/>
<path class="diagram-map-line fiber-moving-map" d="M192 102 L192 225"/>
<path class="diagram-map-tip fiber-moving-tip" d="M188 218 L192 225 L196 218"/>
<path class="diagram-path fiber-hair" d="M120 390 C33 358 33 292 48 235"/>
<path class="diagram-path fiber-hair" d="M120 390 C63 358 63 292 48 235"/>
<path class="diagram-path fiber-hair" d="M120 390 C81 358 81 292 96 235"/>
<path class="diagram-path fiber-hair" d="M120 390 C111 358 111 292 96 235"/>
<path class="diagram-path fiber-hair" d="M120 390 C129 358 129 292 144 235"/>
<path class="diagram-path fiber-hair" d="M120 390 C159 358 159 292 144 235"/>
<path class="diagram-path fiber-hair" d="M120 390 C177 358 177 292 192 235"/>
<path class="diagram-path fiber-hair" d="M120 390 C207 358 207 292 192 235"/>
<circle class="diagram-point fiber-domain-point" cx="48" cy="98" r="4"/>
<circle class="diagram-point fiber-image-point" cx="48" cy="235" r="4"/>
<circle class="diagram-point fiber-domain-point" cx="96" cy="98" r="4"/>
<circle class="diagram-point fiber-image-point" cx="96" cy="235" r="4"/>
<circle class="diagram-point fiber-domain-point" cx="144" cy="98" r="4"/>
<circle class="diagram-point fiber-image-point" cx="144" cy="235" r="4"/>
<circle class="diagram-point fiber-domain-point" cx="192" cy="98" r="4"/>
<circle class="diagram-point fiber-image-point" cx="192" cy="235" r="4"/>
<circle class="diagram-point fiber-base-point" cx="120" cy="390" r="5"/>
</g>
<g class="fiber-bundle" data-fiber="1" data-center-path="M340 390 C300 352 300 289 340 235">
<path class="diagram-map-line fiber-moving-map" d="M268 102 L268 225"/>
<path class="diagram-map-tip fiber-moving-tip" d="M264 218 L268 225 L272 218"/>
<path class="diagram-map-line fiber-moving-map" d="M316 102 L316 225"/>
<path class="diagram-map-tip fiber-moving-tip" d="M312 218 L316 225 L320 218"/>
<path class="diagram-map-line fiber-moving-map" d="M364 102 L364 225"/>
<path class="diagram-map-tip fiber-moving-tip" d="M360 218 L364 225 L368 218"/>
<path class="diagram-map-line fiber-moving-map" d="M412 102 L412 225"/>
<path class="diagram-map-tip fiber-moving-tip" d="M408 218 L412 225 L416 218"/>
<path class="diagram-path fiber-hair" d="M340 390 C253 358 253 292 268 235"/>
<path class="diagram-path fiber-hair" d="M340 390 C283 358 283 292 268 235"/>
<path class="diagram-path fiber-hair" d="M340 390 C301 358 301 292 316 235"/>
<path class="diagram-path fiber-hair" d="M340 390 C331 358 331 292 316 235"/>
<path class="diagram-path fiber-hair" d="M340 390 C349 358 349 292 364 235"/>
<path class="diagram-path fiber-hair" d="M340 390 C379 358 379 292 364 235"/>
<path class="diagram-path fiber-hair" d="M340 390 C397 358 397 292 412 235"/>
<path class="diagram-path fiber-hair" d="M340 390 C427 358 427 292 412 235"/>
<circle class="diagram-point fiber-domain-point" cx="268" cy="98" r="4"/>
<circle class="diagram-point fiber-image-point" cx="268" cy="235" r="4"/>
<circle class="diagram-point fiber-domain-point" cx="316" cy="98" r="4"/>
<circle class="diagram-point fiber-image-point" cx="316" cy="235" r="4"/>
<circle class="diagram-point fiber-domain-point" cx="364" cy="98" r="4"/>
<circle class="diagram-point fiber-image-point" cx="364" cy="235" r="4"/>
<circle class="diagram-point fiber-domain-point" cx="412" cy="98" r="4"/>
<circle class="diagram-point fiber-image-point" cx="412" cy="235" r="4"/>
<circle class="diagram-point fiber-base-point" cx="340" cy="390" r="5"/>
</g>
<g class="fiber-bundle" data-fiber="2" data-center-path="M560 390 C520 352 520 289 560 235">
<path class="diagram-map-line fiber-moving-map" d="M488 102 L488 225"/>
<path class="diagram-map-tip fiber-moving-tip" d="M484 218 L488 225 L492 218"/>
<path class="diagram-map-line fiber-moving-map" d="M536 102 L536 225"/>
<path class="diagram-map-tip fiber-moving-tip" d="M532 218 L536 225 L540 218"/>
<path class="diagram-map-line fiber-moving-map" d="M584 102 L584 225"/>
<path class="diagram-map-tip fiber-moving-tip" d="M580 218 L584 225 L588 218"/>
<path class="diagram-map-line fiber-moving-map" d="M632 102 L632 225"/>
<path class="diagram-map-tip fiber-moving-tip" d="M628 218 L632 225 L636 218"/>
<path class="diagram-path fiber-hair" d="M560 390 C473 358 473 292 488 235"/>
<path class="diagram-path fiber-hair" d="M560 390 C503 358 503 292 488 235"/>
<path class="diagram-path fiber-hair" d="M560 390 C521 358 521 292 536 235"/>
<path class="diagram-path fiber-hair" d="M560 390 C551 358 551 292 536 235"/>
<path class="diagram-path fiber-hair" d="M560 390 C569 358 569 292 584 235"/>
<path class="diagram-path fiber-hair" d="M560 390 C599 358 599 292 584 235"/>
<path class="diagram-path fiber-hair" d="M560 390 C617 358 617 292 632 235"/>
<path class="diagram-path fiber-hair" d="M560 390 C647 358 647 292 632 235"/>
<circle class="diagram-point fiber-domain-point" cx="488" cy="98" r="4"/>
<circle class="diagram-point fiber-image-point" cx="488" cy="235" r="4"/>
<circle class="diagram-point fiber-domain-point" cx="536" cy="98" r="4"/>
<circle class="diagram-point fiber-image-point" cx="536" cy="235" r="4"/>
<circle class="diagram-point fiber-domain-point" cx="584" cy="98" r="4"/>
<circle class="diagram-point fiber-image-point" cx="584" cy="235" r="4"/>
<circle class="diagram-point fiber-domain-point" cx="632" cy="98" r="4"/>
<circle class="diagram-point fiber-image-point" cx="632" cy="235" r="4"/>
<circle class="diagram-point fiber-base-point" cx="560" cy="390" r="5"/>
</g>
</svg>
<span class="path-label" style="left:7.5000%;top:8.0435%">$A$</span>
<span class="path-label" style="left:7.5000%;top:89.5652%">$B$</span>
<span class="path-label" style="left:53.9706%;top:32.3913%">$f$</span>
<span class="path-label fiber-sample-label" data-fiber="0" style="left:7.0588%;top:16.3043%">$a_{00}$</span>
<span class="path-label fiber-sample-label" data-fiber="0" style="left:14.1176%;top:16.3043%">$a_{01}$</span>
<span class="path-label fiber-sample-label" data-fiber="0" style="left:21.1765%;top:16.3043%">$a_{02}$</span>
<span class="path-label fiber-sample-label" data-fiber="0" style="left:28.2353%;top:16.3043%">$a_{03}$</span>
<span class="path-label fiber-center-label" aria-hidden="true" style="left:17.6471%;top:16.3043%">$a_0$</span>
<span class="path-label" style="left:17.6471%;top:90.2174%">$b_0$</span>
<span class="path-label fiber-sample-label" data-fiber="1" style="left:39.4118%;top:16.3043%">$a_{10}$</span>
<span class="path-label fiber-sample-label" data-fiber="1" style="left:46.4706%;top:16.3043%">$a_{11}$</span>
<span class="path-label fiber-sample-label" data-fiber="1" style="left:53.5294%;top:16.3043%">$a_{12}$</span>
<span class="path-label fiber-sample-label" data-fiber="1" style="left:60.5882%;top:16.3043%">$a_{13}$</span>
<span class="path-label fiber-center-label" aria-hidden="true" style="left:50.0000%;top:16.3043%">$a_1$</span>
<span class="path-label" style="left:50.0000%;top:90.2174%">$b_1$</span>
<span class="path-label fiber-sample-label" data-fiber="2" style="left:71.7647%;top:16.3043%">$a_{20}$</span>
<span class="path-label fiber-sample-label" data-fiber="2" style="left:78.8235%;top:16.3043%">$a_{21}$</span>
<span class="path-label fiber-sample-label" data-fiber="2" style="left:85.8824%;top:16.3043%">$a_{22}$</span>
<span class="path-label fiber-sample-label" data-fiber="2" style="left:92.9412%;top:16.3043%">$a_{23}$</span>
<span class="path-label fiber-center-label" aria-hidden="true" style="left:82.3529%;top:16.3043%">$a_2$</span>
<span class="path-label" style="left:82.3529%;top:90.2174%">$b_2$</span>
</div>
</div>
<figcaption id="fig-fiber-general-caption">

Click the pulsing fibres to contract; click again to expand. The paths in each tuft merge into a single path $p_i$ from $f(a_i)$ to $b_i$, while the candidate preimages merge into $a_i$. The coincidence depicts equality by paths. The condition for $f$ to be an equivalence is that every fibre is contractible

</figcaption>
</figure>

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.

```agda
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.

```agda
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

<div class="single-line-code"><code>`(x ≡ y) ≃ (f x ≡ f y)`</code></div>

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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

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

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

<figure class="book-diagram type-comparison path-figure" id="fig-proposition-and-proof" aria-describedby="fig-proposition-and-proof-caption">
<div class="diagram-framed type-comparison-panels proposition-proof-panels">
<section class="type-comparison-panel">

$$P=(\langle P\rangle,h_P):\operatorname{hProp}\,\ell$$

<div class="diagram-space">

$$\langle P\rangle:\operatorname{Type}_{\ell}$$

<div class="path-stage" style="aspect-ratio:280/140">

<span class="path-label" style="left:50%;top:50%">(no elements)</span>

</div>
</div>

$$h_P:\operatorname{isProp}\langle P\rangle$$

</section>
<section class="type-comparison-panel">

$$Q=(\langle Q\rangle,h_Q):\operatorname{hProp}\,\ell$$

<div class="diagram-space">

$$\langle Q\rangle:\operatorname{Type}_{\ell}$$

<div class="path-stage" style="aspect-ratio:280/140">
<svg viewBox="0 0 280 140" aria-hidden="true" focusable="false">
<path class="diagram-path" d="M60 90 Q140 10 220 90"/>
<circle class="diagram-point" cx="60" cy="90" r="4"/>
<circle class="diagram-point" cx="220" cy="90" r="4"/>
</svg>
<span class="path-label" style="left:21.4286%;top:83%">$p$</span>
<span class="path-label" style="left:78.5714%;top:83%">$q$</span>
<span class="path-label" style="left:50%;top:24%">$h_Q\,p\,q$</span>
</div>
</div>

$$h_Q:\operatorname{isProp}\langle Q\rangle$$

</section>
</div>
<figcaption id="fig-proposition-and-proof-caption">

The certificate $h_Q$ assigns a path to any two proofs; the curve shows its value $h_Q\,p\,q$ at $p$ and $q$

</figcaption>
</figure>

### 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

$$\frac{a:A}{|a|_1:\|A\|_1}\qquad\frac{x,y:\|A\|_1}{\mathsf{squash}_1(x,y):x=y}$$

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.

<figure class="book-diagram type-comparison path-figure" id="fig-truncation-witnesses" aria-describedby="fig-truncation-witnesses-caption">
<div class="diagram-framed">
<div class="path-stage diagram-compact-stage" style="aspect-ratio:420/340">
<svg viewBox="0 0 420 340" aria-hidden="true" focusable="false">
<rect class="diagram-space-shape" x="15" y="10" width="390" height="100"/>
<rect class="diagram-space-shape" x="15" y="205" width="390" height="125"/>
<path class="diagram-map-line" d="M95 83 L95 249"/>
<path class="diagram-map-tip" d="M91 242 L95 249 L99 242"/>
<path class="diagram-map-line" d="M325 83 L325 249"/>
<path class="diagram-map-tip" d="M321 242 L325 249 L329 242"/>
<path class="diagram-path" d="M95 253 Q210 350 325 253"/>
<circle class="diagram-point" cx="95" cy="79" r="4"/>
<circle class="diagram-point" cx="325" cy="79" r="4"/>
<circle class="diagram-point" cx="95" cy="253" r="4"/>
<circle class="diagram-point" cx="325" cy="253" r="4"/>
</svg>
<span class="path-label" style="left:50%;top:10.2941%">$A$</span>
<span class="path-label" style="left:22.619%;top:16.4706%">$a$</span>
<span class="path-label" style="left:77.381%;top:16.4706%">$b$</span>
<span class="path-label" style="left:50%;top:45.2941%">$\lvert{-}\rvert_1$</span>
<span class="path-label" style="left:50%;top:66.7647%">$\|A\|_1$</span>
<span class="path-label" style="left:13.0952%;top:74.4118%">$\lvert a\rvert_1$</span>
<span class="path-label" style="left:86.9048%;top:74.4118%">$\lvert b\rvert_1$</span>
<span class="path-label" style="left:50%;top:91.7647%">$\operatorname{squash}_1\,\lvert a\rvert_1\,\lvert b\rvert_1$</span>
</div>
</div>
<figcaption id="fig-truncation-witnesses-caption">

Given `a b : A`, their images in the truncation are joined by the displayed path. The two images need not be judgmentally equal; `squash₁` supplies their equality proof

</figcaption>
</figure>

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.

<div class="single-line-code"><code>`rec₁ : isProp P → (A → P) → ∥ A ∥₁ → P`</code></div>

<figure class="book-diagram type-comparison" id="fig-truncation-rec" aria-describedby="fig-truncation-rec-caption">
<div class="diagram-framed type-comparison-panel">

$$h : \operatorname{isProp}(P), \qquad f : A \to P$$

<div class="factorization-stage">
<svg viewBox="0 0 500 230" aria-hidden="true" focusable="false">
<path class="diagram-map-line" d="M88 50 H315"/>
<path class="diagram-map-tip" d="M306 45 L315 50 L306 55"/>
<path class="diagram-map-line" d="M358 76 V160"/>
<path class="diagram-map-tip" d="M353 151 L358 160 L363 151"/>
<path class="diagram-map-line" d="M72 74 L315 177"/>
<path class="diagram-map-tip" d="M303 179 L315 177 L308 167"/>
</svg>
<span class="factorization-label factorization-source">$A$</span>
<span class="factorization-label factorization-truncated">$\|A\|_1$</span>
<span class="factorization-label factorization-target">$P$</span>
<span class="factorization-label factorization-top-map">$|{-}|_1$</span>
<span class="factorization-label factorization-long-map">$f$</span>
<span class="factorization-label factorization-right-map">$\operatorname{rec}_1\,h\,f$</span>
</div>

$$\operatorname{rec}_1\,h\,f\,(|a|_1) = f(a) \qquad (a : A)$$

</div>
<figcaption id="fig-truncation-rec-caption">

`rec₁` factors `f : A → P` through the truncation, provided that `P` is a proposition. Both routes give `f a` on a representative `a`

</figcaption>
</figure>

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

<div class="single-line-code"><code>`map₁ : (A → B) → ∥ A ∥₁ → ∥ B ∥₁`</code></div>

```agda
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.

```agda
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.

```agda
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:

<div class="single-line-code"><code>`⊥₀-rec : ⊥₀ → A`</code></div>

<div class="single-line-code"><code>`⊥*-rec : ⊥* → A`</code></div>

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.

```agda
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.

```agda
⊥ : ∀ {ℓ} → 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Π`.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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.

```agda
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:

<div class="single-line-code"><code>`M : A → hProp ℓ`</code></div>

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`:

<div class="single-line-code"><code>`x ∈ᶜ M  :=  ⟨ M x ⟩`</code></div>

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.

```agda
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`.

```agda
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

$$\frac{a:A}{\mathsf{yes}\,a:\operatorname{Dec}(A)}\qquad\frac{n:A\to\bot_{0}}{\mathsf{no}\,n:\operatorname{Dec}(A)}$$

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.

```agda
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)`.

```agda
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

$$\frac{}{\mathsf{true}:\operatorname{Bool}}\qquad\frac{}{\mathsf{false}:\operatorname{Bool}}$$

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.

```agda
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

$$\frac{}{\mathsf{zero}:\mathbb{N}}\qquad\frac{n:\mathbb{N}}{\mathsf{suc}\,n:\mathbb{N}}$$

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.

$$\mathord{+}:\mathbb N\to\mathbb N\to\mathbb N$$

$$m+n=
\begin{cases}
n, & m=0,\\
\operatorname{suc}(m'+n), & m=\operatorname{suc}(m')
\end{cases}$$

```agda
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 <span class="prose-annotation-target">overloading</span><aside class="prose-annotation-note">The same written name can denote different constructors, much as 0 can denote zero in different number systems. When enough type information is available, Agda uses it to decide which constructor is meant.</aside>: 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

$$\frac{}{\mathsf{zero}:\operatorname{Fin}(\operatorname{suc}\,n)}\qquad\frac{i:\operatorname{Fin}(n)}{\mathsf{suc}\,i:\operatorname{Fin}(\operatorname{suc}\,n)}$$

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.

$$\operatorname{to\mathbb N}:\operatorname{Fin}(n)\to\mathbb N$$

$$\operatorname{to\mathbb N}(i)=
\begin{cases}
0, & i=\mathsf{zero},\\
\operatorname{suc}(\operatorname{to\mathbb N}(j)), & i=\mathsf{suc}\,j
\end{cases}$$

```agda
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

$$\frac{}{[]:A^{0}}\qquad\frac{a:A\quad v:A^{n}}{a∷v:A^{n^{+}}}$$

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

$$\operatorname{lookup}:\operatorname{Fin}(n)\to A^{n}\to A$$

$$\operatorname{lookup}(i,a\mathbin{∷}v)=
\begin{cases}
a, & i=\mathsf{zero},\\
\operatorname{lookup}(j,v), & i=\mathsf{suc}\,j
\end{cases}$$

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

<figure class="book-diagram type-comparison path-figure" id="fig-fin-vector-lookup" aria-describedby="fig-fin-vector-lookup-caption">
<div class="diagram-framed">
<div class="diagram-indexed">

$$v=a\mathbin{∷}b\mathbin{∷}c\mathbin{∷}[]:A^{3}$$

<div class="vector-slots"><span>$a$</span><span>$b$</span><span>$c$</span></div>

$$i\mapsto\operatorname{lookup}\,i\,v$$

<div class="path-stage diagram-compact-stage" style="aspect-ratio:420/310">
<svg viewBox="0 0 420 310" aria-hidden="true" focusable="false">
<rect class="diagram-space-shape" x="15" y="15" width="390" height="90"/>
<rect class="diagram-space-shape" x="15" y="205" width="390" height="90"/>
<path class="diagram-map-line" d="M80 85 L80 251"/>
<path class="diagram-map-tip" d="M76 244 L80 251 L84 244"/>
<path class="diagram-map-line" d="M210 85 L210 251"/>
<path class="diagram-map-tip" d="M206 244 L210 251 L214 244"/>
<path class="diagram-map-line" d="M340 85 L340 251"/>
<path class="diagram-map-tip" d="M336 244 L340 251 L344 244"/>
<circle class="diagram-point" cx="80" cy="81" r="4"/>
<circle class="diagram-point" cx="210" cy="81" r="4"/>
<circle class="diagram-point" cx="340" cy="81" r="4"/>
<circle class="diagram-point" cx="80" cy="255" r="4"/>
<circle class="diagram-point" cx="210" cy="255" r="4"/>
<circle class="diagram-point" cx="340" cy="255" r="4"/>
</svg>
<span class="path-label" style="left:50%;top:12.5806%">$\operatorname{Fin}(3)$</span>
<span class="path-label" style="left:19.0476%;top:19.6774%">$0$</span>
<span class="path-label" style="left:50%;top:19.6774%">$1$</span>
<span class="path-label" style="left:80.9524%;top:19.6774%">$2$</span>
<span class="path-label" style="left:9.52381%;top:73.2258%">$A$</span>
<span class="path-label" style="left:19.0476%;top:89.6774%">$a$</span>
<span class="path-label" style="left:50%;top:89.6774%">$b$</span>
<span class="path-label" style="left:80.9524%;top:89.6774%">$c$</span>
</div>
</div>
</div>
<figcaption id="fig-fin-vector-lookup-caption">

Each column follows one position through the vector, its index, and its lookup result. `Fin 3` provides exactly the three valid indices; the entries `a`, `b`, and `c` may coincide

</figcaption>
</figure>

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

$$\operatorname{map}:(A\to B)\to A^{n}\to B^{n}$$

$$\operatorname{map}(f,v)=
\begin{cases}
[], & v=[],\\
f(a)\mathbin{∷}\operatorname{map}(f,w), & v=a\mathbin{∷}w
\end{cases}$$

```agda
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.