Coding inside the cumulative hierarchy

Read this chapter directly, or use the reading guide and dependency map to choose another route.

Reading guide · Dependency map

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.

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

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.

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.

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.

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.

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

  (λ 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.

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

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

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.

  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.

  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.

  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.

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.

  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.

  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.

  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.

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

      (λ 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.

          (λ 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.

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.