---
title: "Small presentations of sets"
module: V.Presentation
lang: en
site: "Bedrock"
description: "Small presentations of sets"
stage: "Ordinals, injections and cardinals"
reading_order: 86
canonical: https://bedrock.institute/en/V.Presentation.html
html: V.Presentation.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Presentation.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, V.Hierarchy]
routes: [cardinal-tools]
translations: [https://bedrock.institute/zh/V.Presentation.md, https://bedrock.institute/ja/V.Presentation.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Small presentations of sets

Membership in a set of the cumulative hierarchy is index-based, but only in a weakened sense: the statement `x ∈ a` records that some index merely exists, and it lives one universe above the index types themselves. Doing set theory inside the hierarchy therefore asks for a way to pass between indices and membership proofs, and for a supply of indices that is small, concrete and unique. This chapter records the elementary lemmas that provide both. Every set comes with a canonical small presentation, an index type and an embedding whose image is the set, and the lemmas move back and forth between an index and a proof of membership, record the injectivity of the embedding, and restate canonical membership in the small relation. Later constructions rely on this package: reasoning about the elements of a set becomes reasoning about its indices.

The primitive notion of set is here already a notion of presentation. The constructor `sett` builds, from a small index type and a family into `V`, the set of values that family takes; membership `y ∈ sett X ix` holds merely when some index `i : X` satisfies `ix i ≡ y`; and the path constructor identifies two presentations with the same members. A presentation is thus built into every set, and the following lemmas make it usable in membership arguments. The universe parameter `ℓ` fixes how large the index types are allowed to be, and everything below is relative to that fixed level.

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

open import Base.Prelude

module V.Presentation {ℓ : Level} where

open import FOL.ZFStructure using ( module hPropStructure )
```

The same membership fact appears in two forms, and the lemmas below move between them. In the structure `𝒮ᵥ`, membership is read as the proposition `x ∈ˢ y`; a proof of it is a truncated existence statement, so no index comes with it. Alongside this, the small membership `a ∈ₛ b` is an equivalent proposition at level `ℓ` rather than `ℓ-suc ℓ`: its underlying type asks for an index of `b` together with a proof that the named element agrees with `a` under bisimulation. For each set `a` there is a chosen presentation: a small type `⟪ a ⟫` of indices, an embedding `⟪ a ⟫↪` into the hierarchy whose embedding property is recorded by `isEmb⟪ a ⟫↪`, and a proof `∈ₛ⟪ a ⟫↪ _` of small membership for each of its own indices. The presentation is canonical in a strong sense: a set cannot carry two different presentations of this kind. The lemmas below combine exactly these ingredients.

```agda
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )

open import Cubical.Functions.Embedding using ( isEmbedding→Inj )
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( _∈ₛ_; ∈∈ₛ; ⟪_⟫; ⟪_⟫↪; isEmb⟪_⟫↪; ∈ₛ⟪_⟫↪_; ∈-asFiber )

open hPropStructure 𝒮ᵥ
```

The first two lemmas convert between indices and membership proofs. The hinge is `∈∈ₛ`, which states that native and small membership agree, packaged as a pair of implications. The lemma `member` takes an index `m : ⟪ a ⟫` and applies the small-to-native implication to the certificate `∈ₛ⟪ a ⟫↪ m`, producing an inhabitant of `⟪ a ⟫↪ m ∈ˢ a`: an explicit proof that `a` contains the element named by `m`. The converse `fiber` starts from a proof of `x ∈ˢ a` and returns an actual index `m : ⟪ a ⟫` together with a path `⟪ a ⟫↪ m ≡ x`. This is not the truncated existence of an index but an explicitly constructed one. The step is legitimate because the embedding has proposition-valued fibers: the truncated membership statement may then be eliminated into the type of such fibers, and there the index can be read off.

```agda
member : (a : S) (m : ⟪ a ⟫) → ⟨ ⟪ a ⟫↪ m ∈ˢ a ⟩
member a m = ∈∈ₛ {a = ⟪ a ⟫↪ m} {b = a} .snd (∈ₛ⟪ a ⟫↪ m)

fiber : (a : S) {x : S} → ⟨ x ∈ˢ a ⟩ → Σ[ m ∈ ⟪ a ⟫ ] (⟪ a ⟫↪ m ≡ x)
fiber a {x} x∈ = ∈-asFiber {a = x} {b = a} x∈

↪-inj : {a : S} {m n : ⟪ a ⟫} → ⟪ a ⟫↪ m ≡ ⟪ a ⟫↪ n → m ≡ n
```

Two short facts complete the picture. The embedding property is exactly injectivity on indices: an embedding into an h-set has proposition-valued fibers, and the standard lemma `isEmbedding→Inj` turns that into the statement that equal values have equal indices, which `↪-inj` records. Finally `∈ₛ↪` states small membership directly: for every index `m`, the element `⟪ a ⟫↪ m` belongs to `a` in the small relation, with certificate `∈ₛ⟪ a ⟫↪ m`. Together with `member`, this shows that the canonical presentation is faithful in both the native and the small membership, and that its indexing map neither loses nor duplicates elements.

```agda
↪-inj {a} {m} {n} = isEmbedding→Inj isEmb⟪ a ⟫↪ m n

∈ₛ↪ : (a : S) (m : ⟪ a ⟫) → ⟨ ⟪ a ⟫↪ m ∈ₛ a ⟩
∈ₛ↪ a m = ∈ₛ⟪ a ⟫↪ m
```