---
title: "The square law for infinite L-cardinals"
module: L.GCH.CardinalSquareLaw
lang: en
site: "Bedrock"
description: "The square law for infinite L-cardinals"
stage: "Proving GCH"
reading_order: 111
canonical: https://bedrock.institute/en/L.GCH.CardinalSquareLaw.html
html: L.GCH.CardinalSquareLaw.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/GCH/CardinalSquareLaw.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, L.Choice.FirstIntersectionStage, V.Model, V.Presentation, V.Coding, L.Constructible, L.Ordinal, L.Ordinal.Stages, L.Ordinal.Linear, L.Ordinal.SquareLaw, L.WellOrder.Base, L.Axioms.Basic, L.Axioms.Infinity, L.Axioms.Numerals, L.Coding.Model, L.Coding.Expressions, L.Coding.Injection, L.Cardinal, L.InjectionComposition, L.GCH.CardinalRepresentative, L.DefinableInjection, L.GCH.OrderType]
routes: [hulls-and-counting]
translations: [https://bedrock.institute/zh/L.GCH.CardinalSquareLaw.md, https://bedrock.institute/ja/L.GCH.CardinalSquareLaw.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# The square law for infinite L-cardinals

For an infinite cardinal `κ` of `L`, the set of ordered pairs of members of `κ` injects into `κ` itself, by an internal coded injection. This chapter builds that injection. The route runs through the Gödel order on pairs: the order is written as a formula of the first-order object language, read off at the ordinal `κ` as the external Gödel order, and collapsed to an order type that the counting lemmas compare with `κ`. The chapter works at a fixed universe level `ℓ`, under excluded middle at the next level, the one classical assumption on which the ordinal comparisons below depend.

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

The construction is not constructive throughout, and the reason lies in the mathematics rather than in the formalism. To order the pairs of an ordinal one must decide, for two ordinals `a` and `b`, whether `a` belongs to `b`; and every classical decision of this chapter is an instance of that single question. The module therefore receives excluded middle at level `ℓ-suc ℓ` as explicit data, the level of the membership propositions being decided.

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

The module parameter fixes that instance once, and every classical step of the chapter consumes precisely it.

```agda
module L.GCH.CardinalSquareLaw {ℓ : Level} (lem : LEM (ℓ-suc ℓ)) where
```

The order to be internalized is written in the first-order object language: formulas built from membership and equality atoms by the connectives, negation and the unbounded existential, interpreted over the ambient hierarchy. Two facts of the hierarchy stand beside it, and both are used to end arguments: membership is well-founded, so ordinals admit induction along `∈`, and no set belongs to itself, so impossible comparisons can be refuted outright.

```agda
open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax
  using ( Formula; var; con; _∈̇_; _≐_; _∧̇_; _∨̇_; ¬̇_; ∃̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ; regularityV; ∈-irrefl )
```

Reading the coordinates of a coded pair, and counting with them, rests on three facts. The successor operation on ordinals is injective, so equal successors have equal predecessors. Every member of an ordinal is named by an index of its small presentation, the naming is injective, and a member of a constructible set is itself constructible. And the ordered pair `pr` is injective in both coordinates, so a coded pair determines its two entries.

```agda
open import L.Choice.FirstIntersectionStage {ℓ} lem using ( ord-suc-inj )
open import V.Model {ℓ} using ( ∈sucV-elim; ∈sucV-inl; self∈sucV )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import V.Coding {ℓ} using ( pr; pr-inj )
open import L.Constructible {ℓ}
```

On the constructible side, the inner structure `𝒮ʟ` restricts the hierarchy to the transitive class of constructible sets. The ordinal facts used throughout are closure facts: members of ordinals are ordinals, successors of ordinals are ordinals, the members of `ω` are ordinals, and any two ordinals are comparable by trichotomy. Beside them stands the external Gödel order on pairs, the order this chapter internalizes.

```agda
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset→isL )
open import L.Ordinal {ℓ} using ( mem-ord; suc-ord; ω-ord; #∈ω; ω-mem-ord )
open import L.Ordinal.Stages {ℓ} lem using ( ord∈Lset-suc )
open import L.Ordinal.Linear {ℓ} lem using ( ord-tri )
import L.Ordinal.SquareLaw {ℓ} lem as SQ
```

The comparison of two ordinals is packaged as three-case data rather than as a truth value, because the proofs below must inspect which case occurred: strictly below, equal, or strictly above. The empty set and `ω` are available as elements of `L`, and the internal successor numerals come with the identification of their underlying sets, which lets a numeral slot be read as an ambient natural number.

```agda
open import L.WellOrder.Base {ℓₚ = ℓ-suc ℓ}
  using ( lt; eq; gt ) renaming ( Tri to TriW )
open import L.Axioms.Basic {ℓ} using ( ∅ʟ )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Axioms.Numerals {ℓ} using ( sucʟ; sucʟ-fst )
```

Inside `L`, ordered pairs and graph conditions are expressed by first-order formulas with inner and ambient readings. Pairing adequacy identifies the coded pair with the ambient ordered pair of its two entries, while the graph readings express single-valuedness, domain, injectivity, and containment of values in the codomain. Together these conditions describe an internal coded injection.

```agda
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-out; domAt )
open import L.Coding.Expressions {ℓ} using ( sucAtL; sucAtL-adequate )
open import L.Coding.Injection {ℓ} lem using ( injAt; module Extract; module Small )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL; IsCardinalL; _↪_ )
open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
```

Three mathematical transitions drive the construction. An ordinal is replaced by an internal cardinal representative contained in it and internally equipotent to it. A definable injective function yields a coded injection. Finally, a well-founded transitive relation is collapsed to an ordinal order type, while trichotomy makes the collapse map injective.

```agda
open import L.GCH.CardinalRepresentative {ℓ} lem using ( cardOf )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.OrderType {ℓ} lem using ( Holds; module Code )
open import L.InjectionComposition {ℓ} lem
  using ( appC; appC-adequate; ω-limit; finite-excl-ω )
```

A comparison of two coded pairs carries six dependent witnesses: four coordinates and their two maxima. Products retain the simultaneous equations and order conditions, while disjoint sums retain the alternative comparison cases. Since the proof components are propositions, they do not create additional choices in the resulting order data.

```agda
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.Prelude using ( subst2 )
open import Cubical.Foundations.HLevels
  using ( isProp×; isSetΣSndProp )
```

The coordinates of a coded pair are members of the underlying set of `κ`, read through the small presentation of that set. Beside the presentation stand the ambient membership, the empty set with its emptiness proof, and `ω` with the successor operation, the notions in which the two coordinates are compared and counted.

```agda
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪; ∈∈ₛ )
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( ∅; ∅-empty; module InfinitySet )
open InfinitySet {ℓ} using ( ω; sucV )
```

Three logical forms recur. Well-foundedness appears as accessibility data for every element, which is what lets the collapse descend along the order. Refutations live in the empty type. And a condition that only asserts that witnesses exist is stated under truncation, which is enough because the goals that consume such conditions are themselves propositions or truncations.

```agda
open import Cubical.Induction.WellFounded using ( Acc; acc; WellFounded )
import Cubical.Induction.WellFounded as WF
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )
```

Two carriers are named and kept apart. The ambient carrier carries the hierarchy's own membership; the inner carrier `S` consists of the constructible sets, each an ambient set with its constructibility proof, and its membership is the ambient membership read on the underlying sets.

```agda
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )
module SV = hPropStructure 𝒮ᵥ using ()
module SL = hPropStructure 𝒮ʟ using (S; _∈ˢ_)
open SL using ( S )
```

The absoluteness instance is fixed over the transitive class of constructible sets: bounded formulas mean the same inside `L` as outside, environments are read through the projection, and the inner satisfaction relation is renamed to plain `_⊨_`.

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

The inner carrier is an h-set, and this is what makes equality of its elements manageable. Its elements are pairs whose second components are propositions, so two elements are equal exactly when their underlying sets are, and the pair-path lemma builds the equality of two pairs from equalities of their components.

```agda
isSetS : isSet S
isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))
opaque
  pair≡ : {A : Type ℓ} {B : Type ℓ} {a a' : A} {b b' : B}
        → a ≡ a' → b ≡ b' → (a , b) ≡ (a' , b')
```

The pair path is exactly that construction: from `a ≡ a'` and `b ≡ b'` it forms, pointwise, the path `(a , b) ≡ (a' , b')`. Ordinals are constructible, and for a direct reason: an ordinal `x` is a member of its own successor, whose stage is a set of `L`, and membership in a stage is constructibility. The statement is a proposition, so its proof carries no information beyond the fact.

```agda
  pair≡ e1 e2 = λ i → e1 i , e2 i
opaque
  isL-ord : (x : V ℓ) → IsOrd x → ⟨ isL x ⟩
  isL-ord x ox = Lset→isL (sucV x) (suc-ord ox) x (ord∈Lset-suc x ox)
```

Thus an ordinal `x` can be regarded as the element `ordL x ox` of the constructible carrier. Applying definable separation to the relation saying that both coordinates belong to `K` then produces `prodL K`, the constructible set of their ordered pairs.

```agda
ordL : (x : V ℓ) → IsOrd x → S
ordL x ox = x , isL-ord x ox
open import L.InjectionComposition {ℓ} lem public using ( module Relation )
private
  module Product (K : S) = Relation K K
```

The describing condition of the product says that both coordinates are members of `K`. Its host reading is the ambient membership of the two projections in the underlying set of `K`, and both directions of the reading are supplied.

```agda
    ((var (suc zero) ∈̇ con K) ∧̇ (var zero ∈̇ con K))
    (λ x y → (fst x ∈ˢ fst K) ⊓ (fst y ∈ˢ fst K))
    (λ x y e h → h) (λ x y e h → h)
```

`prodL K` is therefore the set of the ordered pairs of two members of `K`, separated inside `L` from the stage that bounds them.

```agda
prodL : S → S
prodL = Product.rel
```

Membership in the product is characterized by a truncated existence: some two members `a` and `b` of `K` with the member equal to their ordered pair. The truncation records exactly what the condition asserts, that witnesses exist, and at this point nothing distinguishes one pair of witnesses from another; removing it becomes possible only after the uniqueness of the witnesses has been proved.

```agda
InProd : S → V ℓ → Type (ℓ-suc ℓ)
InProd K e = ∥ Σ[ a ∈ S ] Σ[ b ∈ S ]
               (⟨ fst a ∈ˢ fst K ⟩ × ⟨ fst b ∈ˢ fst K ⟩
                × (e ≡ pr (fst a) (fst b))) ∥₁
```

Inward, the ordered pair of any two members of `K` belongs to `prodL K`; this is the separated relation's own introduction rule.

```agda
prodL-in : (K a b : S) → ⟨ fst a ∈ˢ fst K ⟩ → ⟨ fst b ∈ˢ fst K ⟩
         → ⟨ pr (fst a) (fst b) ∈ˢ fst (prodL K) ⟩
prodL-in K a b ma mb = Product.into K a b ma mb (ma , mb)
```

Outward, a member of `prodL K` comes, in truncated form, from two members of `K` and the pair equation. Against the small presentation of `K` the stronger, untruncated statement is available: every member of the product is the ordered pair of the elements named by two indices of `K`.

```agda
prodL-out : (K e : S) → ⟨ fst e ∈ˢ fst (prodL K) ⟩ → InProd K (fst e)
prodL-out K e h = PT.map (λ { (a , b , q , ma , mb) → a , b , ma , mb , q }) (Product.out K e h)
prodL-fst : (K e : S) → ⟨ fst e ∈ˢ fst (prodL K) ⟩
          → Σ[ a ∈ ⟪ fst K ⟫ ] Σ[ b ∈ ⟪ fst K ⟫ ]
              (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b))
```

The proof converts the truncated witnesses into the fibers of `K`'s indexing, and repairs the pair equation along the fibers' own identifications, which say that each member of `K` is exactly the set its index names.

```agda
prodL-fst K e h = PT.rec isPropFib
  (λ { (a , b , ma , mb , q) →
     fiber (fst K) ma .fst , fiber (fst K) mb .fst
     , q ∙ cong₂ pr (sym (fiber (fst K) ma .snd)) (sym (fiber (fst K) mb .snd)) })
  (prodL-out K e h)
```

The second components are unique: the injectivity of the ordered pair extracts an equation of the named sets, and the injectivity of `K`'s indexing turns it into an equation of indices.

```agda
  where
  inner : (a : ⟪ fst K ⟫)
        → isProp (Σ[ b ∈ ⟪ fst K ⟫ ] (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b)))
  inner a (b , q) (b' , q') = Σ≡Prop (λ _ → setIsSet _ _)
    (↪-inj {a = fst K} (pr-inj (sym q ∙ q') .snd))
```

The first components are unique for the same reason, so the whole fiber statement is a proposition: the untruncated reading does not depend on any choice.

```agda
  isPropFib : isProp (Σ[ a ∈ ⟪ fst K ⟫ ] Σ[ b ∈ ⟪ fst K ⟫ ]
                        (fst e ≡ pr (⟪ fst K ⟫↪ a) (⟪ fst K ⟫↪ b)))
  isPropFib (a , b , q) (a' , b' , q') = Σ≡Prop inner
    (↪-inj {a = fst K} (pr-inj (sym q ∙ q') .fst))
```

## The Gödel order, as a formula

With the product in hand, the order enters: `MaxIs` says that `m` is the maximum of `a` and `b` when these are ordinals.

```agda
MaxIs : S → S → S → Type (ℓ-suc ℓ)
```

The definition offers two alternatives: either `a` belongs to `b` and `m` is `b`, or membership of `a` in `b` is refuted and `m` is `a`. Only the disjunction is truncated, because the definition asserts that one of the alternatives holds without deciding which; on ordinals, excluded middle selects the branch, and the selected `m` is then the maximum of `a` and `b`.

```agda
MaxIs m a b =
  ∥ (⟨ fst a ∈ˢ fst b ⟩ × (fst m ≡ fst b))
  ⊎ ((⟨ fst a ∈ˢ fst b ⟩ → Empty.⊥) × (fst m ≡ fst a)) ∥₁
```

The Gödel comparison of two pairs is likewise data under truncation: either the maximum `m` of the first pair belongs to the maximum `n` of the second, or the two maxima are equal and the pairs compare lexicographically, first coordinate against first coordinate, then second against second.

```agda
OrdIs : S → S → S → S → S → S → Type (ℓ-suc ℓ)
OrdIs m n a b c d =
  ∥ ⟨ fst m ∈ˢ fst n ⟩
  ⊎ ((fst m ≡ fst n)
     × ∥ ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩) ∥₁) ∥₁
```

The maximum is expressible as a bounded formula: `m` equals `b` when `a` belongs to `b`, and equals `a` when membership of `a` in `b` is refuted, the negation making the second alternative a guarded branch. When `a` and `b` are ordinals, this formula says precisely that `m` is their maximum.

```agda
maxAt : ∀ {k} → Fin k → Fin k → Fin k → Formula S k
maxAt m a b = ((var a ∈̇ var b) ∧̇ (var m ≐ var b))
            ∨̇ ((¬̇ (var a ∈̇ var b)) ∧̇ (var m ≐ var a))
```

The Gödel comparison is expressible the same way, with its priorities made explicit: first the maxima are compared; when the maxima are equal, the first coordinates are compared; and when the first coordinates are equal as well, the second coordinates are compared.

```agda
ordAt : ∀ {k} → Fin k → Fin k → Fin k → Fin k → Fin k → Fin k → Formula S k
ordAt m n a b c d =
    (var m ∈̇ var n)
  ∨̇ ((var m ≐ var n)
     ∧̇ ((var a ∈̇ var c) ∨̇ ((var a ≐ var c) ∧̇ (var b ∈̇ var d))))
```

Putting the pieces together, `Lt p q` says that `p` and `q` are coded pairs, of members `a`, `b` and of members `c`, `d`, whose maxima `m` and `n` satisfy the maximum conditions and whose comparison satisfies the Gödel condition. The six witnesses are recorded under truncation: the conditions assert that witnesses exist, and the classical case analysis selects among the alternatives only afterwards.

```agda
Lt : V ℓ → V ℓ → Type (ℓ-suc ℓ)
Lt p q = ∥ Σ[ a ∈ S ] Σ[ b ∈ S ] Σ[ c ∈ S ] Σ[ d ∈ S ] Σ[ m ∈ S ] Σ[ n ∈ S ]
           ( (p ≡ pr (fst a) (fst b)) × (q ≡ pr (fst c) (fst d))
           × MaxIs m a b × MaxIs n c d × OrdIs m n a b c d ) ∥₁
```

Six binders need six slots beyond the caller's environment, and `↑6` shifts an index by exactly that many positions.

```agda
private
  ↑6 : ∀ {k} → Fin k → Fin (suc (suc (suc (suc (suc (suc k))))))
  ↑6 i = suc (suc (suc (suc (suc (suc i)))))
```

The six slots are named `i0` through `i5`, one per quantified witness. The first aliases bind positions zero, one and two, which will hold the maximum of the second pair, the maximum of the first pair, and the second coordinate of the second pair.

```agda
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc zero
  i2 : ∀ {k} → Fin (suc (suc (suc k)))
```

The aliases continue: position two is filled by the second coordinate of the second pair, position three by its first coordinate, position four by the second coordinate of the first pair.

```agda
  i2 = suc (suc zero)
  i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
  i3 = suc (suc (suc zero))
  i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))
  i4 = suc (suc (suc (suc zero)))
```

Position five is the first coordinate of the first pair, completing the six. The order formula itself then begins: it will bind the six witnesses in sequence and say of `p` and `q` exactly what the Gödel comparison requires.

```agda
  i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
  i5 = suc (suc (suc (suc (suc zero))))
opaque
  ltAt : ∀ {k} → Fin k → Fin k → Formula S k
  ltAt p q = ∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (∃̇ (
```

The body binds six witnesses in sequence and conjoins five atoms: `p` is the ordered pair of the fifth and fourth slots, `q` is the ordered pair of the third and second, the first maximum atom relates the coordinates of `p`, the second maximum atom those of `q`, and the order atom compares the two maxima and then the coordinates. Read in the six-slot context, this says exactly that `p` is below `q` in the Gödel order.

```agda
        prAtL (↑6 p) i5 i4
     ∧̇ (prAtL (↑6 q) i3 i2
     ∧̇ (maxAt i1 i5 i4
     ∧̇ (maxAt i0 i3 i2
     ∧̇ ordAt i1 i0 i5 i4 i3 i2)))))))))
```

Adequacy is checked against a concrete six-entry context. The context extends the caller's environment by the six witnesses, newest first: `n`, `m`, `d`, `c`, `b`, `a`, so that slot zero is `n` and slot five is `a`, matching the aliases.

```agda
  private
    env : ∀ {k} → S ^ k → S → S → S → S → S → S
        → S ^ (suc (suc (suc (suc (suc (suc k))))))
    env γ a b c d m n = n ∷ m ∷ d ∷ c ∷ b ∷ a ∷ γ
```

The first adequacy lemma reads the pair atom at that context: satisfaction of the pairing atom is the equation between the caller's `p` and the ordered pair of `a` and `b`.

```agda
    atP : ∀ {k} (p : Fin k) (γ : S ^ k) (a b c d m n : S)
        → ⟨ env γ a b c d m n ⊨ prAtL (↑6 p) i5 i4 ⟩
        ≡ (fst (lookup p γ) ≡ pr (fst a) (fst b))
    atP p γ a b c d m n = cong ⟨_⟩ (prAtL-adequate (↑6 p) i5 i4 (env γ a b c d m n))
```

The second does the same for `q` and the pair of `c` and `d`. With these two identifications, the satisfaction of the formula is interchangeable with the six-witness data of `Lt`.

```agda
    atQ : ∀ {k} (q : Fin k) (γ : S ^ k) (a b c d m n : S)
        → ⟨ env γ a b c d m n ⊨ prAtL (↑6 q) i3 i2 ⟩
        ≡ (fst (lookup q γ) ≡ pr (fst c) (fst d))
    atQ q γ a b c d m n = cong ⟨_⟩ (prAtL-adequate (↑6 q) i3 i2 (env γ a b c d m n))
```

The outward direction consumes the six nested truncations in turn: satisfaction of `ltAt p q` at `γ` yields witnesses `a` through `n` together with the pair equations, the two maximum data, and the order data.

```agda
  lt-out : ∀ {k} (p q : Fin k) (γ : S ^ k) → ⟨ γ ⊨ ltAt p q ⟩
         → Lt (fst (lookup p γ)) (fst (lookup q γ))
  lt-out p q γ = PT.rec squash₁ (λ { (a , ha) → PT.rec squash₁ (λ { (b , hb) →
    PT.rec squash₁ (λ { (c , hc) → PT.rec squash₁ (λ { (d , hd) →
    PT.rec squash₁ (λ { (m , hm) → PT.rec squash₁ (λ { (n , (hp , (hq , (hM , (hN , hO))))) →
```

The two pair equations are transported along the adequacy paths, and the first maximum datum is carried to the ambient level. The six existential witnesses live at the lifted semantic level, so the affirmation case passes unchanged while the refutation case is lowered out of the lifting.

```agda
      ∣ a , b , c , d , m , n
      , ( transport (atP p γ a b c d m n) hp
        , transport (atQ q γ a b c d m n) hq
        , PT.map (λ { (inl h) → inl h
                    ; (inr (n , e)) → inr ((λ k → lower (n k)) , e) }) hM
```

The second maximum datum is mapped identically, completing the witness of `Lt` at the caller's `p` and `q`.

```agda
        , PT.map (λ { (inl h) → inl h
                    ; (inr (n , e)) → inr ((λ k → lower (n k)) , e) }) hN
        , hO ) ∣₁ }) hm }) hd }) hc }) hb }) ha })
```

The inward direction turns `Lt` into the satisfaction statement, which is a proposition.

```agda
  lt-in : ∀ {k} (p q : Fin k) (γ : S ^ k)
        → Lt (fst (lookup p γ)) (fst (lookup q γ)) → ⟨ γ ⊨ ltAt p q ⟩
  lt-in p q γ = PT.rec (snd (γ ⊨ ltAt p q))
    (λ { (a , b , c , d , m , n , (ep , eq' , hM , hN , hO)) →
      ∣ a , ∣ b , ∣ c , ∣ d , ∣ m , ∣ n
```

The six witnesses are re-entered as the nested existential witnesses, with the pair equations transported along the adequacy paths in the reverse direction.

```agda
      , ( transport (sym (atP p γ a b c d m n)) ep
        , ( transport (sym (atQ q γ a b c d m n)) eq'
        , ( PT.map (λ { (inl h) → inl h
                      ; (inr (n , e)) → inr ((λ k → lift (n k)) , e) }) hM
          , ( PT.map (λ { (inl h) → inl h
```

The two maximum data are mapped back, this time lifted into the object level's guarded atoms, and the order datum closes the formula. The Gödel module then packages the order for a set `P`: its describing condition requires both coordinates to be members of `P` and relates them by the order formula.

```agda
                        ; (inr (n , e)) → inr ((λ k → lift (n k)) , e) }) hN
            , hO )))) ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ ∣₁ })
private
  module Godel (P : S) = Relation P P
    ((var (suc zero) ∈̇ con P) ∧̇ ((var zero ∈̇ con P) ∧̇ ltAt (suc zero) zero))
```

The host reading adds membership in `P` on both sides, conjoined with the order relation, and the two directions quote the outward and inward lemmas at the slots the two binders occupy: the first coordinate in the outer slot, the second in the inner one.

```agda
    (λ p q → (fst p ∈ˢ fst P) ⊓ ((fst q ∈ˢ fst P) ⊓ (Lt (fst p) (fst q) , squash₁)))
    (λ p q e h → h .fst , h .snd .fst , lt-out (suc zero) zero (q ∷ p ∷ e ∷ []) (h .snd .snd))
    (λ p q e h → h .fst , h .snd .fst , lt-in (suc zero) zero (q ∷ p ∷ e ∷ []) (h .snd .snd))
```

`godel P` is that separated relation: inside `L`, the set of the ordered pairs of members of `P` that compare below one another in the Gödel order.

```agda
godel : S → S
godel = Godel.rel
```

Inward: for two members `p` and `q` of `P` with `p` below `q`, their ordered pair belongs to `godel P`.

```agda
godel-in : (P p q : S) → ⟨ fst p ∈ˢ fst P ⟩ → ⟨ fst q ∈ˢ fst P ⟩
         → Lt (fst p) (fst q) → ⟨ pr (fst p) (fst q) ∈ˢ fst (godel P) ⟩
godel-in P p q mp mq l = Godel.into P p q mp mq (mp , mq , l)
```

Outward: a member of `godel P` comes with both members and the order data between them.

```agda
godel-out : (P p q : S) → ⟨ pr (fst p) (fst q) ∈ˢ fst (godel P) ⟩
          → ⟨ fst p ∈ˢ fst P ⟩ × ⟨ fst q ∈ˢ fst P ⟩ × Lt (fst p) (fst q)
godel-out = Godel.pair-out
```

## The transfer to the host order

The order module then fixes an ordinal `κ`, the case at which the square law is stated.

```agda
module Order (κ : S) (oκ : IsOrd (fst κ)) where
```

`K` is the underlying set of the ordinal `κ`; the carrier on which the square law unfolds is precisely this set of ordinals below `κ`.

```agda
  K : V ℓ
  K = fst κ
```

`↑` names the members of `K` ambiently, through the small presentation's embedding: each index denotes the ordinal it presents.

```agda
  ↑ : ⟪ K ⟫ → V ℓ
  ↑ = ⟪ K ⟫↪
```

An index `m : ⟪ K ⟫` names the ambient set `↑ m`, together with a proof that it belongs to `κ`. Since constructibility is inherited by members, `upK m` packages that named ordinal as an element of `L`.

```agda
  upK : ⟪ K ⟫ → S
  upK m = ↑ m , isL-trans {x = K} {y = ↑ m} (member K m) (snd κ)
```

The carrier of the order to be compared is `Pair`, the type of two indices of `κ`: an ordered pair in the host, each coordinate naming an ordinal below `κ`.

```agda
  Pair : Type ℓ
  Pair = ⟪ K ⟫ × ⟪ K ⟫
```

On the coordinates themselves stands the coordinate order `≺₁`, quoted from the external square-law development: ordinals below `κ` compare strictly by membership of the ambient sets they name.

```agda
  _≺₁_ : ⟪ K ⟫ → ⟪ K ⟫ → Type (ℓ-suc ℓ)
  _≺₁_ = SQ._≺₁_ K oκ
```

On pairs stands the Gödel order `≺ₚ`: compare maxima first, then the first coordinates, then the second. This is the external order that the internal formula must reproduce.

```agda
  _≺ₚ_ : Pair → Pair → Type (ℓ-suc ℓ)
  _≺ₚ_ = SQ._≺_ K oκ
```

The maximum operation `maxOrd` returns, for two ordinals below `κ`, the larger of the two, again quoted from the external development and again reading as a maximum only because the entries are ordinals.

```agda
  maxOrd : ⟪ K ⟫ → ⟪ K ⟫ → ⟪ K ⟫
  maxOrd = SQ.maxOrd K oκ
```

Two small facts prepare the comparison between the two sides. First, every member of the ordinal `κ` is itself an ordinal, so the named ordinals carry ordinality certificates. Second, `max-out` states that the internal maximum condition, read at elements whose underlying sets name `a'` and `b'`, forces the internal maximum to be exactly the host maximum of `a'` and `b'`; the proof proceeds by the trichotomy data of the host order.

```agda
  ord↑ : (m : ⟪ K ⟫) → IsOrd (↑ m)
  ord↑ m = mem-ord {A = K} oκ (↑ m) (member K m)
  max-out : (a b m : S) (a' b' : ⟪ K ⟫) → fst a ≡ ↑ a' → fst b ≡ ↑ b'
          → MaxIs m a b → fst m ≡ ↑ (maxOrd a' b')
  max-out a b m a' b' ea eb = PT.rec (setIsSet _ _) (go (SQ.tri₁ K oκ a' b'))
```

The case function fixes the shape of that argument: the host trichotomy splits into below, equal, and above; the internal datum splits into the affirmation, where `m` is `b`, and the refutation, where `m` is `a`. Matching the two splits term by term is the whole content.

```agda
    where
    go : (t : TriW (a' ≺₁ b') (a' ≡ b') (b' ≺₁ a'))
       → (⟨ fst a ∈ˢ fst b ⟩ × (fst m ≡ fst b))
         ⊎ ((⟨ fst a ∈ˢ fst b ⟩ → Empty.⊥) × (fst m ≡ fst a))
       → fst m ≡ ↑ (SQ.maxGo K oκ a' b' t)
```

In the below case the affirmation composes the equation of `m` with `b` and the naming of `b`, giving the host maximum. Its refutation branch is impossible: the membership it refutes is exactly the trichotomy's witness, transported through the two namings.

```agda
    go (lt h) (inl (_ , e))   = e ∙ eb
    go (lt h) (inr (na , _))  =
      Empty.rec (na (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) (sym ea) (sym eb) h))
    go (eq p) (inl (a∈b , _)) =
      Empty.rec (∈-irrefl (↑ b')
```

In the equal case an affirmation would place `a` inside `b` while the host declares them equal, contradicting the irreflexivity of membership at the named ordinal `b`; the refutation branch then names the maximum as `a`, transported along the naming of `a`.

```agda
        (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) (ea ∙ cong ↑ p) eb a∈b))
    go (eq p) (inr (_ , e))   = e ∙ ea
    go (gt h) (inl (a∈b , _)) =
      Empty.rec (∈-irrefl (↑ a')
        (ord↑ a' .fst {x = ↑ b'} {y = ↑ a'}
```

In the above case the host witness puts `b` inside `a`; an affirmative internal branch would also put `a` inside `b`, and transitivity would contradict irreflexivity at `a`.

```agda
          (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) ea eb a∈b) h))
    go (gt h) (inr (_ , e))   = e ∙ ea
```

The converse `max-in` writes the host maximum into the internal predicate: for every pair of indices, the lifted element named by `maxOrd` satisfies `MaxIs` at the two lifted coordinates.

```agda
  max-in : (a' b' : ⟪ K ⟫) → MaxIs (upK (maxOrd a' b')) (upK a') (upK b')
  max-in a' b' = go (SQ.tri₁ K oκ a' b')
    where
    go : (t : TriW (a' ≺₁ b') (a' ≡ b') (b' ≺₁ a'))
       → MaxIs (upK (SQ.maxGo K oκ a' b' t)) (upK a') (upK b')
```

Its three cases are immediate from the host comparison: below gives the affirmation with the equation definitional, equality refutes membership by irreflexivity, and above refutes it through the coordinate's own ordinality. The same block defines `code`, the ambient ordered pair of the two named ordinals of a host pair.

```agda
    go (lt h) = ∣ inl (h , refl) ∣₁
    go (eq p) = ∣ inr ((λ h → ∈-irrefl (↑ b') (subst (λ w → ⟨ ↑ w ∈ˢ ↑ b' ⟩) p h)) , refl) ∣₁
    go (gt h) = ∣ inr ((λ h' → ∈-irrefl (↑ a') (ord↑ a' .fst {x = ↑ b'} {y = ↑ a'} h' h)) , refl) ∣₁
  code : Pair → V ℓ
  code p = pr (↑ (fst p)) (↑ (snd p))
```

The heart of the transfer is the refutation lemma. It assumes a contradiction-shaped pair of data: `Lt` holds of the coded pairs of `p` and `q`, while the host order refuses to compare them. The six witnesses of such an assumed `Lt` are collected into a single statement of absurdity.

```agda
  private
    refute : (p q : Pair) → (p ≺ₚ q → Empty.⊥)
           → Σ[ a ∈ S ] Σ[ b ∈ S ] Σ[ c ∈ S ] Σ[ d ∈ S ] Σ[ m ∈ S ] Σ[ n ∈ S ]
               ( (code p ≡ pr (fst a) (fst b)) × (code q ≡ pr (fst c) (fst d))
               × MaxIs m a b × MaxIs n c d × OrdIs m n a b c d )
```

The conclusion is the empty type: the assumed order data and the refused comparison cannot coexist. The proof destructures the six witnesses and works on the underlying sets they name.

```agda
           → Empty.⊥
    refute (a' , b') (c' , d') nk (a , b , c , d , m , n , (ep , eq' , hM , hN , hO)) =
      PT.rec Empty.isProp⊥ outer hO
      where
      ea : fst a ≡ ↑ a'
```

The injectivity of the ordered pair extracts, from each coding equation, the identification of the underlying set of each witness with the corresponding named ordinal. These four equations anchor every later comparison.

```agda
      ea = sym (pr-inj ep .fst)
      eb : fst b ≡ ↑ b'
      eb = sym (pr-inj ep .snd)
      ec : fst c ≡ ↑ c'
      ec = sym (pr-inj eq' .fst)
```

The two maxima are then identified with the host maxima, by `max-out` applied to the two maximum data. At this point the internal and external readings of the whole configuration coincide on all six coordinates.

```agda
      ed : fst d ≡ ↑ d'
      ed = sym (pr-inj eq' .snd)
      em : fst m ≡ ↑ (maxOrd a' b')
      em = max-out a b m a' b' ea eb hM
      en : fst n ≡ ↑ (maxOrd c' d')
```

The equation `en` supplies the same identification for the second pair, so `OrdIs` can now be transported entirely to the host maxima and coordinates.

```agda
      en = max-out c d n c' d' ec ed hN
```

The inner lemma transfers the coordinate comparison. An ambient membership between the named first coordinates becomes membership in the host order, transported along the identifications of the two namings.

```agda
      inner : ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩)
            → (a' ≺₁ c') ⊎ ((a' ≡ c') × (b' ≺₁ d'))
      inner (inl h)       = inl (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) ea ec h)
      inner (inr (e , h)) =
        inr ( ↪-inj {a = K} (sym ea ∙ e ∙ ec)
```

The equality case transfers as well: an equality of the named sets, cycled through the two namings, becomes an equality of indices by the injectivity of `K`'s naming, and the second coordinates compare as before.

```agda
            , subst2 (λ x y → ⟨ x ∈ˢ y ⟩) eb ed h )
```

If the first maximum belongs to the second, transporting this membership along `em` and `en` gives the first, strict-maximum branch of `p ≺ₚ q`, contradicting `nk`.

```agda
      outer : ⟨ fst m ∈ˢ fst n ⟩
            ⊎ ((fst m ≡ fst n)
               × ∥ ⟨ fst a ∈ˢ fst c ⟩ ⊎ ((fst a ≡ fst c) × ⟨ fst b ∈ˢ fst d ⟩) ∥₁)
            → Empty.⊥
      outer (inl h)       = nk (inl (subst2 (λ x y → ⟨ x ∈ˢ y ⟩) em en h))
```

If the two maxima are equal, the equality of the underlying sets becomes an equality of indices by the naming injectivity, and the inner lemma then compares the pairs inside the host order, refuting the refusal once more.

```agda
      outer (inr (e , h)) = PT.rec Empty.isProp⊥
        (λ w → nk (inr (↪-inj {a = K} (sym em ∙ e ∙ en) , inner w))) h
```

To prove `lt→≺`, trichotomy leaves three possibilities for the host pairs. The desired strict case is immediate. Equality and the reverse strict case would each make any refusal of `p ≺ₚ q` incompatible with the assumed `Lt`, by `refute`; hence both also yield the desired comparison.

```agda
  lt→≺ : (p q : Pair) → Lt (code p) (code q) → p ≺ₚ q
  lt→≺ p q l = go (SQ.tri≺ K oκ p q)
    where
    refuted : ((p ≺ₚ q) → Empty.⊥) → p ≺ₚ q
    refuted nk = Empty.rec (PT.rec Empty.isProp⊥ (refute p q nk) l)
```

In the equality case, a putative `p ≺ₚ q` transports to `q ≺ₚ q` and violates irreflexivity. In the reverse strict case, composing that putative comparison with `q ≺ₚ p` gives `p ≺ₚ p`, again impossible.

```agda
    go : TriW (p ≺ₚ q) (p ≡ q) (q ≺ₚ p) → p ≺ₚ q
    go (lt k) = k
    go (eq e) = refuted (λ k → SQ.irr≺ K oκ q (subst (λ w → w ≺ₚ q) e k))
    go (gt h) = refuted (λ k → SQ.irr≺ K oκ p (SQ.trans≺ K oκ p q p k h))
```

The converse `≺→lt` writes the host comparison into the object language. Its six witnesses are the lifted coordinates and the two lifted maxima, the pair equations are definitional, the maximum data come from `max-in`, and the order data from the host comparison itself.

```agda
  ≺→lt : (p q : Pair) → p ≺ₚ q → Lt (code p) (code q)
  ≺→lt (a' , b') (c' , d') k =
    ∣ upK a' , upK b' , upK c' , upK d' , upK (maxOrd a' b') , upK (maxOrd c' d')
    , ( refl , refl , max-in a' b' , max-in c' d' , ord k ) ∣₁
    where
```

The order datum is read case by case: strict membership passes through untouched, and the two equality cases are transported along the naming of the maxima and the naming of the coordinates respectively.

```agda
    ord : (a' , b') ≺ₚ (c' , d')
        → OrdIs (upK (maxOrd a' b')) (upK (maxOrd c' d')) (upK a') (upK b') (upK c') (upK d')
    ord (inl h)                 = ∣ inl h ∣₁
    ord (inr (e , inl h))       = ∣ inr (cong ↑ e , ∣ inl h ∣₁) ∣₁
    ord (inr (e , inr (f , h))) = ∣ inr (cong ↑ e , ∣ inr (cong ↑ f , h) ∣₁) ∣₁
```

If `x < y`, transitivity with `y < z` gives `x < z`; if `x = y`, the given comparison `y < z` is transported along that equality.

```agda
  private
    ≤→≺ : (x y z : ⟪ K ⟫) → SQ._≤₁_ K oκ x y → y ≺₁ z → x ≺₁ z
    ≤→≺ x y z (inl h) h' = SQ.trans₁ K oκ x y z h h'
    ≤→≺ x y z (inr e) h' = subst (λ w → w ≺₁ z) (sym e) h'
```

The companion lemma turns `x ≤ y` and `y = y'` into membership of `x` in the successor of `y'`. In the strict case, `x ∈ y'` gives successor membership directly; in the equality case, identifying `x` with `y'` reduces the claim to `y'` belonging to its own successor.

```agda
    ≤→∈suc : (x y y' : ⟪ K ⟫) → SQ._≤₁_ K oκ x y → y ≡ y'
           → ⟨ ↑ x ∈ˢ sucV (↑ y') ⟩
    ≤→∈suc x y y' (inl h) e = ∈sucV-inl (subst (λ w → x ≺₁ w) e h)
    ≤→∈suc x y y' (inr q) e =
      subst (λ w → ⟨ ↑ w ∈ˢ sucV (↑ y') ⟩) (sym (q ∙ e)) (self∈sucV (↑ y'))
```

The segment lemmas now read off the order. If a pair `r` is below a pair `p`, the first coordinate of `r` is a member of the successor of the maximum of `p`: in the strict-max case this is at-most followed by strict comparison.

```agda
  fst∈suc : (r p : Pair) → r ≺ₚ p
          → ⟨ ↑ (fst r) ∈ˢ sucV (↑ (maxOrd (fst p) (snd p))) ⟩
  fst∈suc (a , b) (c , d) (inl h) =
    ∈sucV-inl (≤→≺ a (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .fst) h)
  fst∈suc (a , b) (c , d) (inr (e , _)) =
```

In the equal-max case the first coordinate is at most the shared maximum and the two maxima are identified, so membership in the successor follows from the self-membership of the maximum in its own successor.

```agda
    ≤→∈suc a (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .fst) e
```

The same argument, applied to the second coordinates, gives `snd∈suc`: the second coordinate of `r` also lands in the successor of `p`'s maximum, whether the maxima compare strictly or are equal.

```agda
  snd∈suc : (r p : Pair) → r ≺ₚ p
          → ⟨ ↑ (snd r) ∈ˢ sucV (↑ (maxOrd (fst p) (snd p))) ⟩
  snd∈suc (a , b) (c , d) (inl h) =
    ∈sucV-inl (≤→≺ b (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .snd) h)
  snd∈suc (a , b) (c , d) (inr (e , _)) =
```

These two bounds show that every predecessor of a pair `(c, d)` has both coordinates in `suc(max(c, d))`.

```agda
    ≤→∈suc b (maxOrd a b) (maxOrd c d) (SQ.max-spec K oκ a b .snd) e
module Coll (κ : S) (oκ : IsOrd (fst κ)) where
```

These bounds control every predecessor segment of the Gödel order. Together with well-foundedness and transitivity, they place the relation on `prodL κ` in the setting where it can be collapsed to its ordinal order type.

```agda
  open Order κ oκ
```

The set to be collapsed onto an order type is `P`, the product: the ordered pairs of members of the ordinal `κ`, already separated inside `L`.

```agda
  P : S
  P = prodL κ
```

The relation of the collapse is `R`, the Gödel order on that product: two members of `P` stand related exactly when the first compares below the second.

```agda
  R : S
  R = godel P
```

For the Gödel relation this follows directly: whenever `y R x`, both `y` and `x` are members of the product.

```agda
  Rsub : (y x : S) → Holds R y x → ⟨ fst y ∈ fst P ⟩ × ⟨ fst x ∈ fst P ⟩
  Rsub y x h = godel-out P y x h .fst , godel-out P y x h .snd .fst
```

The order-type machinery is instantiated once and for this product. Its domain is an index set for the collapse, and `φ` reads off, for each index, the host pair that the corresponding member of the product presents: the two coordinates are recovered untruncated by the presentation reader of the product.

```agda
  module OT = Code P R Rsub using (Dom; Dom≡; isProp≺; toDom; up; up-mem; up-toDom; ↪; _≺_; ≺-in; ≺-out; module Conjuncts)
  φ : OT.Dom → Pair
  φ m = prodL-fst κ (OT.up m) (OT.up-mem m) .fst
      , prodL-fst κ (OT.up m) (OT.up-mem m) .snd .fst
```

The reading comes with its equation: the internal coding of the index equals the ambient ordered pair of the two coordinates. This equation is the hinge on which every comparison between the internal and external orders turns.

```agda
  φ-eq : (m : OT.Dom) → OT.↪ m ≡ code (φ m)
  φ-eq m = prodL-fst κ (OT.up m) (OT.up-mem m) .snd .snd
```

`φ` is injective: if two indices name the same host pair, their codings agree, and the domain's own criterion, equality of codings, returns equality of indices. Thus no two product indices can be sent to the same host pair.

```agda
  φ-inj : (m n : OT.Dom) → φ m ≡ φ n → m ≡ n
  φ-inj m n e = OT.Dom≡ (φ-eq m ∙ cong code e ∙ sym (φ-eq n))
```

The forward transfer reads the internal order outward: if two indices compare inside `L`, their host pairs compare in the Gödel order. The proof quotes the defining equation and the outward reading of the formula, then applies the transfer `lt→≺` at the two host pairs.

```agda
  ≺-fwd : (m n : OT.Dom) → m OT.≺ n → φ m ≺ₚ φ n
  ≺-fwd m n k = lt→≺ (φ m) (φ n)
    (subst2 Lt (φ-eq m) (φ-eq n) (godel-out P (OT.up m) (OT.up n) (OT.≺-out m n k) .snd .snd))
```

The backward transfer reads the host order inward, quoting the inward reading of the formula and the transfer `≺→lt` at the same two pairs. Together the two directions say: the internal relation on the collapse's indices is exactly the host Gödel order, read through `φ`.

```agda
  ≺-bwd : (m n : OT.Dom) → φ m ≺ₚ φ n → m OT.≺ n
  ≺-bwd m n k = OT.≺-in m n
    (godel-in P (OT.up m) (OT.up n) (OT.up-mem m) (OT.up-mem n)
      (subst2 Lt (sym (φ-eq m)) (sym (φ-eq n)) (≺→lt (φ m) (φ n) k)))
```

Well-foundedness transfers with the indices. The accessibility of a host pair supplies the accessibility of the corresponding index, whose predecessors map forward to host pairs of strictly smaller pairs. Induction along the external order thus becomes induction along the internal one.

```agda
  wf : WellFounded OT._≺_
  wf m = go (SQ.wf≺ K oκ (φ m))
    where
    go : {n : OT.Dom} → Acc _≺ₚ_ (φ n) → Acc OT._≺_ n
    go {n} (acc r) = acc (λ n' k → go (r (φ n') (≺-fwd n' n k)))
```

Transitivity transfers the same way: two internal steps are read outward, composed by the host order's transitivity, and read back inward as one internal step from `a` to `c`.

```agda
  ≺-trans : {a b c : OT.Dom} → a OT.≺ b → b OT.≺ c → a OT.≺ c
  ≺-trans {a} {b} {c} k k' =
    ≺-bwd a c (SQ.trans≺ K oκ (φ a) (φ b) (φ c) (≺-fwd a b k) (≺-fwd b c k'))
```

Trichotomy completes the transferred package. For any two indices, the host trichotomy compares their pairs; the statement is a three-way sum of internal comparisons.

```agda
  tri : (a b : OT.Dom) → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
  tri a b = go (SQ.tri≺ K oκ (φ a) (φ b))
    where
    go : TriW (φ a ≺ₚ φ b) (φ a ≡ φ b) (φ b ≺ₚ φ a)
       → (a OT.≺ b) ⊎ ((a ≡ b) ⊎ (b OT.≺ a))
```

The three cases are read back through the backward transfer for the two strict cases, and through the injectivity of `φ` for the equality case: equal pairs name equal indices.

```agda
    go (lt h) = inl (≺-bwd a b h)
    go (eq e) = inr (inl (φ-inj a b e))
    go (gt h) = inr (inr (≺-bwd b a h))
```

Well-foundedness and transitivity construct the collapse and its order type.

```agda
  module C = OT.Conjuncts wf ≺-trans using (module Inj; col; col-ord; col-out; colTable; colTable-in; colTable-pair; colʟ; otL; otL-out)
  module I = C.Inj tri using (code; col-inj; module Inverse)
  injL-ot : InjL P C.otL
  injL-ot = ∣ C.colTable , I.code ∣₁
```

## Three counting facts

Trichotomy then makes the collapse map injective, so its graph witnesses an internal injection `P ↪ C.otL`.

```agda
incl : (a b : V ℓ) → ((z : V ℓ) → ⟨ z ∈ˢ a ⟩ → ⟨ z ∈ˢ b ⟩) → ⟪ a ⟫ ↪ ⟪ b ⟫
```

The counting lemmas begin on the ambient side. An inclusion of two ambient sets acts on the small presentations: each index of the subset names a member of the larger set, and the member's own fiber in the larger presentation names the corresponding index.

```agda
incl a b sub = ι , ι-inj
  where
  ι : ⟪ a ⟫ → ⟪ b ⟫
  ι m = fiber b (sub (⟪ a ⟫↪ m) (member a m)) .fst
  ι-inj : (m n : ⟪ a ⟫) → ι m ≡ ι n → m ≡ n
```

The induced map on indices is injective: if two indices of the subset name members that the larger presentation indexes identically, the equality of the namings forces an equality of the named members, and the subset's own injectivity returns the equality of indices.

```agda
  ι-inj m n e = ↪-inj {a = a}
    (sym (fiber b (sub (⟪ a ⟫↪ m) (member a m)) .snd)
     ∙ cong ⟪ b ⟫↪ e
     ∙ fiber b (sub (⟪ a ⟫↪ n) (member a n)) .snd)
opaque
```

A coded injection in `L` can be read externally: its graph conditions determine an injective map between the small presentations of its domain and codomain. Together with `ω ⊆ a` for every infinite ordinal `a`, this connects internal injections with ordinary cardinal comparisons.

```agda
  coded→ambient : (a b : S) → Σ[ F ∈ S ] InjCode F a b → ⟪ fst a ⟫ ↪ ⟪ fst b ⟫
  coded→ambient a b (F , sv , dm , ij , ran) = Sm.small , Sm.small-inj
    where module Sm = Small F a b sv dm ij ran
ω⊆ : (a : V ℓ) → IsOrd a → (⟨ a ∈ˢ ω ⟩ → Empty.⊥)
   → (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ a ⟩
```

Containment of `ω` follows from trichotomy at the ordinal `a`: `a` cannot belong to `ω` by the infinity hypothesis; `a` equal to `ω` transports the membership; and `ω` inside `a` transfers every membership by transitivity.

```agda
ω⊆ a oa a∉ω z z∈ω = go (ord-tri a oa ω ω-ord)
  where
  go : ⟨ a ∈ˢ ω ⟩ ⊎ ((a ≡ ω) ⊎ ⟨ ω ∈ˢ a ⟩) → ⟨ z ∈ˢ a ⟩
  go (inl h)         = Empty.rec (a∉ω h)
  go (inr (inl e))   = subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈ω
```

Its last case is transitivity applied to `z ∈ ω` and `ω ∈ a`. With containment in hand, the second counting fact is the exclusion: an infinite ordinal admits no internal injection into a member of `ω`, that is, into a finite ordinal.

```agda
  go (inr (inr ω∈a)) = oa .fst z∈ω ω∈a
no-fin : (a b : S) → IsOrd (fst a) → (⟨ fst a ∈ˢ ω ⟩ → Empty.⊥)
       → IsOrd (fst b) → ⟨ fst b ∈ˢ ω ⟩ → InjL a b → Empty.⊥
no-fin a b oa a∉ω ob b∈ω = PT.rec Empty.isProp⊥ (λ c →
  finite-excl-ω (fst b) ob b∈ω (λ x → h c x , h c x)
```

The final piece of the refutation quotes the containment of `ω` in `a`: since `ω ⊆ a`, the two lemmas compose, and an injection of `ω` into `b` would inject `ω` into the finite set `b` after passing through `a`. The inclusion map `ι` is fixed once in the where-clause.

```agda
    (λ x y e → ι .snd x y
       (coded→ambient a b c .snd (ι .fst x) (ι .fst y) (cong fst e))))
  where
  ι : ⟪ ω ⟫ ↪ ⟪ fst a ⟫
  ι = incl ω (fst a) (ω⊆ (fst a) oa a∉ω)
```

The map `h` evaluates the coded injection after the inclusion `ω ↪ a`.

```agda
  h : Σ[ F ∈ S ] InjCode F a b → ⟪ ω ⟫ → ⟪ fst b ⟫
  h c x = coded→ambient a b c .fst (ι .fst x)
```

## A coded injection lifts to the products

For the product construction, fix a graph `F` that is single-valued on `a`, has domain `a`, is injective, and takes its values in `b`; these are the four conditions of a coded injection `a ↪ b`.

```agda
module ProdMap (a b F : S)
               (sv : ⟨ (F ∷ a ∷ []) ⊨ svAt zero ⟩)
               (dm : ⟨ (F ∷ a ∷ []) ⊨ domAt zero (suc zero) ⟩)
```

The map `h` evaluates the coded injection after the inclusion `ω ↪ a`. For the product construction, fix a graph `F` that is single-valued on `a`, has domain `a`, is injective, and takes its values in `b`; these are the four conditions of a coded injection `a ↪ b`.

```agda
               (ij : ⟨ (F ∷ a ∷ []) ⊨ injAt zero ⟩)
               (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩
                    → ⟨ fst y ∈ fst b ⟩) where
```

The extraction module reads the actual function out of the graph: `toFun` computes the value at each domain element, `toFun-graph` certifies that the pair belongs to the graph, and `toFun-inj` transfers the graph's injectivity to the function.

```agda
  module E = Extract F a sv dm using (toFun; toFun-graph; toFun-inj)
```

Two predicates describe the objects in play. `Mem p` says that `p` is a member of the product `prodL a`; `Comp p` says that `p` decomposes into two members `x` and `y` of `a` whose ordered pair is exactly the underlying set of `p`.

```agda
  Mem : S → Type (ℓ-suc ℓ)
  Mem p = ⟨ fst p ∈ˢ fst (prodL a) ⟩
  Comp : S → Type (ℓ-suc ℓ)
  Comp p = Σ[ x ∈ S ] Σ[ y ∈ S ]
             (⟨ fst x ∈ˢ fst a ⟩ × ⟨ fst y ∈ˢ fst a ⟩ × (fst p ≡ pr (fst x) (fst y)))
```

The components of a product member are unique, and `isPropComp` proves it. The first projections are identified by the injectivity of the ordered pair; the second projections are then compared in the inner lemma.

```agda
  isPropComp : (p : S) → isProp (Comp p)
  isPropComp p (x , y , _ , _ , e) (x' , y' , _ , _ , e') =
    Σ≡Prop inner (Σ≡Prop (λ v → snd (isL v)) (pr-inj (sym e ∙ e') .fst))
    where
    inner : (x : S)
```

The inner lemma compares the second components: two candidates `y` and `y'` paired with the same first coordinate are equal, because the pair equation identifies their underlying sets with the same set, and the constructibility and membership components are propositions.

```agda
          → isProp (Σ[ y ∈ S ] (⟨ fst x ∈ˢ fst a ⟩ × ⟨ fst y ∈ˢ fst a ⟩
                                × (fst p ≡ pr (fst x) (fst y))))
    inner x (y , _ , _ , e) (y' , _ , _ , e') =
      Σ≡Prop (λ w → isProp× (snd (fst x ∈ˢ fst a))
                      (isProp× (snd (fst w ∈ˢ fst a)) (setIsSet _ _)))
```

The last component is discharged by the equality of underlying sets, and the uniqueness is complete: `Comp p` is a proposition, so its truncated existence can be eliminated into an honest decomposition.

```agda
        (Σ≡Prop (λ v → snd (isL v)) (pr-inj (sym e ∙ e') .snd))
```

The reader `comp` turns the truncated membership of the product into an honest decomposition, and the uniqueness just proved is what licenses the elimination. The value map `val` then computes, at each member `x` of `a`, the element that the coded injection `F` assigns to it.

```agda
  comp : (p : S) → Mem p → Comp p
  comp p mp = PT.rec (isPropComp p) (λ z → z) (prodL-out a p mp)
  opaque
    val : (x : S) → ⟨ fst x ∈ˢ fst a ⟩ → S
    val x mx = E.toFun (x , mx)
```

The graph lemma certifies that the computed value is paired with its input inside the graph: the ordered pair of `x` and `val x` belongs to `F`. This is the record of the assignment, kept for every member of `a`.

```agda
    val-graph : (x : S) (mx : ⟨ fst x ∈ˢ fst a ⟩)
              → ⟨ pr (fst x) (fst (val x mx)) ∈ fst F ⟩
    val-graph x mx = E.toFun-graph (x , mx)
```

The injectivity lemma transfers the graph's injectivity to the computed values: if two members of `a` receive values with equal underlying sets, the members themselves are equal. This is what will make the lifted map on pairs injective.

```agda
    val-inj : (x : S) (mx : ⟨ fst x ∈ˢ fst a ⟩) (x' : S) (mx' : ⟨ fst x' ∈ˢ fst a ⟩)
            → fst (val x mx) ≡ fst (val x' mx') → fst x ≡ fst x'
    val-inj x mx x' mx' = E.toFun-inj ij (x , mx) (x' , mx')
```

The lifted map `fn` acts on a member of the product by applying `F` coordinatewise: the internal ordered pair of the image of the first coordinate and the image of the second.

```agda
  fn : (p : S) → Mem p → S
  fn p mp = prʟ (val (comp p mp .fst) (comp p mp .snd .snd .fst))
                (val (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst))
```

The image lands in the product over `b`: both component values are members of `b` by the range clause, so their internal pair belongs to `prodL b`. The identification of the internal and ambient pairs is transported along its own first-projection lemma.

```agda
  into : (p : S) (mp : Mem p) → ⟨ fst (fn p mp) ∈ˢ fst (prodL b) ⟩
  into p mp =
    subst (λ w → ⟨ w ∈ˢ fst (prodL b) ⟩) (sym (prʟ-fst (val x mx) (val y my)))
      (prodL-in b (val x mx) (val y my)
        (ran x (val x mx) (val-graph x mx)) (ran y (val y my) (val-graph y my)))
```

A decomposition of `p` supplies coordinates `x,y` together with proofs `x ∈ a` and `y ∈ a`. These membership proofs are part of the data because `val` is defined only on members of `a`.

```agda
    where
    x = comp p mp .fst
    y = comp p mp .snd .fst
    mx = comp p mp .snd .snd .fst
    my = comp p mp .snd .snd .snd .fst
```

The chain type assembles what the graph formula must witness: `p` is the pair of `x` and `y`, `q` is the pair of `x'` and `y'`, and the graph of `F` contains the pairs of the two first coordinates and of the two second coordinates.

```agda
  Chain : S → S → S → S → S → S → Type (ℓ-suc ℓ)
  Chain q p x y x' y' =
      (fst p ≡ pr (fst x) (fst y)) × (fst q ≡ pr (fst x') (fst y'))
    × ⟨ pr (fst x) (fst x') ∈ fst F ⟩ × ⟨ pr (fst y) (fst y') ∈ fst F ⟩
```

The graph formula `mapFo` existentially chooses `x,y,x',y'` and conjoins four assertions: `p=(x,y)`, `q=(x',y')`, and the two applications of `F`.

```agda
  opaque
    mapFo : Formula S 2
    mapFo = ∃̇ (∃̇ (∃̇ (∃̇ (
          prAtL i5 i3 i2
       ∧̇ (prAtL i4 i1 i0
```

The last two atoms are the application clauses: the graph of `F` contains the pairs of the first coordinates and of the second coordinates, which is precisely the statement that `F` maps `x` to `x'` and `y` to `y'`.

```agda
       ∧̇ (appC F i3 i1
       ∧̇ appC F i2 i0))))))
```

Adequacy is checked against the six-entry context that adds the four witnesses, newest first, followed by the pair `q` and the pair `p`: slot zero is `y'`, slot five is `p`, matching the indices of the four atoms.

```agda
    private
      env₄ : S → S → S → S → S → S → S ^ 6
      env₄ q p x y x' y' = y' ∷ x' ∷ y ∷ x ∷ q ∷ p ∷ []
```

The first adequacy lemma reads the pair atom for `p`: satisfaction of the pairing atom at the context is the equation between the underlying set of `p` and the ordered pair of `x` and `y`.

```agda
      at1 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ prAtL i5 i3 i2 ⟩ ≡ (fst p ≡ pr (fst x) (fst y))
      at1 q p x y x' y' = cong ⟨_⟩ (prAtL-adequate i5 i3 i2 (env₄ q p x y x' y'))
```

The second adequacy lemma does the same for `q`, against the witnesses `x'` and `y'`. The two equations anchor the pair part of the chain.

```agda
      at2 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ prAtL i4 i1 i0 ⟩ ≡ (fst q ≡ pr (fst x') (fst y'))
      at2 q p x y x' y' = cong ⟨_⟩ (prAtL-adequate i4 i1 i0 (env₄ q p x y x' y'))
```

The third adequacy lemma reads the first application atom: satisfaction in `L` is identified with the ambient membership of the pair of the two first coordinates in the graph of `F`.

```agda
      at3 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ appC F i3 i1 ⟩ ≡ ⟨ pr (fst x) (fst x') ∈ fst F ⟩
      at3 q p x y x' y' = cong ⟨_⟩ (appC-adequate F i3 i1 (env₄ q p x y x' y'))
```

The fourth does the same for the second coordinates, completing the translation of all four atoms into ordinary statements about members of sets.

```agda
      at4 : (q p x y x' y' : S)
          → ⟨ env₄ q p x y x' y' ⊨ appC F i2 i0 ⟩ ≡ ⟨ pr (fst y) (fst y') ∈ fst F ⟩
      at4 q p x y x' y' = cong ⟨_⟩ (appC-adequate F i2 i0 (env₄ q p x y x' y'))
```

The outward direction consumes the four nested existentials in turn and assembles the truncated chain: four witnesses with all four atoms transported to their ambient readings.

```agda
    mapFo-out : (q p : S) → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩
              → ∥ Σ[ x ∈ S ] Σ[ y ∈ S ] Σ[ x' ∈ S ] Σ[ y' ∈ S ] Chain q p x y x' y' ∥₁
    mapFo-out q p = PT.rec squash₁ (λ { (x , hx) → PT.rec squash₁ (λ { (y , hy) →
      PT.rec squash₁ (λ { (x' , hx') → PT.map (λ { (y' , (h1 , (h2 , (h3 , h4)))) →
        x , y , x' , y'
```

Each atom is transported along its own adequacy path, so the chain records ordinary equations and ordinary memberships rather than satisfaction judgments.

```agda
        , ( transport (at1 q p x y x' y') h1 , transport (at2 q p x y x' y') h2
          , transport (at3 q p x y x' y') h3 , transport (at4 q p x y x' y') h4 ) })
        hx' }) hy }) hx })
```

The inward direction rebuilds the formula from the chain. The four witnesses are entered as the nested existentials, and the four atoms are transported along the adequacy paths in the reverse direction.

```agda
    mapFo-in : (q p x y x' y' : S) → Chain q p x y x' y' → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩
    mapFo-in q p x y x' y' (h1 , h2 , h3 , h4) =
      ∣ x , ∣ y , ∣ x' , ∣ y'
      , ( transport (sym (at1 q p x y x' y')) h1
        , ( transport (sym (at2 q p x y x' y')) h2
```

The last two application atoms complete the nested conjunction of the four assertions, and hence complete the witness for `mapFo`.

```agda
        , ( transport (sym (at3 q p x y x' y')) h3
          , transport (sym (at4 q p x y x' y')) h4 ))) ∣₁ ∣₁ ∣₁ ∣₁
```

Uniqueness says that the graph formula determines the value: any `q` paired with `p` in the graph equals the canonical image `fn p mp`. The proof consumes the truncated chain into the pair equation, the goal being an equation in an h-set.

```agda
  only : (p : S) (mp : Mem p) (q : S) → ⟨ (q ∷ p ∷ []) ⊨ mapFo ⟩ → q ≡ fn p mp
  only p mp q h = PT.rec (isSetS q (fn p mp)) step (mapFo-out q p h)
    where
    x = comp p mp .fst
    y = comp p mp .snd .fst
```

The four components of the member `p` are named once, as in the image lemma, so the uniqueness computation can refer to them directly.

```agda
    mx = comp p mp .snd .snd .fst
    my = comp p mp .snd .snd .snd .fst
    e = comp p mp .snd .snd .snd .snd
```

The chain equation writes `q` as `(x₁',y₁')`, while the fixed decomposition writes `p` as `(x,y)`. Single-valuedness identifies `x₁'` with `val x` and `y₁'` with `val y`, so `q` is the canonical image `(val x,val y)`.

```agda
    step : Σ[ x₁ ∈ S ] Σ[ y₁ ∈ S ] Σ[ x₁' ∈ S ] Σ[ y₁' ∈ S ] Chain q p x₁ y₁ x₁' y₁'
         → q ≡ fn p mp
    step (x₁ , y₁ , x₁' , y₁' , (e₁ , e₂ , h3 , h4)) =
      Σ≡Prop (λ v → snd (isL v))
        (e₂ ∙ cong₂ pr ex ey ∙ sym (prʟ-fst (val x mx) (val y my)))
```

The injectivity of the ordered pair splits the pair equation into two: the underlying set of `x₁` equals that of `x`, and the underlying set of `y₁` equals that of `y`.

```agda
      where
      x₁≡x : fst x₁ ≡ fst x
      x₁≡x = pr-inj (sym e₁ ∙ e) .fst
      y₁≡y : fst y₁ ≡ fst y
      y₁≡y = pr-inj (sym e₁ ∙ e) .snd
```

The two graph memberships are then read through the single-valuedness of `F`: an entry paired with `x₁`, once `x₁` is known to name `x`, must agree with the recorded value `val x mx` on its first projection.

```agda
      ex : fst x₁' ≡ fst (val x mx)
      ex = svAt-out zero (F ∷ a ∷ []) sv x x₁' (val x mx)
             (subst (λ w → ⟨ pr w (fst x₁') ∈ fst F ⟩) x₁≡x h3) (val-graph x mx)
      ey : fst y₁' ≡ fst (val y my)
      ey = svAt-out zero (F ∷ a ∷ []) sv y y₁' (val y my)
```

The second coordinate is treated identically, with its own membership and its own recorded value.

```agda
             (subst (λ w → ⟨ pr w (fst y₁') ∈ fst F ⟩) y₁≡y h4) (val-graph y my)
```

Thus `mapFo` defines the coordinatewise image `fn`: every product member has that graph value, and `into` places the value in `prodL b`.

```agda
  M : DefinableMap
  M = record
    { dom = prodL a ; cod = prodL b ; fn = fn ; into = into ; graph = mapFo
    ; defines = λ p mp →
        mapFo-in (fn p mp) p (comp p mp .fst) (comp p mp .snd .fst)
```

The defining clause is the chain, instantiated at the canonical image of `p`: the two values, the pair equation of the product member, and the two graph lemmas certify that the graph holds of the image and its input.

```agda
          (val (comp p mp .fst) (comp p mp .snd .snd .fst))
          (val (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst))
          ( comp p mp .snd .snd .snd .snd
          , prʟ-fst _ _
          , val-graph (comp p mp .fst) (comp p mp .snd .snd .fst)
```

The uniqueness theorem shows that no second graph value is possible, so the formula represents an actual function on `prodL a`.

```agda
          , val-graph (comp p mp .snd .fst) (comp p mp .snd .snd .snd .fst) )
    ; only = only }
```

Injectivity of the lifted map is proved directly. Two product members whose images agree as underlying sets must themselves agree, and the proof reassembles each member from its components.

```agda
  inj : (p : S) (mp : Mem p) (p' : S) (mp' : Mem p')
      → fst (fn p mp) ≡ fst (fn p' mp') → fst p ≡ fst p'
  inj p mp p' mp' e = e₀ ∙ cong₂ pr ex ey ∙ sym e₀'
    where
    x = comp p mp .fst
```

The components of both members are named once, so the two decompositions can be compared coordinate by coordinate.

```agda
    y = comp p mp .snd .fst
    mx = comp p mp .snd .snd .fst
    my = comp p mp .snd .snd .snd .fst
    e₀ = comp p mp .snd .snd .snd .snd
    x' = comp p' mp' .fst
```

The assumed equality of images is an equality of internal pairs; its injectivity splits it into the equality of the two first images and the equality of the two second images.

```agda
    y' = comp p' mp' .snd .fst
    mx' = comp p' mp' .snd .snd .fst
    my' = comp p' mp' .snd .snd .snd .fst
    e₀' = comp p' mp' .snd .snd .snd .snd
    q : (fst (val x mx) ≡ fst (val x' mx')) × (fst (val y my) ≡ fst (val y' my'))
```

Each component equality is fed to the injectivity of the value map, yielding first coordinates equal and second coordinates equal; the two coordinates of the pair equation are then transported along these.

```agda
    q = pr-inj (sym (prʟ-fst (val x mx) (val y my)) ∙ e ∙ prʟ-fst (val x' mx') (val y' my'))
    ex : fst x ≡ fst x'
    ex = val-inj x mx x' mx' (fst q)
    ey : fst y ≡ fst y'
    ey = val-inj y my y' my' (snd q)
```

The definable map and its injectivity assemble into the internal injection: `prodL a` injects into `prodL b` inside `L`.

```agda
  injL : InjL (prodL a) (prodL b)
  injL = Inj.injL M inj
```

Because `InjL` is propositionally truncated, a coded injection `a ↪ b` may be lifted without choosing its graph globally.

```agda
prod-inj : (a b : S) → InjL a b → InjL (prodL a) (prodL b)
prod-inj a b = PT.rec squash₁
  (λ { (F , sv , dm , ij , ran) → ProdMap.injL a b F sv dm ij ran })
```

## The theorem

To absorb the extra top element of an infinite ordinal, it remains to inject its successor back into the ordinal.

```agda
module Shift (mL : S) (om : IsOrd (fst mL)) (m∉ω : ⟨ fst mL ∈ˢ ω ⟩ → Empty.⊥) where
```

Write `m` for the underlying ordinal of `mL`. Membership and finiteness decisions concern this set, while `mL` retains the evidence that it is an element of `L`.

```agda
  private
    m : V ℓ
    m = fst mL
```

The domain of the shift is the internal successor `D = sucʟ mL`: the successor of the ordinal inside `L`, which contains both the members of `m` and `m` itself.

```agda
    D : S
    D = sucʟ mL
```

Equality of two elements of `L` is equality of their underlying sets, since the constructibility components are propositions. This small equation is used at every identification inside the shift.

```agda
    S≡ : {x y : S} → fst x ≡ fst y → x ≡ y
    S≡ = Σ≡Prop (λ v → snd (isL v))
```

Since `m` is infinite, every member of `ω` belongs to `m`; the containment is quoted from the counting facts and is the reason the successor of a finite member stays inside `m`.

```agda
    ω⊆m : (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ m ⟩
    ω⊆m = ω⊆ m om m∉ω
```

Membership in the shift's domain is stated, and the first decision is defined: an element is either a member of `ω` or the membership is refuted. The disjunction is a genuine case split, delivered by excluded middle.

```agda
    Mem : S → Type (ℓ-suc ℓ)
    Mem x = ⟨ fst x ∈ˢ fst D ⟩
    Fin? : S → Type (ℓ-suc ℓ)
    Fin? x = ⟨ fst x ∈ˢ ω ⟩ ⊎ (⟨ fst x ∈ˢ ω ⟩ → Empty.⊥)
```

The second decision separates the members of the successor: an element of `sucʟ mL` is either a member of `m` or equal to `m`, which is exactly what membership in a successor means.

```agda
    Top? : S → Type (ℓ-suc ℓ)
    Top? x = ⟨ fst x ∈ˢ m ⟩ ⊎ (fst x ≡ m)
```

The first decision is an instance of excluded middle, applied to the membership proposition of `x` in `ω`.

```agda
    fin? : (x : S) → Fin? x
    fin? x = lem (fst x ∈ˢ ω)
```

The second decision is also an instance of excluded middle, refined by the successor's elimination: a member of `sucʟ mL` is either a member of `m` or equal to `m`, so a refuted membership leaves only equality.

```agda
    top? : (x : S) → Mem x → Top? x
    top? x h = go (lem (fst x ∈ˢ m))
      where
      go : ⟨ fst x ∈ˢ m ⟩ ⊎ (⟨ fst x ∈ˢ m ⟩ → Empty.⊥) → Top? x
      go (inl k)  = inl k
```

In the refuted case the elimination consumes the truncated membership in the successor, and the two outcomes are exclusive: an element cannot both belong to `m` and equal `m`, since that would make `m` a member of itself, refuted by the irreflexivity of membership.

```agda
      go (inr nk) = inr (∈sucV-elim {A = m} {x = fst x} (setIsSet (fst x) m)
        (subst (λ w → ⟨ fst x ∈ˢ w ⟩) (sucʟ-fst mL) h) (λ k → Empty.rec (nk k)) (λ q → q))
    not-both : (x : S) → ⟨ fst x ∈ˢ m ⟩ → fst x ≡ m → Empty.⊥
    not-both x k q = ∈-irrefl m (subst (λ w → ⟨ w ∈ˢ m ⟩) q k)
```

The finite and top cases cannot overlap. If `x` belongs to `ω` and equals `m`, transporting its membership along that equality would put `m` in `ω`, contrary to the hypothesis that `m` is infinite.

```agda
    ω-fin : (x : S) → ⟨ fst x ∈ˢ ω ⟩ → fst x ≡ m → Empty.⊥
    ω-fin x k q = m∉ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) q k)
```

A successor can never be empty. Indeed, `a` belongs to `sucV a`; if `sucV a = ∅`, transporting this membership would produce an element of the empty set.

```agda
    suc≢∅ : (a : V ℓ) → sucV a ≡ ∅ → Empty.⊥
    suc≢∅ a e = ∅-empty a
      (∈∈ₛ {a = a} {b = ∅} .fst (subst (λ w → ⟨ a ∈ˢ w ⟩) e (self∈sucV a)))
```

The three cases now define the value of the shift. A finite member is sent to its internal successor; a non-finite member of `m` is sent to itself; and the top element `m` is sent to the empty set of `L`. These are precisely the three alternatives the decisions distinguish.

```agda
    value : (x : S) → Fin? x → Top? x → S
    value x (inl _) _       = sucʟ x
    value x (inr _) (inl _) = x
    value x (inr _) (inr _) = ∅ʟ
```

The value is guaranteed to lie in `m`. For a finite member, its successor is a member of `ω` by the limit property, and `ω` is contained in `m`; for a member of `m` the membership is the decision itself; and the empty set is a member of `ω`, hence of `m`.

```agda
    value-in : (x : S) (f : Fin? x) (t : Top? x) → ⟨ fst (value x f t) ∈ˢ m ⟩
    value-in x (inl k) _ =
      subst (λ w → ⟨ w ∈ˢ m ⟩) (sym (sucʟ-fst x)) (ω⊆m (sucV (fst x)) (ω-limit (fst x) k))
    value-in x (inr _) (inl k) = k
    value-in x (inr _) (inr _) = ω⊆m ∅ (#∈ω zero)
```

The witness type for the graph formula is declared: either `x` is finite and `y` is its successor, or `x` is not finite, lies in `m`, and `y` equals `x`, or `x` equals the top `m` and `y` is empty. The three alternatives are truncated, and each carries its own memberships and equations.

```agda
    Wit : (y x : S) → Type (ℓ-suc ℓ)
    Wit y x = ∥ (⟨ fst x ∈ˢ ω ⟩ × (fst y ≡ sucV (fst x)))
              ⊎ ( ((⟨ fst x ∈ˢ ω ⟩ → Empty.⊥) × ⟨ fst x ∈ˢ m ⟩ × (fst y ≡ fst x))
                ⊎ ((fst x ≡ m) × (fst y ≡ ∅)) ) ∥₁
```

The graph formula is stated in the object language, and its first disjunct says that `x` is a member of the internal `ω` and `y` is its successor, read by the successor clause. The second disjunct begins by denying that `x` is finite.

```agda
  opaque
    graph : Formula S 2
    graph = ((var (suc zero) ∈̇ con ωʟ) ∧̇ sucAtL (suc zero) zero)
          ∨̇ ( ( (¬̇ (var (suc zero) ∈̇ con ωʟ))
              ∧̇ ((var (suc zero) ∈̇ con mL) ∧̇ (var zero ≐ var (suc zero))) )
```

The two guarded alternatives inside complete the second and third disjuncts: a non-finite member of `m` is paired with itself, and the top element is paired with the empty set of `L`.

```agda
            ∨̇ ((var (suc zero) ≐ con mL) ∧̇ (var zero ≐ con ∅ʟ)) )
```

The adequacy of the successor clause is recorded once: satisfaction of the successor atom at the two-entry context is the equation between `y` and the ambient successor of `x`.

```agda
    private
      sa : (y x : S) → ⟨ (y ∷ x ∷ []) ⊨ sucAtL (suc zero) zero ⟩ ≡ (fst y ≡ sucV (fst x))
      sa y x = cong ⟨_⟩ (sucAtL-adequate (suc zero) zero (y ∷ x ∷ []))
```

Reading the formula outward eliminates the truncated disjunction into the propositional witness type. The successor clause is converted by adequacy, while propositional resizing lowers the refutation in the middle clause from its lifted universe; the top clause already has the required form.

```agda
    graph-out : (y x : S) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → Wit y x
    graph-out y x = PT.rec squash₁
      (λ { (inl (k , e)) → ∣ inl (k , transport (sa y x) e) ∣₁
         ; (inr h) → PT.map (λ { (inl (n , (k , e))) →
                                  inr (inl ((λ hx → lower (n hx)) , k , e))
```

The third disjunct carries only the two equations of the top case, so its translation is direct.

```agda
                              ; (inr (q , e)) → inr (inr (q , e)) }) h })
```

The three inward lemmas rebuild the formula from each kind of witness. For a finite member, the successor equation is transported back along the adequacy into the first disjunct.

```agda
    in-fin : (y x : S) → ⟨ fst x ∈ˢ ω ⟩ → fst y ≡ sucV (fst x) → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
    in-fin y x k e = ∣ inl (k , transport (sym (sa y x)) e) ∣₁
```

For a non-finite member of `m`, the refutation of `x ∈ ω` is lifted into the object-level negation. Together with `x ∈ m` and `y = x`, it supplies the middle disjunct.

```agda
    in-mid : (y x : S) → (⟨ fst x ∈ˢ ω ⟩ → Empty.⊥) → ⟨ fst x ∈ˢ m ⟩ → fst y ≡ fst x
           → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
    in-mid y x n k e = ∣ inr ∣ inl ((λ hx → lift (n hx)) , (k , e)) ∣₁ ∣₁
```

For the top element, the two equations of the top case are assembled directly into the third disjunct.

```agda
    in-top : (y x : S) → fst x ≡ m → fst y ≡ ∅ → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩
    in-top y x q e = ∣ inr ∣ inr (q , e) ∣₁ ∣₁
```

The shift function is now defined through the two decisions: the value is the successor, the element itself, or the empty set, according to how the decisions classify the input.

```agda
  private
    fn : (x : S) → Mem x → S
    fn x h = value x (fin? x) (top? x h)
```

The defining clause is verified in all three cases: the finite case quotes the successor equation, the middle case is definitional, and the top case pairs the empty set with the top element.

```agda
    defines' : (x : S) (f : Fin? x) (t : Top? x) → ⟨ (value x f t ∷ x ∷ []) ⊨ graph ⟩
    defines' x (inl k) _       = in-fin (sucʟ x) x k (sucʟ-fst x)
    defines' x (inr n) (inl k) = in-mid x x n k refl
    defines' x (inr n) (inr q) = in-top ∅ʟ x q refl
```

Uniqueness reads the graph backwards: any `y` paired with `x` in the graph equals the chosen value. The proof consumes the truncated disjunction into the equality goal, which is an equation in an h-set.

```agda
    only' : (x : S) (f : Fin? x) (t : Top? x) (y : S)
          → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ value x f t
    only' x f t y hy = PT.rec (isSetS y (value x f t)) (go f t) (graph-out y x hy)
      where
      go : (f : Fin? x) (t : Top? x)
```

The case function receives the unpacked alternatives together with the chosen decisions. In the finite case with the finite affirmation, the successor equation and the internal pairing equation agree after transporting along the successor's first-projection identification.

```agda
         → (⟨ fst x ∈ˢ ω ⟩ × (fst y ≡ sucV (fst x)))
           ⊎ ( ((⟨ fst x ∈ˢ ω ⟩ → Empty.⊥) × ⟨ fst x ∈ˢ m ⟩ × (fst y ≡ fst x))
             ⊎ ((fst x ≡ m) × (fst y ≡ ∅)) )
         → y ≡ value x f t
      go (inl k) _       (inl (_ , e))             = S≡ (e ∙ sym (sucʟ-fst x))
```

The next five clauses compare the chosen finite or non-finite member case with a graph witness. A finite choice contradicts either the middle witness's refutation or the top equation; a non-finite member choice contradicts a finite witness, agrees with a middle witness by its equation, and excludes a top witness because a member of `m` cannot equal `m`.

```agda
      go (inl k) _       (inr (inl (n , _ , _)))   = Empty.rec (n k)
      go (inl k) _       (inr (inr (q , _)))       = Empty.rec (ω-fin x k q)
      go (inr n) (inl k) (inl (k' , _))            = Empty.rec (n k')
      go (inr n) (inl k) (inr (inl (_ , _ , e)))   = S≡ e
      go (inr n) (inl k) (inr (inr (q , _)))       = Empty.rec (not-both x k q)
```

If the chosen input is the top element, a finite witness contradicts its non-finiteness, and a middle witness contradicts the fact that an element of `m` cannot equal `m`. A top witness gives the required equality directly from its empty-value equation.

```agda
      go (inr n) (inr q) (inl (k' , _))            = Empty.rec (n k')
      go (inr n) (inr q) (inr (inl (_ , k , _)))   = Empty.rec (not-both x k q)
      go (inr n) (inr q) (inr (inr (_ , e)))       = S≡ e
```

These data determine a definable function from `sucʟ mL` to `mL`: every input receives the chosen shift value in `m`, and the displayed formula is its graph.

```agda
    M : DefinableMap
    M = record
      { dom = D ; cod = mL ; fn = fn
      ; into = λ x h → value-in x (fin? x) (top? x h)
      ; graph = graph
```

Excluded middle supplies the two decisions for each input. The preceding existence and uniqueness arguments then show that the graph holds exactly at the selected value.

```agda
      ; defines = λ x h → defines' x (fin? x) (top? x h)
      ; only = λ x h → only' x (fin? x) (top? x h) }
```

Injectivity is proved by comparing the cases for two inputs. If both are finite, equality of their shifted values is equality of their successors, so injectivity of ordinal successor identifies the original ordinals.

```agda
    inj' : (x : S) (f : Fin? x) (t : Top? x) (x' : S) (f' : Fin? x') (t' : Top? x')
         → fst (value x f t) ≡ fst (value x' f' t') → fst x ≡ fst x'
    inj' x (inl k) _ x' (inl k') _ e =
      ord-suc-inj (fst x) (fst x') (mem-ord {A = ω} ω-ord (fst x) k)
        (sym (sucʟ-fst x) ∙ e ∙ sucʟ-fst x')
```

A finite input cannot share its shifted value with a non-finite member: that equality would put the latter's value, and hence the latter itself, in `ω`. Nor can it share its value with the top input, because that would equate a successor with the empty set.

```agda
    inj' x (inl k) _ x' (inr n') (inl _) e =
      Empty.rec (n' (subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym (sucʟ-fst x) ∙ e) (ω-limit (fst x) k)))
    inj' x (inl k) _ x' (inr n') (inr _) e =
      Empty.rec (suc≢∅ (fst x) (sym (sucʟ-fst x) ∙ e))
    inj' x (inr n) (inl _) x' (inl k') _ e =
```

The reverse finite/non-finite case gives the same contradiction. Two non-finite members with equal values are equal immediately, while a non-finite member cannot share the top value: equality with the empty set would make it a member of `ω`.

```agda
      Empty.rec (n (subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym (sucʟ-fst x') ∙ sym e) (ω-limit (fst x') k')))
    inj' x (inr n) (inl _) x' (inr n') (inl _) e = e
    inj' x (inr n) (inl _) x' (inr n') (inr _) e =
      Empty.rec (n (subst (λ w → ⟨ w ∈ˢ ω ⟩) (sym e) (#∈ω zero)))
    inj' x (inr n) (inr _) x' (inl k') _ e =
```

For a top input, equality with a finite value would again make a successor empty, and equality with a non-finite member's value would make that member equal to the empty set and hence finite. If both inputs are top, their equations with `m` identify them. Thus the shift is internally injective.

```agda
      Empty.rec (suc≢∅ (fst x') (sym (sucʟ-fst x') ∙ sym e))
    inj' x (inr n) (inr _) x' (inr n') (inl _) e =
      Empty.rec (n' (subst (λ w → ⟨ w ∈ˢ ω ⟩) e (#∈ω zero)))
    inj' x (inr n) (inr q) x' (inr n') (inr q') e = q ∙ sym q'
  injL : InjL (sucʟ mL) mL
```

The definable shift and the preceding case analysis give the coded injection `sucʟ mL ↪ mL`. We will also use the elementary fact that two members of a set represented by the same fiber index are equal: applying the presentation map to the index equality recovers equality of the represented members.

```agda
  injL = Inj.injL M (λ x h x' h' → inj' x (fin? x) (top? x h) x' (fin? x') (top? x' h'))
opaque
  fiber-inj : (g : V ℓ) {x y : V ℓ} (mx : ⟨ x ∈ˢ g ⟩) (my : ⟨ y ∈ˢ g ⟩)
            → fiber g mx .fst ≡ fiber g my .fst → x ≡ y
  fiber-inj g mx my e = sym (fiber g mx .snd) ∙ cong ⟪ g ⟫↪ e ∙ fiber g my .snd
```

For each constructible infinite ordinal `a` that is an internal cardinal, the induction goal is a coded injection from its Cartesian square `a × a` back into `a`. Packaging the statement as `Goal a` lets membership induction apply it uniformly below `a`.

```agda
Goal : V ℓ → Type (ℓ-suc ℓ)
Goal a = (la : ⟨ isL a ⟩) → IsOrd a → IsCardinalL (a , la)
       → (⟨ a ∈ˢ ω ⟩ → Empty.⊥) → InjL (prodL (a , la)) (a , la)
```

The induction step receives the set `a`, the induction hypothesis for every member of `a`, and the four hypotheses: constructibility, ordinality, internal cardinality, and infinity. The cardinality hypothesis is the exclusion of internal injections of `κ` into its own members, the form in which the collapse counting will be used.

```agda
module Step (a : V ℓ) (ih : (a' : V ℓ) → ⟨ a' ∈ˢ a ⟩ → Goal a')
            (la : ⟨ isL a ⟩) (oa : IsOrd a) (carda : IsCardinalL (a , la))
            (a∉ω : ⟨ a ∈ˢ ω ⟩ → Empty.⊥) where
```

Write `κ` for the constructible set whose underlying ordinal is `a`. This keeps the ambient ordinal data and the proof that it belongs to `L` together whenever an internal construction is formed.

```agda
  κ : S
  κ = a , la
```

We now consider `κ × κ` with its Gödel order and the ordinal obtained by collapsing that well-order. The task is to show that every initial segment of this collapse is still bounded below `κ`.

```agda
  open Order κ oa
  open Coll κ oa
```

Since the ordinal `a` is not finite, it contains every finite ordinal. We also need closure under successor: for `m ∈ a`, trichotomy places `sucV m` below, equal to, or above `a`; the next cases rule out the latter two possibilities.

```agda
  ω⊆a : (z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ a ⟩
  ω⊆a = ω⊆ a oa a∉ω
  suc∈ : (m : V ℓ) → ⟨ m ∈ˢ a ⟩ → ⟨ sucV m ∈ˢ a ⟩
  suc∈ m m∈a = go (ord-tri (sucV m) (suc-ord om) a oa)
    where
```

Because `m` is a member of the ordinal `a`, it is itself an ordinal. Its constructibility follows from membership in the constructible set `a`, so `m` determines an element `mL` of the internal universe.

```agda
    om : IsOrd m
    om = mem-ord {A = a} oa m m∈a
    mL : S
    mL = ordL m om
```

Apply trichotomy to `sucV m` and `a`. The first case is exactly the desired membership. If `sucV m = a`, comparing `m` with `ω` splits the contradiction into the finite case and the two infinite cases handled next.

```agda
    go : ⟨ sucV m ∈ˢ a ⟩ ⊎ ((sucV m ≡ a) ⊎ ⟨ a ∈ˢ sucV m ⟩) → ⟨ sucV m ∈ˢ a ⟩
    go (inl h) = h
    go (inr (inl e)) = Empty.rec (fin (ord-tri m om ω ω-ord))
      where
      fin : ⟨ m ∈ˢ ω ⟩ ⊎ ((m ≡ ω) ⊎ ⟨ ω ∈ˢ m ⟩) → Empty.⊥
```

If `m` were a member of `ω`, its successor would also be a member of `ω`, putting the cardinal `a` inside `ω` against the infinity hypothesis. If instead `m` equals `ω` or contains it, the internal cardinality of `a`, applied at the member `m`, would refute the shift injection `sucʟ mL ↪ mL`, an internal injection into a member of the cardinal.

```agda
      fin (inl m∈ω) = a∉ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) e (ω-limit m m∈ω))
      fin (inr r) =
        carda mL m∈a (subst (λ w → InjL w mL) sucL≡κ (Shift.injL mL om m∉ω))
        where
        m∉ω : ⟨ m ∈ˢ ω ⟩ → Empty.⊥
```

The local non-finiteness is read off the same trichotomy: if `m` equalled `ω`, the assumed membership would place `ω` inside itself; if `ω` belonged to `m`, transitivity would again place `ω` inside itself. Both contradict the irreflexivity of membership.

```agda
        m∉ω h = rr r
          where
          rr : (m ≡ ω) ⊎ ⟨ ω ∈ˢ m ⟩ → Empty.⊥
          rr (inl e') = ∈-irrefl ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) e' h)
          rr (inr ω∈m) = ∈-irrefl ω (ω-ord .fst ω∈m h)
```

The equality `sucV m = a` identifies the internal successor `sucʟ mL` with `κ`, so the shift would give the injection into `m` forbidden by cardinality. In the remaining trichotomy case, `a ∈ sucV m` means either `a ∈ m` or `a = m`; each alternative yields self-membership of an ordinal and is therefore impossible.

```agda
        sucL≡κ : sucʟ mL ≡ κ
        sucL≡κ = Σ≡Prop (λ v → snd (isL v)) (sucʟ-fst mL ∙ e)
    go (inr (inr h)) = Empty.rec*
      (∈sucV-elim {A = m} {x = a} {P = Empty.⊥* {ℓ-suc ℓ}} Empty.isProp⊥* h
        (λ a∈m → lift (∈-irrefl a (oa .fst a∈m m∈a)))
```

Successor closure now makes the induction hypothesis available at the smaller ordinals needed below. More generally, if an infinite ordinal `γ` lies below `a`, choose an internal cardinal representative of `γ`; the induction hypothesis at that representative will yield an injection `prodL γ ↪ γ`.

```agda
        (λ a≡m → lift (∈-irrefl m (subst (λ w → ⟨ m ∈ˢ w ⟩) a≡m m∈a))))
  prod-into : (γ : S) → IsOrd (fst γ) → ⟨ fst γ ∈ˢ a ⟩
            → (⟨ fst γ ∈ˢ ω ⟩ → Empty.⊥) → InjL (prodL γ) γ
  prod-into γ oγ γ∈a γ∉ω = PT.rec squash₁ build (cardOf γ oγ)
    where
```

The cardinal representative delivers its data in truncated form: an ordinal `μ` that is an internal cardinal, contained in `γ`, with `γ` injecting into it and it into `γ`. The build function turns this data into the product injection.

```agda
    build : Σ[ μ ∈ S ]
              ( IsOrd (fst μ) × IsCardinalL μ
              × ((z : V ℓ) → ⟨ z ∈ˢ fst μ ⟩ → ⟨ z ∈ˢ fst γ ⟩)
              × InjL γ μ × InjL μ γ )
          → InjL (prodL γ) γ
```

The injection composes three injections. The product injection lifts `γ ↪ μ` coordinatewise; the induction hypothesis applies at the internal cardinal `μ`, giving `prodL μ ↪ μ`; and `μ ↪ γ` composes the result down into `γ`.

```agda
    build (μ , oμ , cardμ , μ⊆γ , γ↪μ , μ↪γ) =
      injl-trans (prodL γ) (prodL μ) γ (prod-inj γ μ γ↪μ)
        (injl-trans (prodL μ) μ γ (ih (fst μ) μ∈a (snd μ) oμ cardμ μ∉ω) μ↪γ)
      where
      μ∈a : ⟨ fst μ ∈ˢ a ⟩
```

The representative `μ` also lies below `a`. If `μ ∈ γ`, transitivity carries it through `γ ∈ a`; if `μ = γ`, membership transports directly. The remaining comparison `γ ∈ μ` is impossible, because the inclusion `μ ⊆ γ` would then give `γ ∈ γ`.

```agda
      μ∈a = go (ord-tri (fst μ) oμ (fst γ) oγ)
        where
        go : ⟨ fst μ ∈ˢ fst γ ⟩ ⊎ ((fst μ ≡ fst γ) ⊎ ⟨ fst γ ∈ˢ fst μ ⟩) → ⟨ fst μ ∈ˢ a ⟩
        go (inl h)       = oa .fst h γ∈a
        go (inr (inl e)) = subst (λ w → ⟨ w ∈ˢ a ⟩) (sym e) γ∈a
```

The representative `μ` must also be infinite. If `μ ∈ ω`, the inclusion `ω ↪ γ` for infinite `γ`, followed by `γ ↪ μ`, would inject `ω` into the finite ordinal `μ`, which is impossible. For later use, `Seg p b` records a predecessor `r ≺ p` whose collapse value is `b`.

```agda
        go (inr (inr h)) = Empty.rec (∈-irrefl (fst γ) (μ⊆γ (fst γ) h))
      μ∉ω : ⟨ fst μ ∈ˢ ω ⟩ → Empty.⊥
      μ∉ω h = no-fin γ μ oγ γ∉ω oμ h γ↪μ
  Seg : OT.Dom → V ℓ → Type (ℓ-suc ℓ)
  Seg p b = Σ[ r ∈ OT.Dom ] ((r OT.≺ p) × (C.col r ≡ b))
```

Segments are unique: two predecessors of `p` with equal collapse values are equal, since the collapse map is injective on indices, a proposition recorded once for later eliminations.

```agda
  isPropSeg : (p : OT.Dom) (b : V ℓ) → isProp (Seg p b)
  isPropSeg p b (r , _ , e) (r' , _ , e') =
    Σ≡Prop (λ r → isProp× (OT.isProp≺ r p) (setIsSet _ _)) (I.col-inj r r' (e ∙ sym e'))
```

Every member of a collapse value determines its segment, by the outward reading of the collapse and the uniqueness just proved. The maximum of a pair is then named: the larger of its two coordinates in the host order.

```agda
  seg : (p : OT.Dom) (b : V ℓ) → ⟨ b ∈ˢ C.col p ⟩ → Seg p b
  seg p b h = PT.rec (isPropSeg p b) (λ z → z) (C.col-out p b h)
  mx : OT.Dom → ⟪ K ⟫
  mx p = maxOrd (φ p .fst) (φ p .snd)
```

Let `mV p` be the ambient ordinal represented by the maximum of the two coordinates of `p`. If `r ≺ p` in the collapsed Gödel order, the first coordinate of `r` lies below the successor of this maximum; this is the first coordinate bound for the Gödel order.

```agda
  mV : OT.Dom → V ℓ
  mV p = ↑ (mx p)
  opaque
    seg-fst : (p r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .fst) ∈ˢ sucV (mV p) ⟩
    seg-fst p r k = fst∈suc (φ r) (φ p) (≺-fwd r p k)
```

The second coordinate of every `r ≺ p` obeys the same bound. We therefore use `gfin p = sucV (mV p)` as a common carrier for both coordinates; under the finite-case hypothesis `mV p ∈ ω`, this carrier is itself a finite ordinal.

```agda
    seg-snd : (p r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .snd) ∈ˢ sucV (mV p) ⟩
    seg-snd p r k = snd∈suc (φ r) (φ p) (≺-fwd r p k)
  gfin : OT.Dom → V ℓ
  gfin p = sucV (mV p)
  opaque
```

For each predecessor `r ≺ p`, the two coordinate bounds select two indices in the presentation of `gfin p`; `h p r` is their ordered pair. When `mV p` is finite, this pair codes `r` inside the square of a finite ordinal.

```agda
    h : (p r : OT.Dom) (k : r OT.≺ p) → ⟪ gfin p ⟫ × ⟪ gfin p ⟫
    h p r k = fiber (gfin p) (seg-fst p r k) .fst , fiber (gfin p) (seg-snd p r k) .fst
```

Equality of two codes `h p r` and `h p r'` forces equality of their first indices by applying the first projection. This is the first half of recovering the coordinates of `r` from its code.

```agda
    h-fst : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
          → h p r k ≡ h p r' k'
          → fiber (gfin p) (seg-fst p r k) .fst
          ≡ fiber (gfin p) (seg-fst p r' k') .fst
    h-fst p r r' k k' e = cong fst e
```

Applying the second projection to the same code equality likewise identifies the second indices. Thus equality of the fiber pairs controls both components separately.

```agda
    h-snd : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
          → h p r k ≡ h p r' k'
          → fiber (gfin p) (seg-snd p r k) .fst
          ≡ fiber (gfin p) (seg-snd p r' k') .fst
    h-snd p r r' k k' e = cong snd e
```

Equality of the first fiber indices implies equality of the ambient ordinals named by those fibers. Since the presentation map of `K` is injective, the first coordinates `φ r .fst` and `φ r' .fst` are equal.

```agda
  step-e1 : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
          → h p r k ≡ h p r' k' → φ r .fst ≡ φ r' .fst
  step-e1 p r r' k k' e =
    ↪-inj {a = K} (fiber-inj (gfin p) (seg-fst p r k) (seg-fst p r' k') (h-fst p r r' k k' e))
```

The second transfer lemma does the same for the second coordinates, so an equality of fiber pairs determines both coordinates of the underlying pair, which is what the finite case of the collapse will need.

```agda
  step-e2 : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
          → h p r k ≡ h p r' k' → φ r .snd ≡ φ r' .snd
  step-e2 p r r' k k' e =
    ↪-inj {a = K} (fiber-inj (gfin p) (seg-snd p r k) (seg-snd p r' k') (h-snd p r r' k k' e))
```

Equality of two fiber-pair codes gives equality of both coordinates of `φ r` and `φ r'`. Pair extensionality combines these coordinate equalities, and injectivity of `φ` then gives `r = r'`. Thus the coding of predecessors of `p` is injective. The finite case to be proved says that if the maximum coordinate of `p` belongs to `ω`, then so does `C.col p`.

```agda
  step-inj : (p r r' : OT.Dom) (k : r OT.≺ p) (k' : r' OT.≺ p)
           → h p r k ≡ h p r' k' → r ≡ r'
  step-inj p r r' k k' e =
    φ-inj r r' (pair≡ (step-e1 p r r' k k' e) (step-e2 p r r' k k' e))
  col-fin : (p : OT.Dom) → ⟨ mV p ∈ˢ ω ⟩ → ⟨ C.col p ∈ˢ ω ⟩
```

The proof compares the collapse value with `ω` by trichotomy, and names its finite carrier first: `g` is the successor of the ambient maximum of `p`, the set into which both coordinates of every predecessor were shown to fall.

```agda
  col-fin p m∈ω = go (ord-tri (C.col p) (C.col-ord p) ω ω-ord)
    where
    g : V ℓ
    g = sucV (mV p)
    og : IsOrd g
```

Because `mV p ∈ ω`, the maximum is an ordinal, and its successor `g` is an ordinal as well. The limit property of `ω` gives `g ∈ ω`, so `g` is a finite ordinal. These are precisely the hypotheses needed to rule out an injection of `ω` into `g × g`.

```agda
    og = suc-ord (ω-mem-ord (mV p) m∈ω)
    g∈ω : ⟨ g ∈ˢ ω ⟩
    g∈ω = ω-limit (mV p) m∈ω
```

The refutation assumes that `ω` is contained in the collapse value. Then every index of `ω` names a segment of `col p`: the containment places the named member inside the collapse, and the segment lemma recovers the predecessor.

```agda
    refute : ((z : V ℓ) → ⟨ z ∈ˢ ω ⟩ → ⟨ z ∈ˢ C.col p ⟩) → Empty.⊥
    refute sub = finite-excl-ω g og g∈ω f f-inj
      where
      s : (x : ⟪ ω ⟫) → Seg p (⟪ ω ⟫↪ x)
      s x = seg p (⟪ ω ⟫↪ x) (sub (⟪ ω ⟫↪ x) (member ω x))
```

For each `x ∈ ω`, let `s x` be the unique predecessor of `p` whose collapse value is `x`. The map `f` sends `x` to the two fiber indices coding the coordinates of this predecessor, hence to an element of the finite square `g × g`. It remains to show that equal such codes come from equal elements of `ω`.

```agda
      f : ⟪ ω ⟫ → ⟪ g ⟫ × ⟪ g ⟫
      f x = h p (s x .fst) (s x .snd .fst)
      f-inj : (x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y
      f-inj x y e = ↪-inj {a = ω}
        (sym (s x .snd .snd)
```

Injectivity is proved by composing three equations: the collapse value of the segment of `x` equals `x`, the segments agree as predecessors by the finite-case injection just proved, and the collapse value of the segment of `y` equals `y`. The composite forces `x` and `y` to agree.

```agda
         ∙ cong C.col (step-inj p (s x .fst) (s y .fst) (s x .snd .fst) (s y .snd .fst) e)
         ∙ s y .snd .snd)
```

Trichotomy now proves `C.col p ∈ ω`. Equality `C.col p = ω` would give the forbidden inclusion `ω ⊆ C.col p`; if `ω ∈ C.col p`, transitivity of the ordinal `C.col p` gives the same inclusion. For the general inverse-collapse construction, fix a predecessor bound `p` and a constructible carrier `g`.

```agda
    go : ⟨ C.col p ∈ˢ ω ⟩ ⊎ ((C.col p ≡ ω) ⊎ ⟨ ω ∈ˢ C.col p ⟩) → ⟨ C.col p ∈ˢ ω ⟩
    go (inl k)         = k
    go (inr (inl e))   = Empty.rec (refute (λ z z∈ω → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈ω))
    go (inr (inr ω∈c)) = Empty.rec (refute (λ z z∈ω → C.col-ord p .fst z∈ω ω∈c))
  module Inv (p : OT.Dom) (g : S)
```

Assume that, for every `r ≺ p`, both coordinates represented by `φ r` belong to the carrier of `g`. These two bounds ensure that the pair represented by `r` belongs to the internal product `prodL g`, the codomain of the inverse collapse.

```agda
             (bfst : (r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .fst) ∈ˢ fst g ⟩)
             (bsnd : (r : OT.Dom) → r OT.≺ p → ⟨ ↑ (φ r .snd) ∈ˢ fst g ⟩) where
```

Every member `x` of the collapse value determines its segment: the truncated membership is eliminated, since segments are unique, and yields a predecessor `r` whose collapse value is the underlying set of `x`.

```agda
    private
      pre : (x : S) → ⟨ fst x ∈ˢ C.col p ⟩ → Σ[ r ∈ OT.Dom ] (C.col r ≡ fst x)
      pre x mx = seg p (fst x) mx .fst , seg p (fst x) mx .snd .snd
```

For the predecessor selected from `x ∈ C.col p`, the presentation equation identifies `OT.↪ r` with the ordered pair of the two coordinates represented by `φ r`. Membership in `prodL g` is therefore reduced to the two coordinate bounds; `bfst` supplies the first one.

```agda
      bound : (x : S) (mx : ⟨ fst x ∈ˢ C.col p ⟩) → ⟨ OT.↪ (pre x mx .fst) ∈ˢ fst (prodL g) ⟩
      bound x mx = subst (λ w → ⟨ w ∈ˢ fst (prodL g) ⟩) (sym (φ-eq (seg p (fst x) mx .fst)))
        (prodL-in g (upK (φ (seg p (fst x) mx .fst) .fst))
                    (upK (φ (seg p (fst x) mx .fst) .snd))
                    (bfst _ (seg p (fst x) mx .snd .fst))
```

The bound `bsnd` supplies the second coordinate membership. Together the two bounds place the represented ordered pair in `g × g`, completing the required codomain proof.

```agda
                    (bsnd _ (seg p (fst x) mx .snd .fst)))
```

Consequently, collapse on the initial segment below `p` has a definable inverse into `prodL g`: each member of `C.col p` returns to its unique predecessor, and distinct collapse values return to distinct pairs. This gives an internal injection `C.colʟ p ↪ prodL g`. The main induction now aims to prove `C.col p ∈ a` for every `p`, beginning with trichotomy for its maximum coordinate.

```agda
    open I.Inverse (C.colʟ p) (prodL g) pre bound public
      using ( fn; graph; at; only; M; inj; injL ) renaming ( SourceMem to Mem )
  colIn : (p : OT.Dom) → ⟨ C.col p ∈ˢ a ⟩
  colIn p = go (ord-tri (mV p) (ord↑ (mx p)) ω ω-ord)
    where
```

If the maximum of the pair is finite, the collapse value is finite by the finite case, and the containment of `ω` in `a` places it inside `a`. Otherwise the maximum is infinite, and the trichotomy between the collapse value and `a` is examined.

```agda
    go : ⟨ mV p ∈ˢ ω ⟩ ⊎ ((mV p ≡ ω) ⊎ ⟨ ω ∈ˢ mV p ⟩) → ⟨ C.col p ∈ˢ a ⟩
    go (inl m∈ω) = ω⊆a (C.col p) (col-fin p m∈ω)
    go (inr inf) = go' (ord-tri (C.col p) (C.col-ord p) a oa)
      where
      m∉ω : ⟨ mV p ∈ˢ ω ⟩ → Empty.⊥
```

In the infinite branch, suppose for contradiction that `mV p ∈ ω`. If `mV p = ω`, transporting this membership gives `ω ∈ ω`. If instead `ω ∈ mV p`, transitivity of `ω` combines the two memberships to give `ω ∈ ω` again. Irreflexivity rules out both alternatives, so `mV p` is not finite.

```agda
      m∉ω h = rr inf
        where
        rr : (mV p ≡ ω) ⊎ ⟨ ω ∈ˢ mV p ⟩ → Empty.⊥
        rr (inl e)   = ∈-irrefl ω (subst (λ w → ⟨ w ∈ˢ ω ⟩) e h)
        rr (inr ω∈m) = ∈-irrefl ω (ω-ord .fst ω∈m h)
```

The carrier `g` is the successor of the maximum, and is an ordinal because the maximum is a member of the ordinal `κ`; the ordinal is then packaged as an element `gL` of `L`.

```agda
      g : V ℓ
      g = sucV (mV p)
      og : IsOrd g
      og = suc-ord (ord↑ (mx p))
      gL : S
```

The carrier belongs to `a` by the successor closure proved above, and it is infinite: if `g` belonged to `ω`, then the maximum, being a member of `g`, would belong to `ω` by transitivity, contradicting the infiniteness just established.

```agda
      gL = ordL g og
      g∈a : ⟨ g ∈ˢ a ⟩
      g∈a = suc∈ (mV p) (member K (mx p))
      g∉ω : ⟨ g ∈ˢ ω ⟩ → Empty.⊥
      g∉ω h = m∉ω (ω-ord .fst (self∈sucV (mV p)) h)
```

For every `r ≺ p`, the bounds `seg-fst` and `seg-snd` place both coordinates of `r` in `g = sucV (mV p)`. The inverse-collapse construction therefore gives an internal injection from `C.colʟ p` into `prodL gL`.

```agda
      module IV = Inv p gL (seg-fst p) (seg-snd p) using (injL)
```

Compose the inverse-collapse injection with `prod-into gL` to obtain `C.colʟ p ↪ gL`. To construct the latter injection, `prod-into` first chooses an internal cardinal representative `μ` of `gL`, applies the induction hypothesis at `μ`, and transports the resulting square injection along the injections between `μ` and `gL`.

```agda
      col↪g : InjL (C.colʟ p) gL
      col↪g = injl-trans (C.colʟ p) (prodL gL) gL IV.injL (prod-into gL og g∈a g∉ω)
      absurd : ((z : V ℓ) → ⟨ z ∈ˢ a ⟩ → ⟨ z ∈ˢ C.col p ⟩) → Empty.⊥
      absurd sub = carda gL g∈a
        (injl-trans κ (C.colʟ p) gL (inclusion-coded κ (C.colʟ p) sub) col↪g)
```

If the cardinal were contained in the collapse value, composing that inclusion with the injection into `gL` would inject `κ` into its own member `gL`, contradicting the internal cardinality of `κ`. The trichotomy between the collapse value and `a` therefore leaves only direct membership.

```agda
      go' : ⟨ C.col p ∈ˢ a ⟩ ⊎ ((C.col p ≡ a) ⊎ ⟨ a ∈ˢ C.col p ⟩) → ⟨ C.col p ∈ˢ a ⟩
      go' (inl h)       = h
      go' (inr (inl e)) = Empty.rec (absurd (λ z z∈a → subst (λ w → ⟨ z ∈ˢ w ⟩) (sym e) z∈a))
      go' (inr (inr h)) = Empty.rec (absurd (λ z z∈a → C.col-ord p .fst z∈a h))
  result : InjL (prodL κ) κ
```

The product first injects into the collapse order type `C.otL`. Every member `z` of this order type is equal to `C.col b` for some `b : OT.Dom`, and `colIn b` places that collapse value in `a`; hence `C.otL ⊆ κ`. Composing the first injection with the coded inclusion gives the required internal injection `prodL κ ↪ κ`.

```agda
  result = injl-trans P C.otL κ injL-ot (inclusion-coded C.otL κ ot⊆a)
    where
    ot⊆a : (z : V ℓ) → ⟨ z ∈ˢ fst C.otL ⟩ → ⟨ z ∈ˢ a ⟩
    ot⊆a z hz = PT.rec (snd (z ∈ˢ a))
      (λ { (b , e) → subst (λ w → ⟨ w ∈ˢ a ⟩) e (colIn b) }) (C.otL-out z hz)
```

Membership well-founded induction now proves the square law. Given an ordinal `κ` that is an internal cardinal and satisfies `ω ∈ κ`, the induction step constructed above yields an internal injection `prodL κ ↪ κ` once the required proof that `κ` is not finite is supplied.

```agda
square-law-L :
    (κ : S) → IsOrd (fst κ) → IsCardinalL κ → ⟨ ω ∈ˢ fst κ ⟩
  → InjL (prodL κ) κ
square-law-L κ oκ cκ ω∈κ =
  WF.WFI.induction regularityV {P = Goal} Step.result (fst κ) (snd κ) oκ cκ
```

Finally, `κ` cannot belong to `ω`. If it did, transitivity of the ordinal `ω` would combine `ω ∈ κ` with `κ ∈ ω` to give `ω ∈ ω`, contradicting irreflexivity. This discharges the infinitude hypothesis required by the induction step.

```agda
    (λ κ∈ω → ∈-irrefl ω (ω-ord .fst ω∈κ κ∈ω))
```