---
title: "Coding inside the cumulative hierarchy"
module: V.Coding
lang: en
site: "Bedrock"
description: "Coding inside the cumulative hierarchy"
stage: "The ambient hierarchy"
reading_order: 23
canonical: https://bedrock.institute/en/V.Coding.html
html: V.Coding.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/V/Coding.lagda.md
prerequisites: [Base.Prelude, FOL.ZFStructure, FOL.Coding, V.Hierarchy, V.Model]
routes: [ambient-model]
translations: [https://bedrock.institute/zh/V.Coding.md, https://bedrock.institute/ja/V.Coding.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Coding inside the cumulative hierarchy

The generic coding construction of FOL.Coding needs exactly two injective operations on some carrier: an injective pairing, and an injective map from natural numbers. To code syntax over the cumulative hierarchy, both must be found among sets, and the hierarchy supplies them. For the naturals, its own von Neumann numerals serve. A smaller numeral belongs to a larger one, since each numeral sits inside its successor, and no set belongs to itself; so distinct indices, compared by the trichotomy on natural numbers, give distinct sets. For pairing, the Kuratowski encoding serves: the pair of `a` and `b` is the set whose members are the singleton `⁅ a ⁆s` and the unordered pair `⁅ a , b ⁆`, so the first component is recoverable as the common element and the second as the one that may differ.

Both arguments face one constraint from the type theory. Small membership in a hierarchy set is propositionally truncated, so a case analysis on it may eliminate only into propositions. Equality in `V` is propositional because `V` is an h-set, and the path propositions built from such equalities are exactly the targets the reasoning below needs. Working at that level of discipline, every step stays proposition-valued and no witness is ever extracted from a truncation.

The chapter is stated at a fixed universe level `ℓ`: the hierarchy's own structure `𝒮ᵥ` is the carrier that the codes will live over, and its membership relation is the one being analyzed. The eventual coding instance uses truth values in `hProp (ℓ-suc ℓ)`, one level up.

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

open import Base.Prelude

module V.Coding {ℓ : Level} where

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

The numeral argument rests on two membership facts about successors in the hierarchy: a set always belongs to its own successor, and a member of a set belongs to that set's successor. Applied to the numerals, the first says `# n ∈ # (suc n)`, and the second says a member of `# n` survives into `# (suc n)`. The order on natural numbers then decides which numeral is smaller, with the trichotomy `m ≟ n` supplying the three cases the injectivity proof will separate.

```agda
import FOL.Coding
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; ∈-irrefl )
open import V.Model {ℓ} using ( self∈sucV; ∈sucV-inl )

open import Cubical.Data.Nat.Order using ( _<_; <-split; ¬-<-zero; _≟_; lt; eq; gt )
import Cubical.Data.Empty as Empty
```

Here is the elimination restriction in its precise form. The small membership statement `⟨ x ∈ₛ s ⟩` is a proposition by truncation, so when a hypothesis gives a truncated disjunction of memberships, the eliminator must target a proposition. Because `V` is an h-set, certified by `setIsSet`, the path type `x ≡ y` between hierarchy sets is propositional; every case split below may therefore eliminate into such an equality path.

```agda
import Cubical.Data.Sum as Sum
open Sum using ( _⊎_; inl; inr )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( setIsSet )
```

The two set constructions the Kuratowski code needs come with their membership classifications attached. For an unordered pair `⁅ a , b ⁆`, the classification `pairing-ax` says that `x` belongs to it merely when `x ≡ a` or `x ≡ b`, in the truncated sense. The singleton `⁅ a ⁆s` carries the analogous classification through the singleton package, and `SetPackage.classification` extracts these records. Every argument about the codes below is therefore stated as membership reasoning rather than as unfolding of nested braces.

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties using ( _∈ₛ_ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ⁅_,_⁆; pairing-ax; ⁅_⁆s; SingletonPackage; module InfinitySet )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( SetPackage )  -- lint-agda: keep (used qualified: SetPackage.classification)
```

The numeral `# n`, written using `#_`, is the von Neumann ordinal representing the natural number `n` inside the hierarchy. With the two alphabets in hand, the direct operations on `hProp (ℓ-suc ℓ)` and the structure `𝒮ᵥ` are what the coding instance at the end will interpret the encoded syntax in; the injectivity proofs of this chapter use only the successor facts and the classifications just described.

```agda
open InfinitySet using ( #_ )

open hPropStructure 𝒮ᵥ
```

## Numerals are distinct

The first alphabet is the numeral map, and its injectivity splits into two statements. Monotonicity says a smaller numeral belongs to a larger one. The induction is on the *larger* index, so that each inductive step is the syntactic successor and no arithmetic on indices appears. The step case divides by the trichotomy on natural numbers into a strictly smaller index and an equal one, each settled by a successor membership fact; the base case is vacuous. Injectivity then follows: if the codes of two distinct indices agreed, monotonicity would place a numeral inside itself, which membership irreflexivity forbids.

The stepping stone `#⊆suc` says that any member of `# n` is also a member of the next numeral; it is exactly the successor fact that a member of a set belongs to that set's successor. In the base case of `#mono` there is nothing to prove, since no index is strictly below zero and the hypothesis `m < 0` is refuted outright.

```agda
#⊆suc : (n : ℕ) {x : S} → ⟨ x ∈ˢ (# n) ⟩ → ⟨ x ∈ˢ (# (suc n)) ⟩
#⊆suc n {x} = ∈sucV-inl {A = # n} {x = x}

#mono : (m n : ℕ) → m < n → ⟨ (# m) ∈ˢ (# n) ⟩
#mono m zero    m<0    = Empty.rec (¬-<-zero m<0)
#mono m (suc n) m<sucn = Sum.rec
```

In the successor step, `<-split` merely says `m < suc n` splits into `m < n` or `m ≡ n`. In the first branch the induction hypothesis gives `# m ∈ # n`, and `#⊆suc` promotes it into the successor. In the second branch the two numerals coincide, and a set belongs to its own successor, so transporting along the reversal of `m ≡ n` turns the membership `# n ∈ # (suc n)` into the one wanted.

```agda
  (λ m<n → #⊆suc n (#mono m n m<n))
  (λ m≡n → subst (λ M → ⟨ (# M) ∈ˢ (# (suc n)) ⟩) (sym m≡n) (self∈sucV (# n)))
  (<-split m<sucn)
```

Injectivity follows by trichotomy on the indices. Equal indices are the conclusion. If `m < n`, monotonicity gives `# m ∈ # n`, and the assumed equation `# m ≡ # n` transports this membership into `# n ∈ # n`, which membership irreflexivity forbids. The remaining case `n < m` is the mirror image, with the transport run in the other direction.

The strictly-smaller case is the instructive one. The membership `# m ∈ # n` speaks about the numeral `# m`; rewriting its type along `# m ≡ # n` replaces that set by `# n` everywhere, producing an inhabitant of `# n ∈ # n`. Irreflexivity of membership consumes this inhabitant into an element of the empty type, so the case cannot arise.

```agda
#-inj : (m n : ℕ) → # m ≡ # n → m ≡ n
#-inj m n #m≡#n with m ≟ n
... | eq m≡n = m≡n
... | lt m<n = Empty.rec (∈-irrefl (# n)
      (subst (λ z → ⟨ z ∈ˢ (# n) ⟩) #m≡#n (#mono m n m<n)))
```

The greater case is identical with the roles of `m` and `n` exchanged: monotonicity puts `# n` inside `# m`, the equation transports in the opposite direction, and irreflexivity of `# m` refutes it. The variant `#-inj′` packages the same statement with the indices implicit, which is the shape the coding interface consumes.

```agda
... | gt n<m = Empty.rec (∈-irrefl (# m)
      (subst (λ z → ⟨ z ∈ˢ (# m) ⟩) (sym #m≡#n) (#mono n m n<m)))

#-inj′ : ∀ {m n} → # m ≡ # n → m ≡ n
#-inj′ {m} {n} = #-inj m n
```

## Kuratowski pairing

The second injective alphabet is the Kuratowski pair: the code of `a` and `b` is the set whose members are the singleton `⁅ a ⁆s` and the unordered pair `⁅ a , b ⁆`. Note the distinction between the outer ordered pair, which records order, and its inner unordered pair, which does not. Injectivity means both components are recoverable from the code, and this recovery is driven entirely by the classification specifications: membership in a singleton is equality to its element, and membership in an unordered pair merely means equality to one of the two.

The singleton classification is named once in both directions. `∈singl` says a member of `⁅ a ⁆s` must equal `a`, and `singl∈` says equality suffices to belong. Both are projections of the same classification record for the singleton package.

```agda
private
  ∈singl : {a x : S} → ⟨ x ∈ₛ ⁅ a ⁆s ⟩ → x ≡ a
  ∈singl {a} {x} = SetPackage.classification (SingletonPackage a) x .fst

  singl∈ : {a x : S} → x ≡ a → ⟨ x ∈ₛ ⁅ a ⁆s ⟩
  singl∈ {a} {x} = SetPackage.classification (SingletonPackage a) x .snd
```

For unordered pairs, the classification has the shape of a truncated disjunction: a member of `⁅ a , b ⁆` is, merely, equal to `a` or to `b`. The two introduction lemmas supply the left and right disjuncts as truncated witnesses, so membership can be produced from either equality without choosing anything.

```agda
  self∈singl : (a : S) → ⟨ a ∈ₛ ⁅ a ⁆s ⟩
  self∈singl a = singl∈ refl

  inl∈⁅,⁆ : {a b x : S} → x ≡ a → ⟨ x ∈ₛ ⁅ a , b ⁆ ⟩
  inl∈⁅,⁆ {a} {b} {x} e = pairing-ax a b x .snd ∣ inl e ∣₁

  inr∈⁅,⁆ : {a b x : S} → x ≡ b → ⟨ x ∈ₛ ⁅ a , b ⁆ ⟩
```

A singleton determines its element: if `⁅ a ⁆s ≡ ⁅ c ⁆s`, transport the membership `a ∈ ⁅ a ⁆s` along this path and classify the result; it must equal `c`. The elimination is into the path proposition `a ≡ c`, which is allowed since `V` is an h-set.

```agda
  inr∈⁅,⁆ {a} {b} {x} e = pairing-ax a b x .snd ∣ inr e ∣₁

  mem⁅,⁆ : {a b x : S} → ⟨ x ∈ₛ ⁅ a , b ⁆ ⟩ → ∥ (x ≡ a) ⊎ (x ≡ b) ∥₁
  mem⁅,⁆ {a} {b} {x} = pairing-ax a b x .fst

  singl-inj : {a c : S} → ⁅ a ⁆s ≡ ⁅ c ⁆s → a ≡ c
  singl-inj {a} {c} q = ∈singl (subst (λ s → ⟨ a ∈ₛ s ⟩) q (self∈singl a))
```

A singleton that happens to equal an unordered pair forces both components down to its element. Each component belongs to the unordered pair merely, so transporting the membership across `sym q` and classifying yields a path from that component to `a`; both eliminations target the pair of path propositions `(c ≡ a) × (d ≡ a)`. This degenerate comparison is exactly the hard case of pair injectivity below.

```agda
  singl≡pair : {a c d : S} → ⁅ a ⁆s ≡ ⁅ c , d ⁆ → (c ≡ a) × (d ≡ a)
  singl≡pair {a} {c} {d} q =
      ∈singl (subst (λ s → ⟨ c ∈ₛ s ⟩) (sym q) (inl∈⁅,⁆ {a = c} {b = d} refl))
    , ∈singl (subst (λ s → ⟨ d ∈ₛ s ⟩) (sym q) (inr∈⁅,⁆ {a = c} {b = d} refl))
```

The injectivity proof of the pair is now assembled from the four comparison lemmas. Given `p : pr a b ≡ pr c d`, the singleton part of the code is a member of both sides, so transporting its membership forward along `p` and classifying yields, merely, `⁅ a ⁆s ≡ ⁅ c ⁆s` or `⁅ a ⁆s ≡ ⁅ c , d ⁆`; the first disjunct gives `a ≡ c` immediately and the second through the reversal of `singl≡pair`. The unordered-pair part is harder because its membership alone may not determine the second component: when the code collapses, `⁅ a , b ⁆` has matched a singleton on the left or the right, and knowing which side it matched is not enough. So two truncated records are kept, one transported forward along `p` from membership of `⁅ a , b ⁆` in `pr a b`, and one transported backward along the reversal of `p` from membership of `⁅ c , d ⁆` in `pr c d`. The backward record supplies exactly the information the degenerate branches lack, and under the temporary hypothesis `a ≡ b`, the case where the whole code collapses to a singleton of singletons, it converts a recovered `a ≡ b` into `d ≡ b`. Every elimination of a truncated disjunction in this proof targets a proposition built from paths in the h-set `V`, so no witness is ever chosen.

The code `pr a b` is the unordered pair whose two members are the singleton `⁅ a ⁆s` and the unordered pair `⁅ a , b ⁆`. The outer expression is the ordered Kuratowski code, and it should not be confused with its second ingredient: the inner `⁅ a , b ⁆` records no order, the whole code does. Injectivity is the claim that an equality of codes `pr a b ≡ pr c d` determines both inputs, that is, it yields paths `a ≡ c` and `b ≡ d`.

```agda
pr : S → S → S
pr a b = ⁅ ⁅ a ⁆s , ⁅ a , b ⁆ ⁆

pr-inj : ∀ {a b c d} → pr a b ≡ pr c d → (a ≡ c) × (b ≡ d)
pr-inj {a} {b} {c} {d} p = a≡c , b≡d
  where
```

First component. The singleton part `⁅ a ⁆s` belongs to `pr a b` by its right disjunct. Transporting this membership along `p` and classifying gives, merely, `⁅ a ⁆s ≡ ⁅ c ⁆s` or `⁅ a ⁆s ≡ ⁅ c , d ⁆` (this is `H₁`). In the first disjunct `singl-inj` yields `a ≡ c` directly. In the second, the comparison `singl≡pair` forces `c ≡ a`, and its reversal is what is wanted. The truncated disjunction is eliminated into the path proposition `a ≡ c`, which is permitted since `V` is an h-set.

```agda
  H₁ : ∥ (⁅ a ⁆s ≡ ⁅ c ⁆s) ⊎ (⁅ a ⁆s ≡ ⁅ c , d ⁆) ∥₁
  H₁ = mem⁅,⁆ (subst (λ s → ⟨ ⁅ a ⁆s ∈ₛ s ⟩) p (inl∈⁅,⁆ {b = ⁅ a , b ⁆} refl))

  a≡c : a ≡ c
  a≡c = PT.rec (setIsSet a c)
    (Sum.rec singl-inj (λ e → sym (singl≡pair e .fst))) H₁
```

Second component. Two truncated records are gathered. `H₂` comes from membership of the unordered-pair part in `pr a b`, transported forward along `p`: merely, `⁅ a , b ⁆` equals `⁅ c ⁆s` or `⁅ c , d ⁆`. `K` runs the same argument backwards, from membership of `⁅ c , d ⁆` in `pr c d` transported along `sym p`: merely, `⁅ c , d ⁆` equals `⁅ a ⁆s` or `⁅ a , b ⁆`. Both are needed because in the degenerate cases below each single record leaves a gap that only the other fills.

```agda
  H₂ : ∥ (⁅ a , b ⁆ ≡ ⁅ c ⁆s) ⊎ (⁅ a , b ⁆ ≡ ⁅ c , d ⁆) ∥₁
  H₂ = mem⁅,⁆ (subst (λ s → ⟨ ⁅ a , b ⁆ ∈ₛ s ⟩) p (inr∈⁅,⁆ {a = ⁅ a ⁆s} refl))

  K : ∥ (⁅ c , d ⁆ ≡ ⁅ a ⁆s) ⊎ (⁅ c , d ⁆ ≡ ⁅ a , b ⁆) ∥₁
  K = mem⁅,⁆ (subst (λ s → ⟨ ⁅ c , d ⁆ ∈ₛ s ⟩) (sym p) (inr∈⁅,⁆ {a = ⁅ c ⁆s} refl))

  d≡b-from-K : a ≡ b → d ≡ b
```

The helper `d≡b-from-K` handles the degenerate situation under the temporary hypothesis `a ≡ b`, where the two ingredients of the code coincide and `pr a b` collapses to the unordered pair `⁅ ⁅ a ⁆s , ⁅ a ⁆s ⁆`. Reading `K`: either `⁅ c , d ⁆` equals the singleton `⁅ a ⁆s`, whose classification forces `d ≡ a`, hence `d ≡ b`; or it equals `⁅ a , b ⁆`, in which case `d` is, merely, equal to `a` or to `b`, and both alternatives compose to `d ≡ b`. All eliminations land in the path proposition `d ≡ b`.

```agda
  d≡b-from-K a≡b = PT.rec (setIsSet d b)
    (Sum.rec
      (λ e → singl≡pair (sym e) .snd ∙ a≡b)
      (λ e → PT.rec (setIsSet d b)
        (Sum.rec (λ d≡a → d≡a ∙ a≡b) (λ d≡b → d≡b))
```

The main argument for `b ≡ d` runs through `H₂`. In its first disjunct, the inner unordered pair `⁅ a , b ⁆` equals the singleton `⁅ c ⁆s`; the comparison `singl≡pair` read backwards gives `b ≡ c`, and from `a ≡ c` and the reversal of `b ≡ c` the path `a ≡ b` follows, exactly the hypothesis the helper consumes. The helper then yields `d ≡ b`, whose reversal is the goal. This is where the backward record `K` enters: the helper is stated from `K`, so the forward classification alone does not reach this case.

```agda
        (mem⁅,⁆ (subst (λ s → ⟨ d ∈ₛ s ⟩) e (inr∈⁅,⁆ {a = c} refl)))))
    K

  b≡d : b ≡ d
  b≡d = PT.rec (setIsSet b d)
    (Sum.rec
```

In the second disjunct of `H₂`, the two inner unordered pairs coincide, `⁅ a , b ⁆ ≡ ⁅ c , d ⁆`. Then `b` belongs to `⁅ c , d ⁆` merely, so classifying the membership of `b` gives `b ≡ c` or `b ≡ d`. The second alternative is already the goal; the first reduces to it through the same composition and helper as before.

```agda
      (λ e → let b≡c = singl≡pair (sym e) .snd
             in sym (d≡b-from-K (a≡c ∙ sym b≡c)))
      (λ e → PT.rec (setIsSet b d)
        (Sum.rec
          (λ b≡c → sym (d≡b-from-K (a≡c ∙ sym b≡c)))
```

The two branches combine into `b ≡ d`, completing `pr-inj`: both components of the Kuratowski code are recoverable from an equality of codes. Every branch eliminated a truncated disjunction into a proposition built from paths in the h-set `V`; no witness was ever chosen from a truncation.

```agda
          (λ b≡d → b≡d))
        (mem⁅,⁆ (subst (λ s → ⟨ b ∈ₛ s ⟩) e (inr∈⁅,⁆ {a = a} refl)))))
    H₂
```

## The instance

With both injective alphabets in hand, the generic coding construction of FOL.Coding can be applied to the hierarchy: an injective pairing and an injective numeral map are its two parameters. The resulting `VCode` assigns to terms and formulas over the hierarchy's carrier codes that are themselves sets of the hierarchy. It does not make every set a code; it gives set-valued codes for the coded syntax.

Note the level: `VCode` is taken at `ℓ-suc ℓ`, the level at which the relations of the `ZFStructure` `𝒮ᵥ` take values. This universe index is a type-theoretic level, not a stage of the hierarchy.

The instantiation passes the level `ℓ-suc ℓ`, the structure `𝒮ᵥ`, and the four pieces established above: `pr` with `pr-inj`, and the numeral map `#_` with `#-inj′`. No classical axiom, resizing, or choice hypothesis enters; the instance rests on the classification specifications and the two injectivity proofs alone.

```agda
module VCode = FOL.Coding {ℓ-suc ℓ} 𝒮ᵥ pr pr-inj #_ #-inj′
```

## Recap

The two injective operations the generic coding needs were already available in the hierarchy. Numerals are injective: `#-inj` follows from monotonicity and membership irreflexivity under the natural-number trichotomy. Kuratowski pairs are injective: `pr-inj` recovers both components through the classification specifications for singletons and unordered pairs. The instantiation `VCode` therefore supplies the FOL.Coding construction over the hierarchy, at level `ℓ-suc ℓ` and without any classical hypothesis. Terms and formulas over the hierarchy's sets now have codes that are sets of `V`, and the `Codes` relation is available to reason about them.