---
title: "Choice by a transversal"
module: L.Choice.Transversal
lang: en
site: "Bedrock"
description: "Choice by a transversal"
stage: "The canonical well-order and Choice"
reading_order: 84
canonical: https://bedrock.institute/en/L.Choice.Transversal.html
html: L.Choice.Transversal.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Choice/Transversal.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.ZFModel, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Axioms.Basic, L.Choice.FirstIntersectionStage, L.Choice.StageOrders, L.Choice.InternalWellOrder, L.Coding.Model, L.WellOrder.Base]
routes: [choice-completion]
translations: [https://bedrock.institute/zh/L.Choice.Transversal.md, https://bedrock.institute/ja/L.Choice.Transversal.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Choice by a transversal

This chapter proves the axiom of choice for `𝒮ʟ` by separating the least member
of every cell under a stage-bounded internal well-order and showing that the
resulting set meets each pairwise-disjoint cell exactly once.

This chapter proves the axiom of choice at `𝒮ʟ` in the **transversal** form
used by the model record: given a set whose members
are inhabited and pairwise disjoint, merely a set meeting each member in exactly
one point.

The argument follows the classical proof, with its most laborious step already
carried out earlier. The textbook well-orders the universe and takes the least member of every
cell. A well-order of all of `L` is a relation on a proper class, and this book
never built one; what the previous chapters built instead is a well-order of each
**stage**, uniformly, and, at every ordinal, as an element of the model. That is
enough, because a set is small. One ordinal bounds a family, its members and
their members all at once, and inside the tower at that ordinal the choosing is
an ordinary least-element search.

So the chapter is four moves. The **bound**: the stage chapter's bounding ordinal
for the family, above the family's own stage and hence above every member of
every member of it. The **order there**: the table's relation at that ordinal, an
element of the model, with two lemmas reading membership in it against the meta
comparison in both directions. The **description**: "some member of the family
contains this set, and nothing in that member precedes it", a formula with the
order as a constant, which the model's own separation cuts a set out with. The
**count**: that set meets each member in exactly one point, existence from the
least element and uniqueness from pairwise disjointness, which is what
disjointness is for and the only place the book uses it.

There is a fifth thing, and it is an observation rather than a move. Choice is
stated relative to a ZF model on this carrier, because the intersection it names
is that model's derived operation; and the whole of that dependence is one
transport along the intersection's specification.

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

open import Base.Prelude
open import Base.Classical using ( LEM )

module L.Choice.Transversal {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; con; _∈̇_; _∧̇_; ¬̇_; ∃̇_ )
import FOL.ZFModel
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset→isL )
open import L.Axioms.Basic {ℓ} using ( LsetS )
open import L.Choice.FirstIntersectionStage {ℓ} lem using ( bound-below₂ )
open import L.Choice.StageOrders {ℓ} lem using ( Mem; relOf )
open import L.Choice.InternalWellOrder {ℓ} lem using ( module Bound )
open import L.Coding.Model {ℓ} using ( appC; appC-adequate )
open import L.WellOrder.Base {ℓ-suc ℓ}
  using ( SWO; IsLeast; isPropLeastOf; leastOf )

open import Cubical.Data.Sigma using ( Σ≡Prop )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁ )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )

open hPropStructure 𝒮ʟ

module ModelL = FOL.ZFModel 𝒮ʟ
open ModelL using ( isZFModel )

module AbsL = FOL.Absoluteness.Single 𝒮ᵥ isL isL-trans
open AbsL renaming ( _⊨ᵐ_ to _⊨_ )
```

## The description

`Pick` is the one-variable formula saying that a point lies in a member
of the family and has no predecessor there under the chosen relation.

One formula, one free variable, two constants. Of a set `z` it says: some member
of the family contains `z`, and nothing in that member precedes `z` under the
order. The application atom takes the order directly as a constant. The family
is likewise named directly, since it appears only under a membership atom.

The formula is sealed, by the standing law that a description read at constants
is sealed where it is built. Here that law is free rather than decisive: sealed
and unsealed both check in 2.3 s, and the chapter says so rather than borrowing
someone else's number. The reason is worth one line, because it says what the
earlier measurements were really about. Those descriptions carried coded syntax
inside them, and each satisfaction at a concrete environment normalized a whole
hierarchy description; this one carries four atoms and one application, so there
is nothing large to unfold. The seal stays, because it costs nothing and because
a later reader of this description should not have to re-measure.

Perf: sealed by the standing law (a description read at constants), though
measured here at 2.3 s either way: this description names no coded syntax.

```agda
opaque
  Pick : S → S → Formula S 1
  Pick c r =
    ∃̇ ( (var zero ∈̇ con c)
      ∧̇ ( (var (suc zero) ∈̇ var zero)
        ∧̇ (¬̇ ∃̇ ( (var zero ∈̇ var (suc zero))
               ∧̇ appC r zero (suc (suc zero)) )) ) )
```

## The transversal

Inside the bounding stage, least-element search chooses one point per cell;
separation collects those points, and disjointness proves uniqueness in every
intersection.

The module fixes the ZF model supplying the intersection, the family, and the
family's two hypotheses. The choice-stage construction supplies the bound and
order at the family itself: `β` is an ordinal above the family's own
stage, hence above its members and their members, and above `ω` where the names
live; `W` is the well-order of the members of the tower at `β`; and
`rel` is that same order as an **element of the model**, which is what
lets it be named by a constant in the description at all.

`Cell x` is the predicate "is a member of `x`" on those members, and
`least` applies the generic search from `L.WellOrder.Base` to it.
The same search serves finite-stage orders and name selection, and will serve
later GCH constructions; here its role is specific: it turns the stage order
into one chosen representative for each cell. This is precisely the selection
that excluded middle makes possible for the transversal.

`pick-in` and `pick-out` are the description's two readings, and
neither is a corollary of the other: one builds a satisfaction out of a least
element, the other extracts a least element from a satisfaction, and each has to
move a set between the two ways it can be presented, as an element of `L` and as
a member of the tower at `β`. Every truncation payload is named,
`Two` and `Predecessor`, so that neither reading writes the nesting
out; the negation is the one place a truncation is eliminated into the empty
type, and it is eliminated in a named helper.

Then the separation and the counting. `transversalSet` is the model's own
separation, at the tower at `β`, by the description. `Cut` fixes a
member of the family: the centre of the intersection is the least element, which
is in the transversal because `pick-in` says so and in the member because
being least includes being there. Uniqueness is where pairwise disjointness is
used. Another point of the intersection satisfies the description, so it is least in
**some** member of the family; it also lies in this one; so the two members meet
and are equal; so it is least in this member too, and least elements are unique
by trichotomy alone. The generic uniqueness theorem
`isPropLeastOf` closes precisely this last comparison.

```agda
module Trans (zf : isZFModel) (a : S)
             (inh : (x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁)
             (disj : (x y : S) → ⟨ x ∈ˢ a ⟩ → ⟨ y ∈ˢ a ⟩
                   → ∥ Σ[ z ∈ S ] (⟨ z ∈ˢ x ⟩ × ⟨ z ∈ˢ y ⟩) ∥₁ → x ≡ y)
             where
  open ModelL.isZFModel zf using ( separate; separate-spec; _∩_; ∩-spec )
  private
    module B = Bound (fst a) (snd a)

  β : V ℓ
  β = B.boundOrd

  oβ : IsOrd β
  oβ = B.boundOrd-ord

  W : SWO (Mem (Lset β))
  W = B.boundOrder

  rel : S
  rel = B.orderL

  elt : Mem (Lset β) → S
  elt m = fst m , Lset→isL β oβ (fst m) (snd m)

  Cell : S → Mem (Lset β) → hProp (ℓ-suc ℓ)
  Cell x m = fst m ∈ fst x

  Least : S → S → Type (ℓ-suc ℓ)
  Least x z = Σ[ h ∈ ⟨ fst z ∈ Lset β ⟩ ] IsLeast W (Cell x) (fst z , h)

  private
    members : (x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ m ∈ Mem (Lset β) ] ⟨ Cell x m ⟩ ∥₁
    members x x∈a = PT.map atMember (inh x x∈a)
      where
      atMember : Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ → Σ[ m ∈ Mem (Lset β) ] ⟨ Cell x m ⟩
      atMember (y , y∈x) =
        (fst y , bound-below₂ (fst a) (snd a) (fst x) (fst y) y∈x x∈a) , y∈x

    least : (x : S) → ⟨ x ∈ˢ a ⟩ → Σ[ m ∈ Mem (Lset β) ] IsLeast W (Cell x) m
    least x x∈a = leastOf W lem (Cell x) (members x x∈a)

    Predecessor : S → S → S → Type (ℓ-suc ℓ)
    Predecessor x z w = ⟨ w ∈ˢ x ⟩
                      × ⟨ (w ∷ x ∷ z ∷ []) ⊨ appC rel zero (suc (suc zero)) ⟩

    Two : S → S → Type (ℓ-suc ℓ)
    Two x z = ⟨ x ∈ˢ a ⟩
            × (⟨ z ∈ˢ x ⟩
              × (∥ Σ[ w ∈ S ] Predecessor x z w ∥₁
                 → Lift {j = ℓ-suc ℓ} Empty.⊥))

    Out : S → Type (ℓ-suc ℓ)
    Out z = ∥ Σ[ x ∈ S ] (⟨ x ∈ˢ a ⟩ × Least x z) ∥₁

  opaque
    unfolding Pick

    pick-in : (x : S) → ⟨ x ∈ˢ a ⟩ → (z : S) → Least x z
            → ⟨ (z ∷ []) ⊨ Pick a rel ⟩
    pick-in x x∈a z (hz , (z∈x , mini)) =
      ∣ x , (x∈a , (z∈x , neg)) ∣₁
      where
      noPredecessor : Σ[ w ∈ S ] Predecessor x z w → Empty.⊥
      noPredecessor (w , (w∈x , hap)) = mini (fst w , hw) w∈x lt
        where
        hw : ⟨ fst w ∈ Lset β ⟩
        hw = bound-below₂ (fst a) (snd a) (fst x) (fst w) w∈x x∈a
        hpr : ⟨ pr (fst w) (fst z) ∈ fst rel ⟩
        hpr = subst ⟨_⟩ (appC-adequate rel zero (suc (suc zero)) (w ∷ x ∷ z ∷ [])) hap
        lt : relOf W (fst w , hw) (fst z , hz)
        lt = B.orderL-rep (fst w , hw) (fst z , hz) hpr

      neg : ∥ Σ[ w ∈ S ] Predecessor x z w ∥₁
          → Lift {j = ℓ-suc ℓ} Empty.⊥
      neg q = lift (PT.rec Empty.isProp⊥ noPredecessor q)

    pick-out : (z : S) → ⟨ (z ∷ []) ⊨ Pick a rel ⟩ → Out z
    pick-out z = PT.rec PT.squash₁ atTwo
      where
      atTwo : Σ[ x ∈ S ] Two x z → Out z
      atTwo (x , (x∈a , (z∈x , neg))) = ∣ x , (x∈a , (hz , (z∈x , mini))) ∣₁
        where
        hz : ⟨ fst z ∈ Lset β ⟩
        hz = bound-below₂ (fst a) (snd a) (fst x) (fst z) z∈x x∈a

        mini : (b : Mem (Lset β)) → ⟨ Cell x b ⟩
             → relOf W b (fst z , hz) → Empty.⊥
        mini b b∈x lt = lower (neg ∣ elt b , (b∈x , hap) ∣₁)
          where
          hpr : ⟨ pr (fst b) (fst z) ∈ fst rel ⟩
          hpr = B.orderL-fill b (fst z , hz) lt
          hap : ⟨ (elt b ∷ x ∷ z ∷ []) ⊨ appC rel zero (suc (suc zero)) ⟩
          hap = subst ⟨_⟩
            (sym (appC-adequate rel zero (suc (suc zero)) (elt b ∷ x ∷ z ∷ []))) hpr

  transversalSet : S
  transversalSet = separate (LsetS β oβ) (Pick a rel)

  private
    csp : (z : S) → (z ∈ˢ transversalSet)
                  ≡ ((z ∈ˢ LsetS β oβ) ⊓ ((z ∷ []) ⊨ Pick a rel))
    csp = separate-spec (LsetS β oβ) (Pick a rel)

    inC : (z : S) → ⟨ fst z ∈ Lset β ⟩ → ⟨ (z ∷ []) ⊨ Pick a rel ⟩
        → ⟨ z ∈ˢ transversalSet ⟩
    inC z hL hp = subst ⟨_⟩ (sym (csp z)) (hL , hp)

    outC : (z : S) → ⟨ z ∈ˢ transversalSet ⟩ → ⟨ (z ∷ []) ⊨ Pick a rel ⟩
    outC z h = snd (subst ⟨_⟩ (csp z) h)

  module Cut (x : S) (x∈a : ⟨ x ∈ˢ a ⟩) where
    private
      m : Mem (Lset β)
      m = least x x∈a .fst

      lm : IsLeast W (Cell x) m
      lm = least x x∈a .snd

      z₀ : S
      z₀ = elt m

      inMeet : (z : S) → ⟨ z ∈ˢ transversalSet ⟩ → ⟨ z ∈ˢ x ⟩
             → ⟨ z ∈ˢ (transversalSet ∩ x) ⟩
      inMeet z hc hx = subst ⟨_⟩ (sym (∩-spec transversalSet x z)) (hc , hx)

      outMeet : (z : S) → ⟨ z ∈ˢ (transversalSet ∩ x) ⟩
              → ⟨ z ∈ˢ transversalSet ⟩ × ⟨ z ∈ˢ x ⟩
      outMeet z h = subst ⟨_⟩ (∩-spec transversalSet x z) h

      centre : Σ[ z ∈ S ] ⟨ z ∈ˢ (transversalSet ∩ x) ⟩
      centre = z₀ , inMeet z₀
        (inC z₀ (snd m) (pick-in x x∈a z₀ (snd m , lm))) (fst lm)

      same : (z : S) → ⟨ z ∈ˢ (transversalSet ∩ x) ⟩ → fst z ≡ fst m
      same z h = PT.rec (setIsSet (fst z) (fst m)) atOut
                   (pick-out z (outC z (fst (outMeet z h))))
        where
        z∈x : ⟨ z ∈ˢ x ⟩
        z∈x = snd (outMeet z h)

        atOut : Σ[ x' ∈ S ] (⟨ x' ∈ˢ a ⟩ × Least x' z) → fst z ≡ fst m
        atOut (x' , (x'∈a , (hz , lz))) =
          cong (λ p → fst (fst p))
            (isPropLeastOf W (Cell x) ((fst z , hz) , lz') (m , lm))
          where
          x≡x' : x ≡ x'
          x≡x' = disj x x' x∈a x'∈a ∣ z , (z∈x , fst lz) ∣₁

          lz' : IsLeast W (Cell x) (fst z , hz)
          lz' = subst (λ y → IsLeast W (Cell y) (fst z , hz)) (sym x≡x') lz

    meetsOnce : isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (transversalSet ∩ x) ⟩)
    meetsOnce = centre , atPoint
      where
      atPoint : (p : Σ[ z ∈ S ] ⟨ z ∈ˢ (transversalSet ∩ x) ⟩) → centre ≡ p
      atPoint (z , h) = sym (Σ≡Prop
        (λ w → snd (w ∈ˢ (transversalSet ∩ x)))
        (Σ≡Prop (λ v → snd (isL v)) (same z h)))

  transversal : (x : S) → ⟨ x ∈ˢ a ⟩
              → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (transversalSet ∩ x) ⟩)
  transversal = Cut.meetsOnce
```

## The theorem

The final wrapper converts the transversal construction into the exact choice
field required by the ZF model record on `𝒮ʟ`.

`ChoiceStatement` is the statement the frontier used to hold, moved here
verbatim and proved here: the model's choice field at `𝒮ʟ`, relative to a
ZF model on this carrier because the intersection is that model's derived
operation. `hasChoiceL` gives the proof. The root chapter applies it to the very
model it is assembling, which is why the statement quantifies over the model in
the first place.

This line gives the Choice field used by the root theorem. Its statement
remains relative to the ZF model being assembled because intersection is the
derived operation of that model.

```agda
ChoiceStatement : isZFModel → Type (ℓ-suc ℓ)
ChoiceStatement zf =
  (a : S)
  → ((x : S) → ⟨ x ∈ˢ a ⟩ → ∥ Σ[ y ∈ S ] ⟨ y ∈ˢ x ⟩ ∥₁)
  → ((x y : S) → ⟨ x ∈ˢ a ⟩ → ⟨ y ∈ˢ a ⟩
       → ∥ Σ[ z ∈ S ] (⟨ z ∈ˢ x ⟩ × ⟨ z ∈ˢ y ⟩) ∥₁ → x ≡ y)
  → ∥ Σ[ c ∈ S ] ((x : S) → ⟨ x ∈ˢ a ⟩
       → isContr (Σ[ z ∈ S ] ⟨ z ∈ˢ (c ∩ x) ⟩)) ∥₁
  where open ModelL.isZFModel zf using ( _∩_ )

hasChoiceL : (zf : isZFModel) → ChoiceStatement zf
hasChoiceL zf a inh disj = ∣ T.transversalSet , T.transversal ∣₁
  where module T = Trans zf a inh disj
```

## Recap

`Pick`, the bounded stage order, and separation together produce the
transversal whose exact-one-point property supplies `hasChoiceL`.

`Pick` is the description: some member of the family contains this set,
and nothing in that member precedes it. `pick-in` and `pick-out`
are its two readings against being a least element of a member.
`transversalSet` is what the model's separation cuts out with it, over the
tower at the family's bounding ordinal, and `transversal` counts the
intersection with each member: one point, existence from the least-element
search and uniqueness from pairwise disjointness. `hasChoiceL` is the
model's choice field, and with it the frontier is empty and gone.

One measurement, and it is a law declining to bite. A description read at
constants is sealed where it is built, and that law was worth ninety-nine fold
where it was found; here it is worth nothing, 2.3 s either way, because this
description carries no coded syntax. The seal stays, and the number is recorded
so that the law keeps its true shape: it is about what a description **contains**,
not about where it is read.

## What the book was for

The completed Choice chain supplies the missing model field, so under the single
stated excluded-middle hypothesis the constructible universe satisfies ZFC.

This is the end of the chain, so it is worth stating plainly what has been
established. **In cubical Agda, granted one instance of the excluded middle at the
model's own truth level, the constructible universe is a model of ZFC.** Read with the
ambient-hierarchy result that the hierarchy models ZF, that is Gödel's relative consistency of
choice in semantic form: a universe satisfying ZF contains inside it a
sub-universe satisfying ZFC, so an inconsistency of ZFC would already be an
inconsistency of ZF.

The costs are stated explicitly. The host is cubical Agda with its universe
tower, informally about as strong as ZFC plus an inaccessible; excluded middle
is a module parameter rather than an axiom, and it is the only hypothesis the
theorem carries; and the development has no postulates or holes. This chapter
supplies the Choice field that `L.Model` combines with the earlier ZF
structure.