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.

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

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.

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.

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.

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.

  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.

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.

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.

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.

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.

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.

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.

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

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.

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.

  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.

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.

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

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.

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.

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.

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.

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.

  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.

  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.

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.

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.

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.

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.

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.

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.

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.

  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.

  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.

  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.

        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.

  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.

    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.

    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.

  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.

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

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

  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.

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

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

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

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.

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.

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.

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

  K : V ℓ
  K = fst κ

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

  ↑ : ⟪ 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.

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

  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.

  _≺₁_ : ⟪ 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.

  _≺ₚ_ : 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.

  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.

  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.

    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.

    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.

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

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

  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.

    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.

  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.

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

      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.

      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.

      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.

      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.

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

      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.

      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.

  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.

    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.

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

    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.

  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.

    ≤→∈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.

  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.

    ≤→∈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.

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

    ≤→∈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.

  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.

  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.

  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.

  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.

  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.

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

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

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

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

  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.

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

  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.

    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.

  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.

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.

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.

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

  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.

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

  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.

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

  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.

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.

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

  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.

  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.

  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.

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

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

  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.

    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.

    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.

  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.

  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.

    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.

  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.

  opaque
    mapFo : Formula S 
    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'.

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

    private
      env₄ : S → S → S → S → S → S → S ^ 
      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.

      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.

      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.

      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.

      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.

    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.

        , ( 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 })