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.

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

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.

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.

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

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