Closing a small set under definable least witnesses should preserve an infinite cardinal bound. This chapter proves inside L that if the starting set injects into an infinite cardinal, then so does its Skolem hull.

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

Excluded middle supplies local decisions such as whether a member of a union lies in its left summand. Classical reasoning enters through one explicit hypothesis, so the resulting bound records exactly that assumption.

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

Fix a universe level ℓ and excluded middle for propositions at level ℓ-suc ℓ. The internal sets, coded graphs, and truncated witnesses are all formed relative to this fixed instance.

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

Coded graphs are expressed in the first-order language of equality and membership. Conjunction, disjunction, negation, and existential quantification describe their cases, while satisfaction is interpreted over the ambient cumulative hierarchy.

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

The argument moves between ordinal stages and their constructible members. Transitivity keeps members inside L, while ordinal membership and stage cumulativity place each object in a stage large enough for definable selection.

open import V.Coding {ℓ} using ( pr; pr-inj; #-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd; Lset; Lset-mono; Lset-layer; layer-trans )
open import L.Ordinal {ℓ} using ( mem-ord; #∈ω )
open import L.Ordinal.Stages {ℓ} lem using ( Lset-cumul; ord∈Lset-suc )

The counting maps must themselves be sets of L. Separation constructs subgraphs, pairing and union build their codes, and adequacy connects the internal formulas for application, single-valuedness, and domains with their set-theoretic meanings.

open import L.Axioms.Basic {ℓ} using ( LsetS; ∅ʟ )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
open import L.Axioms.Infinity {ℓ} lem using ( ωʟ )
open import L.Axioms.Numerals {ℓ} using ( pairʟ; unionʟ )
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; appAt; appAt-adequate; svAt-out; domAt-in )

An internal injection is witnessed by a constructible graph with exact domain, single-valuedness, injectivity, and a range bound. InjCode retains a particular graph, whereas InjL retains only the proposition that one exists.

open import L.Coding.Expressions {ℓ} using ( numL; tagAtL; tagAtL-adequate )
open import L.Coding.CodeConstructibility {ℓ}
  using ( sglʟ; sglʟ-in; sglʟ-out; cupʟ; cupʟ-inl; cupʟ-inr; cupʟ-out )
open import L.Coding.Injection {ℓ} lem using ( injAt-out; module Extract )
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )

The counting proof composes internal injections. Definable maps turn formulas with unique values into constructible graphs, least-witness selection supplies such maps for Skolem closure, and the internal product provides room for tagged pairs.

open import L.InjectionComposition {ℓ} lem using ( inclusion-coded; injl-trans )
open import L.DefinableInjection {ℓ} lem using ( DefinableMap; module Inj )
open import L.GCH.LeastWitnessMap {ℓ} lem using ( module Least )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prodL; prodL-in; module Relation )
open import L.InjectionComposition {ℓ} lem using ( appC; appC-adequate )

Least witnesses are selected inside a common constructible stage. Bounding ordinals collect the parameters there, superadequacy stabilizes satisfaction, and the satisfaction graph records the choices as a set of L.

open import L.Stage {ℓ} lem using ( LeastOrd; isPropLeastOrd; leastOrd; stage; stage-ord; stage-mem )
open import L.Ordinal using ( boundingOrd )
open import L.Coding.EnvironmentSet {ℓ} lem using ( envSet; envSet-in )
open import L.GCH.AdequateStages {ℓ} lem using ( Superadequate )
open import L.Coding.SatisfactionGraphSet {ℓ} lem using ( module SatGraph )

The Skolem hull is obtained by iterating least-witness closure from the starting set. Its constructible presentation supplies stage bounds for selection, while condensation identifies the hull with the corresponding constructible structure.

open import L.GCH.SkolemHull {ℓ} lem using ( module Frame; module HullStage )
open import L.GCH.ConstructibleHull {ℓ} lem using ( module Condense′; module Telescope )
open import L.GCH.StageCountingTools {ℓ} lem
  using ( isPropInjCode; injcode-resp; injFo; module InjFo; pinAt; pin-in; pin-out; seq-map; Lω
        ; limit-stage-counted )

Each closure step is indexed by a formula code and a finite parameter sequence. Formula shapes are countable, finite sequences over an infinite cardinal are bounded by the square law, and well-founded induction supplies that law for the internal cardinals in the count.

open import L.GCH.FiniteSequenceCoding {ℓ} lem using ( seqL; seqL-in; seq-count )
open import L.GCH.CardinalSquareLaw {ℓ} lem using ( prod-inj; ω⊆; Goal; module Step )
open import L.Cardinal {ℓ} lem using ( IsCardinalL )
open import V.Hierarchy {ℓ} using ( regularityV )
import Cubical.Induction.WellFounded as WF

When both arguments of a graph are identified by equalities, two-place transport moves a graph-membership proof across both identifications at once. Thus equality replacement remains compatible with the coded relation.

open import Cubical.Foundations.Prelude using ( subst2 )

The tags 0 and 1 are distinct, making the two branches of a tagged injection disjoint. Equality of dependent pairs with proposition-valued fibers reduces to equality of their first components, so constructibility proofs do not affect the count.

open import Cubical.Data.Nat.Properties using ( znots; snotz )
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
open import Cubical.Data.Sum using ( _⊎_; inl; inr )
open import Cubical.Foundations.HLevels using ( isProp×; isSetΣSndProp )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )

Von Neumann numerals provide the tags, ω collects them, and successor describes their finite progression. The empty set serves as the value of a singleton injection, while propositional truncation records existence without choosing a representative.

open import Cubical.HITs.CumulativeHierarchy.Constructions using ( module InfinitySet )
open InfinitySet {ℓ} using ( #_; ω; sucV )
open import Cubical.HITs.CumulativeHierarchy.Constructions using ( ∅ )
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT

Existence of a coded injection is propositionally truncated because the count depends only on whether a witnessing graph exists. Elimination is therefore made only into propositions, preserving independence from the choice of graph.

open PT using ( ∥_∥₁; ∣_∣₁; squash₁ )

For ambient sets, x ∈ˢ y is the proposition that x belongs to y. The domain and range clauses of coded functions ultimately reduce to this relation on underlying sets.

open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

Write S for the carrier of the constructible model. Its elements are ambient sets paired with proofs of membership in L; since those proofs are propositions, the underlying set determines the constructible element up to equality.

module SL = hPropStructure 𝒮ʟ using ( S )
open SL using ( S )

A formula with constructible constants can be evaluated inside L and projected to the ambient hierarchy. Transitivity makes the two readings agree, so an internally proved graph statement can be used as ordinary membership between underlying sets.

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

Holds F x y means that the ordered pair of the underlying sets of x and y belongs to the underlying graph F. This is the ambient relation represented by every coded application formula in the argument.

Holds : S → S → S → Type (ℓ-suc ℓ)
Holds F x y = ⟨ pr (fst x) (fst y) ∈ fst F ⟩

The element nn k : S is the ambient von Neumann numeral # k together with its constructibility proof. In particular, nn 0 and nn 1 serve as internal tags without leaving L.

nn : ℕ → S
nn k = # k , numL k

If two elements of S have equal underlying sets, then the elements themselves are equal. The second components contain only constructibility proofs, so proof irrelevance lifts equality of the first components to equality of the dependent pairs.

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

The carrier S is an h-set. Its first component lies in the cumulative hierarchy, which is an h-set, and each fiber of constructibility proofs is a proposition; hence every equality type in S is a proposition.

isSetS : isSet S
isSetS = isSetΣSndProp setIsSet (λ v → snd (isL v))

De Bruijn indices for the first two variable slots are named, since the coded formulas of this chapter never mention more than eight slots at once.

private
  i0 : ∀ {k} → Fin (suc k)
  i0 = zero
  i1 : ∀ {k} → Fin (suc (suc k))
  i1 = suc i0

The names i2, i3, and i4 denote variable positions two, three, and four. Each is one successor beyond the preceding index, with a polymorphic tail k keeping the position valid when more variables are available.

  i2 : ∀ {k} → Fin (suc (suc (suc k)))
  i2 = suc i1
  i3 : ∀ {k} → Fin (suc (suc (suc (suc k))))
  i3 = suc i2
  i4 : ∀ {k} → Fin (suc (suc (suc (suc (suc k)))))

After the defining equation for i4, the same successor pattern defines positions five and six. These names make the shifts caused by nested binders visible in the types of coded formulas.

  i4 = suc i3
  i5 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc k))))))
  i5 = suc i4
  i6 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc k)))))))
  i6 = suc i5

Slot seven is the last, and the eight indices cover every variable position used in this chapter.

  i7 : ∀ {k} → Fin (suc (suc (suc (suc (suc (suc (suc (suc k))))))))
  i7 = suc i6

An ordinal is contained in its own stage: each member of an ordinal is itself an ordinal, and the cumulative construction places every member of the ordinal into the stage indexed by that ordinal.

ord⊆Lset : (α : V ℓ) → IsOrd α → (z : V ℓ) → ⟨ z ∈ α ⟩ → ⟨ z ∈ Lset α ⟩
ord⊆Lset α oα z z∈α =
  Lset-cumul z α oz oα z∈α (ord∈Lset-suc z oz)
  where
  oz : IsOrd z

Since z ∈ α and α is an ordinal, z is itself an ordinal. This places z in its successor stage; cumulativity along z ∈ α then gives z ∈ Lset α.

  oz = mem-ord {A = α} oα z z∈α

Fix constructible sets D₁ and D₂. Their internal binary union is the common domain for combining two injections; its membership principle gives both inclusions and a truncated case split.

module Union2 (D₁ D₂ : S) where

The union is the internal union of the two sets.

  D : S
  D = cupʟ D₁ D₂

Left members are included by the left rule of the union.

  in₁ : (z : S) → ⟨ fst z ∈ fst D₁ ⟩ → ⟨ fst z ∈ fst D ⟩
  in₁ z = cupʟ-inl D₁ D₂ (fst z)

Right members are included symmetrically.

  in₂ : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → ⟨ fst z ∈ fst D ⟩
  in₂ z = cupʟ-inr D₁ D₂ (fst z)

If z ∈ D₁ ∪ D₂, then it merely belongs to the left side or the right side. The disjunction is propositionally truncated because membership retains that some presentation index names z, but not which index supplied it.

  out : (z : S) → ⟨ fst z ∈ fst D ⟩ → ∥ ⟨ fst z ∈ fst D₁ ⟩ ⊎ ⟨ fst z ∈ fst D₂ ⟩ ∥₁
  out z = cupʟ-out D₁ D₂ (fst z)

Let κ be a constructible set containing the tags 0 and 1, and let E₁ and E₂ code injections from D₁ and D₂ into κ. Tagging their values combines them into an injection from D₁ ∪ D₂ into κ × κ. This construction requires no ordinal hypothesis on κ.

module TagUnion (κ : S) (0∈κ : ⟨ #  ∈ fst κ ⟩) (1∈κ : ⟨ #  ∈ fst κ ⟩)
                (D₁ D₂ E₁ E₂ : S) (c₁ : InjCode E₁ D₁ κ) (c₂ : InjCode E₂ D₂ κ) where

Write D = D₁ ∪ D₂. A member of either summand belongs to D, and every member of D yields a truncated proof that it comes from one of the two summands.

  open Union2 D₁ D₂ public using ( D; in₁; in₂; out )

Each coded injection extracts its underlying function together with the proof that its graph holds exactly when the coding says so.

  module X₁ = Extract E₁ D₁ (fst c₁) (fst (snd c₁)) using ( toFun; toFun-graph )
  module X₂ = Extract E₂ D₂ (fst c₂) (fst (snd c₂)) using ( toFun; toFun-graph )

Mem z is the proposition that z belongs to the union domain D. Carrying this proof with an input supplies exactly the domain evidence needed to evaluate the piecewise function.

  Mem : S → Type (ℓ-suc ℓ)
  Mem z = ⟨ fst z ∈ fst D ⟩

Membership in the left domain is decidable by excluded middle, and the decision is the case split the tagged injection is built on.

  Case : S → Type (ℓ-suc ℓ)
  Case z = ⟨ fst z ∈ fst D₁ ⟩ ⊎ (⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥)

Excluded middle decides, for every member of the union, whether it came from the left domain.

  decide : (z : S) → Case z
  decide z = lem (fst z ∈ fst D₁)

A member outside the left domain must lie in the right domain: the union membership splits into the two sides, and the left side contradicts the assumed failure.

  off : (z : S) → Mem z → (⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥) → ⟨ fst z ∈ fst D₂ ⟩
  off z m no = PT.rec (snd (fst z ∈ fst D₂))
    (λ { (inl h) → Empty.rec (no h) ; (inr h) → h }) (out z m)

The value on each side is the tagged image: the numeral tag zero or one paired with the extracted function value, so the two injections land in disjoint tagged ranges.

  val : (z : S) → Mem z → Case z → S
  val z m (inl h)  = prʟ (nn ) (X₁.toFun (z , h))
  val z m (inr no) = prʟ (nn ) (X₂.toFun (z , off z m no))

For z ∈ D, the function fn decides whether z ∈ D₁. It returns (0,E₁(z)) in the left case and (1,E₂(z)) in the complementary right case.

  fn : (z : S) → Mem z → S
  fn z m = val z m (decide z)

The ambient meaning Wit y z has two branches. In the left branch, z ∈ D₁, and there merely exists v with (z,v) ∈ E₁ such that the underlying set of y is (0,v).

  Wit : (y z : S) → Type (ℓ-suc ℓ)
  Wit y z =
      (⟨ fst z ∈ fst D₁ ⟩
        × ∥ Σ[ v ∈ S ] (Holds E₁ z v × (fst y ≡ pr (# ) (fst v))) ∥₁)
    ⊎ ((⟨ fst z ∈ fst D₁ ⟩ → Empty.⊥)

In the right branch, z ∉ D₁, and there merely exists v with (z,v) ∈ E₂ such that y = (1,v) on underlying sets. The distinct tags rule out equality between outputs from opposite branches.

        × ∥ Σ[ v ∈ S ] (Holds E₂ z v × (fst y ≡ pr (# ) (fst v))) ∥₁)

The graph is written as a two-slot formula: membership in D₁ conjoined with an existential over the first code, or the negation of that membership conjoined with an existential over the second code. Inside the existential, the injected value and the tag equation are atoms of the coding.

  opaque
    fo : Formula S 
    fo = ((var i1 ∈̇ con D₁) ∧̇ ∃̇ (appC E₁ i2 i0 ∧̇ tagAtL i1  i0))
       ∨̇ ((¬̇ (var i1 ∈̇ con D₁)) ∧̇ ∃̇ (appC E₂ i2 i0 ∧̇ tagAtL i1  i0))

Reading the two coding atoms uses their adequacy lemmas: satisfaction of the application atom becomes a membership Holds E z v, and satisfaction of the tag atom becomes the equation between y and the tagged pair.

    private
      rd : (E : S) (k : ℕ) (y z v : S)
         → ⟨ (v ∷ y ∷ z ∷ []) ⊨ appC E i2 i0 ⟩ → ⟨ (v ∷ y ∷ z ∷ []) ⊨ tagAtL i1 k i0 ⟩
         → Holds E z v × (fst y ≡ pr (# k) (fst v))
      rd E k y z v ha ht =

After transport along the two adequacy equivalences, the satisfaction witnesses become the components required by Wit: graph membership Holds E z v and the equality identifying y with the pair tagged by k.

          subst ⟨_⟩ (appC-adequate E i2 i0 (v ∷ y ∷ z ∷ [])) ha
        , subst ⟨_⟩ (tagAtL-adequate i1 k i0 (v ∷ y ∷ z ∷ [])) ht

Conversely, from Holds E z v and the underlying equality y = (k,v), transport backward along adequacy produces satisfaction of the application atom.

      wr : (E : S) (k : ℕ) (y z v : S)
         → Holds E z v → fst y ≡ pr (# k) (fst v)
         → ⟨ (v ∷ y ∷ z ∷ []) ⊨ appC E i2 i0 ⟩ × ⟨ (v ∷ y ∷ z ∷ []) ⊨ tagAtL i1 k i0 ⟩
      wr E k y z v ha ht =
          subst ⟨_⟩ (sym (appC-adequate E i2 i0 (v ∷ y ∷ z ∷ []))) ha

The same backward transport turns the tagged-pair equality into satisfaction of the tag atom. Together the two proofs reconstruct the conjunction under the existential quantifier.

        , subst ⟨_⟩ (sym (tagAtL-adequate i1 k i0 (v ∷ y ∷ z ∷ []))) ht

Reading a satisfaction proof of fo proceeds by its two disjuncts. The left yields z ∈ D₁ and a truncated E₁ witness tagged by zero; the right yields z ∉ D₁ and the corresponding E₂ witness tagged by one. Applying rd inside each truncation gives a truncated inhabitant of Wit y z.

    fo-out : (y z : S) → ⟨ (y ∷ z ∷ []) ⊨ fo ⟩ → ∥ Wit y z ∥₁
    fo-out y z = PT.map
      (λ { (inl (h , hv)) → inl (h , PT.map (λ { (v , (ha , ht)) → v , rd E₁  y z v ha ht }) hv)
         ; (inr (h , hv)) → inr ((λ z∈ → lower (h z∈))
             , PT.map (λ { (v , (ha , ht)) → v , rd E₂  y z v ha ht }) hv) })

The inward reading of the graph turns the host-side witness into satisfaction, case by case. In the left case the membership and the truncated entry are transported through the adequacy equations of the application and tag codings; the right case does the same after lifting the refutation of membership into the object-language negation.

    fo-in : (y z : S) → Wit y z → ⟨ (y ∷ z ∷ []) ⊨ fo ⟩
    fo-in y z (inl (h , hv)) =
      ∣ inl (h , PT.map (λ { (v , (ha , ht)) → v , wr E₁  y z v ha ht }) hv) ∣₁
    fo-in y z (inr (h , hv)) =
      ∣ inr ((λ z∈ → lift (h z∈))

The tail of the right case completes the second disjunct: the entry of E₂ is transported exactly as in the left, with the tag 1 in place of 0. Both disjuncts are then injected into the truncated existence, and the introduction is finished.

          , PT.map (λ { (v , (ha , ht)) → v , wr E₂  y z v ha ht }) hv) ∣₁

Each coded relation is single-valued: two entries with the same first component have the same second component. This is the first conjunct of the injection code, read out through the adequacy of the application coding.

  private
    sv₁ : (x y y' : S) → Holds E₁ x y → Holds E₁ x y' → fst y ≡ fst y'
    sv₁ = svAt-out zero (E₁ ∷ D₁ ∷ []) (fst c₁)
    sv₂ : (x y y' : S) → Holds E₂ x y → Holds E₂ x y' → fst y ≡ fst y'
    sv₂ = svAt-out zero (E₂ ∷ D₂ ∷ []) (fst c₂)

Each coded relation is also injective: two entries with the same second component have first components with equal underlying sets. The range clause begins the list: every value of the relation lies in the cardinal.

    ij₁ : (y x x' : S) → Holds E₁ x y → Holds E₁ x' y → fst x ≡ fst x'
    ij₁ = injAt-out zero (E₁ ∷ D₁ ∷ []) (fst (snd (snd c₁)))
    ij₂ : (y x x' : S) → Holds E₂ x y → Holds E₂ x' y → fst x ≡ fst x'
    ij₂ = injAt-out zero (E₂ ∷ D₂ ∷ []) (fst (snd (snd c₂)))
    ran₁ : (x y : S) → Holds E₁ x y → ⟨ fst y ∈ fst κ ⟩

The second range clause completes the data extracted from the two injection codes. For each relation we now have single-valuedness, injectivity, and the fact that every value lies in κ; these are the properties used to build the tagged map.

    ran₁ = snd (snd (snd c₁))
    ran₂ : (x y : S) → Holds E₂ x y → ⟨ fst y ∈ fst κ ⟩
    ran₂ = snd (snd (snd c₂))

The witness is constructed from the two cases for a member. If z ∈ D₁, its value uses the function extracted from E₁; otherwise it uses the function extracted from E₂ at the resulting member of D₂. In either case the extraction supplies both the graph entry and the equation identifying the tagged pair with the chosen value.

  wit : (z : S) (m : Mem z) (c : Case z) → Wit (val z m c) z
  wit z m (inl h)  = inl (h , ∣ X₁.toFun (z , h)
    , (X₁.toFun-graph (z , h) , prʟ-fst (nn ) (X₁.toFun (z , h))) ∣₁)
  wit z m (inr no) = inr (no , ∣ X₂.toFun (z , off z m no)
    , (X₂.toFun-graph (z , off z m no) , prʟ-fst (nn ) (X₂.toFun (z , off z m no))) ∣₁)

Uniqueness in the left case composes three equations: the entry's second component equals the value named by the truncated witness; single-valuedness of E₁ identifies the two function values; and the pair's first-projection equation says the value is exactly the tagged entry.

  only : (z : S) (m : Mem z) (c : Case z) (y : S) → Wit y z → fst y ≡ fst (val z m c)
  only z m (inl h) y (inl (_ , hv)) = PT.rec (setIsSet _ _)
    (λ { (v , (hg , hy)) →
       hy ∙ cong (pr (# )) (sv₁ z v (X₁.toFun (z , h)) hg (X₁.toFun-graph (z , h)))
          ∙ sym (prʟ-fst (nn ) (X₁.toFun (z , h))) }) hv

The mixed cases are refuted outright: a member inside D₁ cannot carry a witness recorded off D₁, and conversely. The right-right case is then handled exactly as the left, with E₂, the tag 1, and the off-set function value.

  only z m (inl h) y (inr (no , _)) = Empty.rec (no h)
  only z m (inr no) y (inl (h , _)) = Empty.rec (no h)
  only z m (inr no) y (inr (_ , hv)) = PT.rec (setIsSet _ _)
    (λ { (v , (hg , hy)) →
       hy ∙ cong (pr (# )) (sv₂ z v (X₂.toFun (z , off z m no)) hg (X₂.toFun-graph (z , off z m no)))

The final equation composes the tag identification with the pair's first-projection equation, completing uniqueness. The witness thus determines its value in both cases.

          ∙ sym (prʟ-fst (nn ) (X₂.toFun (z , off z m no))) }) hv

The value lands in the internal product: the pair of the numeral 0 or 1 with the function value is presented through its first projection equation, and prodL-in admits it because both numerals lie in κ and the function value lies in κ by the range clause.

  into : (z : S) (m : Mem z) (c : Case z) → ⟨ fst (val z m c) ∈ˢ fst (prodL κ) ⟩
  into z m (inl h) = subst (λ w → ⟨ w ∈ˢ fst (prodL κ) ⟩) (sym (prʟ-fst (nn ) (X₁.toFun (z , h))))
    (prodL-in κ (nn ) (X₁.toFun (z , h)) 0∈κ (ran₁ z (X₁.toFun (z , h)) (X₁.toFun-graph (z , h))))
  into z m (inr no) = subst (λ w → ⟨ w ∈ˢ fst (prodL κ) ⟩) (sym (prʟ-fst (nn ) (X₂.toFun (z , off z m no))))
    (prodL-in κ (nn ) (X₂.toFun (z , off z m no)) 1∈κ

The right case supplies the range fact from E₂ and the numeral 1, completing the membership of both tagged values in the product.

      (ran₂ z (X₂.toFun (z , off z m no)) (X₂.toFun-graph (z , off z m no))))

These ingredients define a map from the ordinary union D to the internal product prodL κ. Its value is chosen by the left-biased case distinction, and into proves that this tagged value belongs to the product.

  Dmap : DefinableMap
  Dmap = record
    { dom = D ; cod = prodL κ ; fn = fn
    ; into = λ z m → into z m (decide z)
    ; graph = fo

The defining clause feeds the witness into the graph introduction, and uniqueness converts every graph entry into the value at the decided case, transported along the carrier equality. The definable map is complete.

    ; defines = λ z m → fo-in (fn z m) z (wit z m (decide z))
    ; only = λ z m y h → S≡ (PT.rec (setIsSet _ _) (only z m (decide z) y) (fo-out y z h)) }

Injectivity of the tagged map is proved by comparing the decided cases of two inputs. The case analysis has four combinations, and the tagged pair structure separates them cleanly.

  inj : (z : S) (m : Mem z) (z' : S) (m' : Mem z') → fst (fn z m) ≡ fst (fn z' m') → fst z ≡ fst z'
  inj z m z' m' = go (decide z) (decide z')
    where
    go : (c : Case z) (c' : Case z') → fst (val z m c) ≡ fst (val z' m' c') → fst z ≡ fst z'
    go (inl h) (inl h') q = ij₁ (X₁.toFun (z , h)) z z' (X₁.toFun-graph (z , h))

In the same-tag case, the pair equation is inverted by pr-inj: the tags agree, so the equation of the values identifies the two function values, which is exactly the argument the injectivity clause consumes.

      (subst (λ w → ⟨ pr (fst z') w ∈ fst E₁ ⟩) (sym (snd p)) (X₁.toFun-graph (z' , h')))
      where
      p : (#  ≡ # ) × (fst (X₁.toFun (z , h)) ≡ fst (X₁.toFun (z' , h')))
      p = pr-inj (sym (prʟ-fst (nn ) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn ) (X₁.toFun (z' , h')))
    go (inl h) (inr no') q = Empty.rec (znots (#-inj   (fst

The mixed-tag cases are impossible: equality of the two values would force the numeral 0 to equal the numeral 1, contradicted in the two orientations by znots and snotz. When both inputs take the right branch, injectivity of E₂ identifies them.

      (pr-inj (sym (prʟ-fst (nn ) (X₁.toFun (z , h))) ∙ q ∙ prʟ-fst (nn ) (X₂.toFun (z' , off z' m' no')))))))
    go (inr no) (inl h') q = Empty.rec (snotz (#-inj   (fst
      (pr-inj (sym (prʟ-fst (nn ) (X₂.toFun (z , off z m no))) ∙ q ∙ prʟ-fst (nn ) (X₁.toFun (z' , h')))))))
    go (inr no) (inr no') q = ij₂ (X₂.toFun (z , off z m no)) z z' (X₂.toFun-graph (z , off z m no))
      (subst (λ w → ⟨ pr (fst z') w ∈ fst E₂ ⟩) (sym (snd p)) (X₂.toFun-graph (z' , off z' m' no')))

The pair equation for the right-right case splits into the agreement of the tags and of the function values, the latter being what injectivity consumes.

      where
      p : (#  ≡ # ) × (fst (X₂.toFun (z , off z m no)) ≡ fst (X₂.toFun (z' , off z' m' no')))
      p = pr-inj (sym (prʟ-fst (nn ) (X₂.toFun (z , off z m no))) ∙ q
                  ∙ prʟ-fst (nn ) (X₂.toFun (z' , off z' m' no')))

The resulting graph is a coded injection from the ordinary union D₁ ∪ D₂ into prodL κ. The map uses tags in its values to distinguish the two branches, and resolves an element in the overlap through the first branch.

  injL : InjL D (prodL κ)
  injL = Inj.injL Dmap inj

The two premises expose their injection graphs only under propositional truncation. Eliminating both truncations into the proposition InjL (D₁ ∪ D₂) (prodL κ) lets the tagged construction be applied to any witnessing pair of graphs, yielding the required mere coded injection.

tag-union : (κ : S) → ⟨ #  ∈ fst κ ⟩ → ⟨ #  ∈ fst κ ⟩
          → (D₁ D₂ : S) → InjL D₁ κ → InjL D₂ κ
          → InjL (unionʟ (pairʟ D₁ D₂)) (prodL κ)
tag-union κ h0 h1 D₁ D₂ = PT.rec2 squash₁
  (λ { (E₁ , c₁) (E₂ , c₂) → TagUnion.injL κ h0 h1 D₁ D₂ E₁ E₂ c₁ c₂ })

The least-predecessor construction is stated generically. It takes an ordinal γ, a relation G, a domain D, and a set P of predecessors bounded by the stage γ, such that every member of D merely has some G-predecessor in P; the task is to choose one canonically.

module LeastPre (γ : V ℓ) (oγ : IsOrd γ) (G D P : S)
  (inP : (p z : S) → Holds G p z → ⟨ fst p ∈ fst P ⟩)
  (P⊆L : (p : S) → ⟨ fst p ∈ fst P ⟩ → ⟨ fst p ∈ Lset γ ⟩)
  (have : (z : S) → ⟨ fst z ∈ fst D ⟩ → ∥ Σ[ p ∈ S ] Holds G p z ∥₁) where

Membership in the domain is recorded as a type, so that the argument can carry it alongside the elements.

  Mem : S → Type (ℓ-suc ℓ)
  Mem z = ⟨ fst z ∈ fst D ⟩

The graph formula is the application clause of the constant G: holding at a pair means exactly that the pair belongs to the relation.

  private
    graphFo : Formula S 
    graphFo = appC G i0 i1

The existence hypothesis is moved to the common stage without choosing a predecessor globally. Each truncated predecessor lies in P, hence in Lset γ, and the adequacy equation turns its relation membership into satisfaction of the graph formula.

    have-γ : (z : S) → Mem z
           → ∥ Σ[ p ∈ S ] (⟨ fst p ∈ Lset γ ⟩ × ⟨ (p ∷ z ∷ []) ⊨ graphFo ⟩) ∥₁
    have-γ z m = PT.map
      (λ { (p , h) → p , P⊆L p (inP p z h)
                       , subst ⟨_⟩ (sym (appC-adequate G i0 i1 (p ∷ z ∷ []))) h })

The original truncated existence supplies the witness that the transport consumes.

      (have z m)

The stage-order construction now selects, for every member of the domain, the least G-predecessor in Lset γ. It also supplies a definable graph and the membership readings that identify each input with its selected value.

    module Ls = Least γ oγ D graphFo have-γ using ( fn; fn-holds; Dmap; T; T-in; T-out )

The selected least predecessor is the value function of the construction.

  fn : (z : S) → Mem z → S
  fn = Ls.fn

The value satisfies the relation at its input: the internal satisfaction is transported back to the application clause at the environment pairing the value with the input.

  fn-holds : (z : S) (m : Mem z) → Holds G (fn z m) z
  fn-holds z m = subst ⟨_⟩ (appC-adequate G i0 i1 (fn z m ∷ z ∷ [])) (Ls.fn-holds z m)

The definable map is recorded with codomain P, the membership of the value being guaranteed by the inward direction of the standing hypothesis.

  Dmap : DefinableMap
  Dmap = record Ls.Dmap { cod = P ; into = λ z m → inP (fn z m) z (fn-holds z m) }

The graph of the least-predecessor function is an element of L, as the stage machinery returns it with its membership description.

  T : S
  T = Ls.T

The inward reading exhibits the pair of an input with its selected value as an entry of the graph.

  T-in : (z : S) (m : Mem z) → ⟨ pr (fst z) (fst (fn z m)) ∈ fst T ⟩
  T-in = Ls.T-in

The outward reading recovers, from every entry, the input together with the equation identifying the second component with the selected value; this is what later arguments use to compare candidates.

  T-out : (z e : S) → ⟨ pr (fst z) (fst e) ∈ fst T ⟩
        → Σ[ m ∈ Mem z ] (fst e ≡ fst (fn z m))
  T-out = Ls.T-out

Under the additional hypothesis that the relation is functional, the least-predecessor function becomes injective: the module carries that single assumption.

  module Functional
    (funct : (p z z' : S) → Holds G p z → Holds G p z' → fst z ≡ fst z') where

If two inputs share a value, the value satisfies the relation at both inputs; the second satisfaction is transported along the equation of the values, and functionality then identifies the two inputs.

    inj : (z : S) (m : Mem z) (z' : S) (m' : Mem z')
        → fst (fn z m) ≡ fst (fn z' m') → fst z ≡ fst z'
    inj z m z' m' q = funct (fn z m) z z' (fn-holds z m)
      (subst (λ w → ⟨ pr w (fst z') ∈ fst G ⟩) (sym q) (fn-holds z' m'))

The injectivity is packaged into a coded injection from the domain into the predecessor set.

    injL : InjL D P
    injL = Inj.injL Dmap inj

The point construction handles an at-most-singleton domain. Given only 0 ∈ κ, it sends every member of the singleton generated by a to the zeroth numeral and obtains a coded injection into κ.

module Point (κ : S) (0∈κ : ⟨ #  ∈ fst κ ⟩) (a : S) where

Let Y be the constructible singleton generated by a. The argument will use only its membership introduction and elimination laws.

  Y : S
  Y = sglʟ a

The member a belongs to its own singleton, by the introduction reading of the singleton construction.

  Y-in : ⟨ fst a ∈ fst Y ⟩
  Y-in = sglʟ-in a (fst a) refl

The elimination reading says the singleton contains nothing else: any member has a as its underlying set.

  Y-out : (z : S) → ⟨ fst z ∈ fst Y ⟩ → fst z ≡ fst a
  Y-out z = sglʟ-out a (fst z)

The graph is described by the atomic formula with two free slots that equates the value slot with the internal empty set, whose underlying set is the numeral 0.

  fo : Formula S 
  fo = var i0 ≐ con ∅ʟ

The definable map sends the unique input to the zeroth numeral; the codomain membership is the standing fact 0∈κ.

  Dmap : DefinableMap
  Dmap = record
    { dom = Y ; cod = κ ; fn = λ _ _ → nn 
    ; into = λ _ _ → 0∈κ
    ; graph = fo

The graph holds definitionally, since the atomic sentence equates the numeral with itself; uniqueness holds because both members of the singleton present the same underlying set.

    ; defines = λ z m → refl
    ; only = λ z m y h → S≡ h }

Injectivity composes the two outward readings: both inputs present the same underlying set as a, hence they are equal as carrier elements.

  inj : (z : S) (m : ⟨ fst z ∈ fst Y ⟩) (z' : S) (m' : ⟨ fst z' ∈ fst Y ⟩)
      → fst (nn ) ≡ fst (nn ) → fst z ≡ fst z'
  inj z m z' m' _ = Y-out z m ∙ sym (Y-out z' m')

The singleton-to-cardinal injection is packaged in the same form as every other counting piece.

  injL : InjL Y κ
  injL = Inj.injL Dmap inj

Counting every finite closure step

The counting theorem fixes an ordinal lam closed under successor, a start set X contained in Lset lam, and a proof that X is constructible. The elementarity and superadequacy hypotheses provide the closure and least-witness facts for the Skolem hull generated from X.

module Count (lam : V ℓ) (ordλ : IsOrd lam)
  (succλ : (d : V ℓ) → ⟨ d ∈ˢ lam ⟩ → ⟨ sucV d ∈ˢ lam ⟩)
  (X : V ℓ) (X⊆L : (x : V ℓ) → ⟨ x ∈ˢ X ⟩ → ⟨ x ∈ˢ Lset lam ⟩)
  (∅∈λ : ⟨ ∅ ∈ˢ lam ⟩)
  (elem : Frame.A.Elementary lam ordλ succλ X X⊆L ∅∈λ)

The counting target is an internal cardinal κ outside ω, together with a coded injection of the start into it. The task is to count the whole hull by the same cardinal.

  (sup : Superadequate lam)
  (X-isL : ⟨ isL X ⟩)
  (κ : S) (oκ : IsOrd (fst κ)) (cκ : IsCardinalL κ) (κ∉ω : ⟨ fst κ ∈ˢ ω ⟩ → Empty.⊥)
  (base : InjL (X , X-isL) κ) where

The hull is presented as the union of its finite iterates hullStep n. One closure step is governed by Φ, whose nontrivial branch records a least witness for a formula key and a finite parameter environment over the current iterate.

  module Cn = Condense′ lam ordλ succλ X X⊆L ∅∈λ elem sup X-isL
    using ( hullStep; hullL; hullStep⊆Hull )
  module B = Telescope.Build lam ordλ succλ X X⊆L ∅∈λ
    using ( A; Body
          ; LeastWitness; leastWitnessFo; leastWitness-in; leastWitness-out

For a least witness, the accompanying data recover a natural length, a finite assignment into the current set, the encoded environment, and membership of the formula key in Lset ω. Uniqueness holds after the key and environment have been fixed.

          ; LeastWitnessData; leastWitness-data; leastWitness-unique; witFo-leastWitness
          ; Φ; Φ-out; λ-isL; ω-num; pack )
  module SM = SatGraph B.A using ( pairs; pairs-out; valOf )

The finite iterates come with introduction and elimination rules, and every iterate lies in the full hull. The full hull itself is contained in Lset lam; these inclusions keep every set used by the counting construction inside the fixed ambient stage.

  module It = Telescope.HullIter.It lam ordλ succλ X X⊆L ∅∈λ X-isL B.pack
    using ( Num; iter; iter-in; iter-out; iterUnion-out; ω-num )
  module HSH = HullStage.H lam ordλ succλ X X⊆L ∅∈λ using ( Hull⊆L )
  open Cn using ( hullStep; hullL )

Because κ is an ordinal and does not belong to ω, it contains every finite numeral. Internal cardinality is not used for this conclusion; it is needed separately for the square law.

  num∈κ : (k : ℕ) → ⟨ # k ∈ fst κ ⟩
  num∈κ k = ω⊆ (fst κ) oκ κ∉ω (# k) (#∈ω k)

The infinite-cardinal square argument gives the coded injection pairκ : InjL (prodL κ) κ. It uses all three relevant hypotheses on κ: ordinality, internal cardinality, and non-membership in ω; the result is an injection, not a bijection.

  pairκ : InjL (prodL κ) κ
  pairκ = WF.WFI.induction regularityV {P = Goal} Step.result (fst κ) (snd κ) oκ cκ κ∉ω

The stage Lω = Lset ω injects into κ by composition. Limit-stage counting first gives Lω ↪ ωʟ, and the inclusion ω ⊆ κ, obtained from the ordinality and non-finiteness of κ, gives ωʟ ↪ κ.

  Lω↪κ : InjL Lω κ
  Lω↪κ = injl-trans Lω ωʟ κ limit-stage-counted
    (inclusion-coded ωʟ κ (λ z hz → ω⊆ (fst κ) oκ κ∉ω z hz))

For one closure step, fix a constructible Z contained in Lset lam and an actual graph E satisfying InjCode E Z κ. The goal is to turn this chosen stage injection into the mere coded injection InjL (Φ Z) κ.

  module OneStep (Z : S) (Z⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst Z ⟩ → ⟨ z ∈ˢ Lset lam ⟩)
                 (E : S) (cE : InjCode E Z κ) where

ΦZ = Φ Z is one closure step. Its membership description has three branches: an old member of Z, the empty-set fallback, or a least witness determined by a formula key and a finite parameter environment over Z.

    ΦZ : S
    ΦZ = B.Φ Z

The new part is separated first: D₂ collects the members of ΦZ that are not members of Z. Separation inside L keeps the new part constructible.

    opaque
      D₂ : S
      D₂ = hasSeparationL ΦZ (¬̇ (var i0 ∈̇ con Z)) .fst .fst

Its membership specification says exactly what separation computed: belonging to D₂ is belonging to ΦZ together with the refutation of belonging to Z.

      D₂-spec : (z : S) → (fst z ∈ fst D₂)
              ≡ ((fst z ∈ fst ΦZ) ⊓ ((z ∷ []) ⊨ ¬̇ (var i0 ∈̇ con Z)))
      D₂-spec z = hasSeparationL ΦZ (¬̇ (var i0 ∈̇ con Z)) .fst .snd z

The introduction rule lifts the refutation of membership into the object level, so an element of ΦZ together with a proof that it is not in Z enters D₂.

    opaque
      D₂-in : (z : S) → ⟨ fst z ∈ fst ΦZ ⟩ → (⟨ fst z ∈ fst Z ⟩ → Empty.⊥) → ⟨ fst z ∈ fst D₂ ⟩
      D₂-in z h no = subst ⟨_⟩ (sym (D₂-spec z)) (h , λ z∈ → lift (no z∈))

The elimination rule unpacks membership in D₂ through the specification, and lowers the object-level refutation back to an ordinary implication.

      D₂-out : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → ⟨ fst z ∈ fst ΦZ ⟩ × (⟨ fst z ∈ fst Z ⟩ → Empty.⊥)
      D₂-out z h = r .fst , λ z∈ → lower (r .snd z∈)
        where
        r : ⟨ fst z ∈ fst ΦZ ⟩
          × ⟨ (z ∷ []) ⊨ ¬̇ (var i0 ∈̇ con Z) ⟩

The unpacked statement is a pair: membership in ΦZ and satisfaction of the negated atom.

        r = subst ⟨_⟩ (D₂-spec z) h

Inside the new part, the elements equal to the empty set are separated out as D∅.

    opaque
      D∅ : S
      D∅ = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .fst

Its specification is the same two-fold pattern: membership in D₂ together with the equation to the empty set.

      D∅-spec : (z : S) → (fst z ∈ fst D∅)
              ≡ ((fst z ∈ fst D₂) ⊓ ((z ∷ []) ⊨ var i0 ≐ con ∅ʟ))
      D∅-spec z = hasSeparationL D₂ (var i0 ≐ con ∅ʟ) .fst .snd z

An element of D₂ that equals the empty set enters D∅ with both data.

    opaque
      D∅-in : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → fst z ≡ ∅ → ⟨ fst z ∈ fst D∅ ⟩
      D∅-in z h e = subst ⟨_⟩ (sym (D∅-spec z)) (h , e)

Its elimination is the specification read directly: membership in D₂ and the equation to the empty set.

      D∅-out : (z : S) → ⟨ fst z ∈ fst D∅ ⟩ → ⟨ fst z ∈ fst D₂ ⟩ × (fst z ≡ ∅)
      D∅-out z h = subst ⟨_⟩ (D∅-spec z) h

The remainder Dw collects the elements of D₂ that differ from the empty set.

    opaque
      Dw : S
      Dw = hasSeparationL D₂ (¬̇ (var i0 ≐ con ∅ʟ)) .fst .fst

Its specification mirrors the previous one, with the negated equation in place of the equation.

      Dw-spec : (z : S) → (fst z ∈ fst Dw)
              ≡ ((fst z ∈ fst D₂) ⊓ ((z ∷ []) ⊨ ¬̇ (var i0 ≐ con ∅ʟ)))
      Dw-spec z = hasSeparationL D₂ (¬̇ (var i0 ≐ con ∅ʟ)) .fst .snd z

Introduction requires membership in D₂ and a refutation of equality with the empty set.

    opaque
      Dw-in : (z : S) → ⟨ fst z ∈ fst D₂ ⟩ → (fst z ≡ ∅ → Empty.⊥) → ⟨ fst z ∈ fst Dw ⟩
      Dw-in z h ne = subst ⟨_⟩ (sym (Dw-spec z)) (h , λ q → lift (ne q))

Elimination returns membership in D₂ and the refutation, lowered from the object level.

      Dw-out : (z : S) → ⟨ fst z ∈ fst Dw ⟩ → ⟨ fst z ∈ fst D₂ ⟩ × (fst z ≡ ∅ → Empty.⊥)
      Dw-out z h = r .fst , λ q → lower (r .snd q)
        where
        r : ⟨ fst z ∈ fst D₂ ⟩
          × ⟨ (z ∷ []) ⊨ ¬̇ (var i0 ≐ con ∅ʟ) ⟩

Two unions provide the bounds needed later. U₁ contains Z and the genuinely new part D₂, while U₃ contains the empty-valued part D∅ and the nonempty witness part Dw. The next lemmas prove the required inclusions into these unions.

        r = subst ⟨_⟩ (Dw-spec z) h
    module U₁ = Union2 Z D₂ using ( D; in₁; in₂ )
    module U₃ = Union2 D∅ Dw using ( D; in₁; in₂ )

The closure step is covered by the first union. Each member z of ΦZ either belongs to Z or does not, decided by excluded middle; in both cases z is constructible, because ΦZ is.

    ΦZ⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst ΦZ ⟩ → ⟨ z ∈ˢ fst U₁.D ⟩
    ΦZ⊆ z h = go (lem (z ∈ fst Z))
      where
      zS : S
      zS = z , isL-trans {x = fst ΦZ} {y = z} h (snd ΦZ)

The two cases enter U₁ through its two union inclusions. A member already in Z uses the first inclusion; otherwise D₂-in first proves that it belongs to the new part, after which the second inclusion applies.

      go : ⟨ z ∈ fst Z ⟩ ⊎ (⟨ z ∈ fst Z ⟩ → Empty.⊥) → ⟨ z ∈ fst U₁.D ⟩
      go (inl hz) = U₁.in₁ zS hz
      go (inr no) = U₁.in₂ zS (D₂-in zS h no)

The new part is covered by the second union, by the same excluded-middle argument on the equation with the empty set.

    D₂⊆ : (z : V ℓ) → ⟨ z ∈ˢ fst D₂ ⟩ → ⟨ z ∈ˢ fst U₃.D ⟩
    D₂⊆ z h = go (lem ((z ≡ ∅) , setIsSet z ∅))
      where
      zS : S
      zS = z , isL-trans {x = fst D₂} {y = z} h (snd D₂)

An element equal to the empty set enters through D∅; an element distinct from it enters through Dw.

      go : (z ≡ ∅) ⊎ (z ≡ ∅ → Empty.⊥) → ⟨ z ∈ fst U₃.D ⟩
      go (inl e)  = U₃.in₁ zS (D∅-in zS h e)
      go (inr ne) = U₃.in₂ zS (Dw-in zS h ne)

Every member of D∅ equals ∅, although D∅ itself may be empty. Since the numeral 0 belongs to κ, inclusion coding therefore gives D∅ ↪ κ inside L.

    D∅↪κ : InjL D∅ κ
    D∅↪κ = inclusion-coded D∅ κ
      (λ z hz → subst (λ w → ⟨ w ∈ fst κ ⟩)
        (sym (D∅-out (z , isL-trans {x = fst D∅} {y = z} hz (snd D∅)) hz .snd)) (num∈κ ))

A second union prepares the coding of witnesses: U₂ joins the elements born by stage ω with the finite sequences of members of Z.

    module U₂ = Union2 Lω (seqL Z) using ( D; in₁; in₂ )

Let PB be the square of U₂ = Lω ∪ seqL Z. Every actual witness code (s,e), with s ∈ Lω and e ∈ seqL Z, lies in PB; PB is a homogeneous upper bound and also contains pairs that are not valid witness codes.

    PB : S
    PB = prodL U₂.D

The least-witness formula is pinned at the fixed base Z. The resulting five-variable formula pin₅ is satisfied at the frame (e,s,z,p,q) exactly when z is the least witness determined by the environment e and key s; the last two slots are carried by the surrounding frame.

    opaque
      pin₅ : Formula S 
      pin₅ = pinAt Z B.leastWitnessFo

Inward, a least witness for z at the parameter environment e with key s yields the satisfaction of the pinned formula at the five-slot context.

      pin₅-in : (e s z p q : S) → B.LeastWitness Z e s z
              → ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩
      pin₅-in e s z p q h =
        pin-in Z B.leastWitnessFo (e ∷ s ∷ z ∷ p ∷ q ∷ [])
          (B.leastWitness-in Z e s z p q h)

Outward, satisfaction of the pinned formula unpacks to a least witness, the pinning being inverted by the pinning lemma.

      pin₅-out : (e s z p q : S) → ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩
               → B.LeastWitness Z e s z
      pin₅-out e s z p q h =
        B.leastWitness-out Z e s z p q
          (pin-out Z B.leastWitnessFo (e ∷ s ∷ z ∷ p ∷ q ∷ []) h)

The relation to be counted is propositionally truncated. GW p z says merely that there are a key s and an environment e such that p = (s,e) and z is their least witness.

    GW : (p z : S) → Type (ℓ-suc ℓ)
    GW p z = ∥ Σ[ s ∈ S ] Σ[ e ∈ S ]
               ((fst p ≡ pr (fst s) (fst e)) × B.LeastWitness Z e s z) ∥₁

The same relation is written as a formula: two existentials bind the key and the environment, the pairing atom identifies p, and the pinned formula carries the witness condition.

    opaque
      se₃ : Formula S 
      se₃ = ∃̇ (∃̇ (prAtL i3 i1 i0 ∧̇ pin₅))

Inward: given the pair equation and a least witness, the two witnesses are entered and the pair atom is transported along its adequacy into the object language.

      se₃-in : (z p q s e : S) → fst p ≡ pr (fst s) (fst e)
             → B.LeastWitness Z e s z → ⟨ (z ∷ p ∷ q ∷ []) ⊨ se₃ ⟩
      se₃-in z p q s e qp h =
        ∣ s , ∣ e , ( subst ⟨_⟩ (sym (prAtL-adequate i3 i1 i0 (e ∷ s ∷ z ∷ p ∷ q ∷ []))) qp
                    , pin₅-in e s z p q h ) ∣₁ ∣₁

Outward, the two existentials are consumed one at a time; the first step strips the outer quantifier and keeps the entry s with the truncated remainder.

      se₃-out : (z p q : S) → ⟨ (z ∷ p ∷ q ∷ []) ⊨ se₃ ⟩ → GW p z
      se₃-out z p q = PT.rec squash₁ at₁
        where
        at₂ : (s : S) → Σ[ e ∈ S ] ( ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
                                   × ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩ ) → GW p z

After the second existential is opened, adequacy of the pairing atom recovers p = (s,e), and the outward reading of the pinned formula recovers the least-witness condition. These witnesses are then placed back under the propositional truncation defining GW.

        at₂ s (e , (qp , h)) = ∣ s , e
          , ( subst ⟨_⟩ (prAtL-adequate i3 i1 i0 (e ∷ s ∷ z ∷ p ∷ q ∷ [])) qp
            , pin₅-out e s z p q h ) ∣₁
        at₁ : Σ[ s ∈ S ] ∥ Σ[ e ∈ S ] ( ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ prAtL i3 i1 i0 ⟩
                                      × ⟨ (e ∷ s ∷ z ∷ p ∷ q ∷ []) ⊨ pin₅ ⟩ ) ∥₁ → GW p z

Because GW p z is a proposition, the remaining outer truncation can be eliminated into it. Together, se₃-in and se₃-out give the two implications between the host relation GW and satisfaction of its object-language formula.

        at₁ (s , h) = PT.rec squash₁ (at₂ s) h

Bounded separation constructs a relation G inside L whose entries are ordered pairs (p,z) with p ∈ PB, z ∈ Dw, and GW p z. Thus G restricts the least-witness relation to the chosen code pool and the nonempty new part.

    private
      module WitnessGraph = Relation PB Dw ((var i1 ∈̇ con PB) ∧̇ se₃)
        (λ p z → (fst p ∈ fst PB) ⊓ (GW p z , squash₁))
        (λ p z q h → h .fst , se₃-out z p q (h .snd))
        (λ p z q h → h .fst , PT.rec (snd ((z ∷ p ∷ q ∷ []) ⊨ se₃))

The outward reading of the describing condition is the formula's own outward reading, which returns exactly the data of GW.

          (λ { (s , e , qp , hw) → se₃-in z p q s e qp hw }) (h .snd))

G is the resulting constructible relation, represented as a set of ordered pairs (p,z). It relates a candidate code in PB to an element of Dw when that code carries least-witness data for the element.

    G : S
    G = WitnessGraph.rel

Inward: a code p in PB that, together with z, names a least witness through some key and environment, belongs to G.

    G-in : (p z : S) → ⟨ fst p ∈ fst PB ⟩ → ⟨ fst z ∈ fst Dw ⟩
         → (s e : S) → fst p ≡ pr (fst s) (fst e)
         → B.LeastWitness Z e s z → Holds G p z
    G-in p z hp hz s e qp h =
      WitnessGraph.into p z hp hz (hp , ∣ s , e , qp , h ∣₁)

Conversely, Holds G p z yields both p ∈ PB and the propositionally truncated witness data GW p z. It does not choose a key and environment outside that truncation.

    G-out : (p z : S) → Holds G p z → ⟨ fst p ∈ fst PB ⟩ × GW p z
    G-out = WitnessGraph.pair-out

The relation is total on Dw only in the truncated sense: every z ∈ Dw merely has some p with Holds G p z. Reading membership in ΦZ exposes the three possible reasons why z entered the closure step.

    have : (z : S) → ⟨ fst z ∈ fst Dw ⟩ → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
    have z hz = PT.rec squash₁ body (B.Φ-out Z z (D₂-out z (Dw-out z hz .fst) .fst))
      where
      body : B.Body Z z → ∥ Σ[ p ∈ S ] Holds G p z ∥₁
      body (inl h) = Empty.rec (D₂-out z (Dw-out z hz .fst) .snd h)

Two of them are already excluded by the separators: z cannot be an old member of Z, nor the empty set. What remains is the witness case, read through the outward lemma of the witness formula.

      body (inr (inl e)) = Empty.rec (Dw-out z hz .snd e)
      body (inr (inr hw)) = PT.rec squash₁ read (B.witFo-leastWitness z Z hw)
        where
        read : Σ[ e ∈ S ] Σ[ s ∈ S ] B.LeastWitness Z e s z
             → ∥ Σ[ p ∈ S ] Holds G p z ∥₁

The witness branch supplies an environment e, a key s, and a least witness. Its data lemma then gives a natural length n, a meta-level assignment g : Fin n → ⟪Z⟫, an equation identifying e with the encoded environment of g, and the membership s ∈ Lset ω.

        read (e , s , hw') = PT.map at (B.leastWitness-data Z e s z hw')
          where
          at : B.LeastWitnessData Z e s → Σ[ p ∈ S ] Holds G p z
          at (n , g , qe , hs) = prʟ s e
            , G-in (prʟ s e) z

The code p is the internal pair of the key and the environment. Its membership in PB is built entry by entry: the key enters through Lω because it lies in Lset ω, and the environment enters through the finite sequences of Z, being the environment of a length-n assignment into Z. The relation then accepts the pair.

                (subst (λ w → ⟨ w ∈ fst PB ⟩) (sym (prʟ-fst s e))
                  (prodL-in U₂.D s e (U₂.in₁ s hs)
                    (U₂.in₂ e (seqL-in Z n e
                      (subst (λ w → ⟨ w ∈ˢ fst (envSet Z n) ⟩) (sym qe) (envSet-in Z g))))))
                hz s e (prʟ-fst s e) hw'

Uniqueness for a witness key

The required functionality has the reverse orientation needed for counting: if one fixed code p is related both to z and to z', then z and z' have equal underlying sets. Different codes for the same element are still allowed.

    funct : (p z z' : S) → Holds G p z → Holds G p z' → fst z ≡ fst z'
    funct p z z' h h' = PT.rec2 (setIsSet (fst z) (fst z')) read (G-out p z h .snd) (G-out p z' h' .snd)
      where
      read : Σ[ s ∈ S ] Σ[ e ∈ S ]
               ((fst p ≡ pr (fst s) (fst e)) × B.LeastWitness Z e s z)

Both relations are read outward, each returning a key, an environment, the pair equation, and a least witness.

           → Σ[ s₂ ∈ S ] Σ[ e₂ ∈ S ]
               ((fst p ≡ pr (fst s₂) (fst e₂)) × B.LeastWitness Z e₂ s₂ z')
           → fst z ≡ fst z'
      read (s , e , q , hw) (s₂ , e₂ , q₂ , hw₂) =
        B.leastWitness-unique Z e s z z' hw hw₂'

Both readings express the same fixed p as (s,e) and (s₂,e₂). Injectivity of ordered-pair coding identifies the two keys and the two environments at the level of underlying sets, and proof irrelevance lifts those equalities to the corresponding elements of S.

        where
        ee : (fst s₂ ≡ fst s) × (fst e₂ ≡ fst e)
        ee = pr-inj (sym q₂ ∙ q)
        hw₂' : B.LeastWitness Z e s z'
        hw₂' = subst2 (λ e' s' → B.LeastWitness Z e' s' z')

After transporting the second least-witness proof along those identifications, both proofs concern the same key and environment. Least-witness uniqueness then gives fst z ≡ fst z'.

          (S≡ {x = e₂} {y = e} (snd ee)) (S≡ {x = s₂} {y = s} (fst ee)) hw₂

The code pool has a birth stage: γG is the stage at which PB appears in the hierarchy.

    γG : V ℓ
    γG = stage (fst PB) (snd PB)

That stage is indexed by an ordinal, which is what the counting lemma requires of it.

    oγG : IsOrd γG
    oγG = stage-ord (fst PB) (snd PB)

The pool is contained in its birth stage, by the transitivity of the stages: a member of a set born at γG belongs to Lset γG.

    PB⊆Lγ : (p : S) → ⟨ fst p ∈ fst PB ⟩ → ⟨ fst p ∈ Lset γG ⟩
    PB⊆Lγ p hp = layer-trans (Lset-layer γG) {x = fst PB} {y = fst p} hp (stage-mem (fst PB) (snd PB))

The hypotheses now instantiate LeastPre: every z ∈ Dw merely has a related code in PB, and a fixed code determines at most one such z. Least selection chooses one code for each element and yields InjL Dw PB. It does not assert that witness codes were unique beforehand, and this is only the count of the nonempty new part, not yet the full one-step result.

    module LP = LeastPre γG oγG G Dw PB (λ p z h → G-out p z h .fst) PB⊆Lγ have
      using ( module Functional )

The least-preimage construction injects the genuinely new witnesses into PB. Each z ∈ Dw merely has some related code, and the stage order selects the least such code. Codes need not be unique before selection; injectivity follows instead because a fixed code can represent only one witness.

    Dw↪PB : InjL Dw PB
    Dw↪PB = LP.Functional.injL funct

The injection Z ↪ κ acts coordinatewise on finite sequences, giving seqL Z ↪ seqL κ. Composing with finite-sequence counting yields seqL Z ↪ κ; this second map requires only that κ be an infinite ordinal, not that it be an internal cardinal.

    seq↪κ : InjL (seqL Z) κ
    seq↪κ = injl-trans (seqL Z) (seqL κ) κ (seq-map Z κ E cE) (seq-count κ oκ κ∉ω)

First count U₂.D = Lω ∪ seqL Z: tagging its two summands gives an injection into κ × κ, and pairκ folds that product into κ. Since PB = U₂.D × U₂.D, prod-inj lifts this injection to PB ↪ κ × κ; a second use of pairκ then gives PB ↪ κ. The two folds are the steps that use the square law and hence internal cardinality.

    PB↪κ : InjL PB κ
    PB↪κ = injl-trans PB (prodL κ) κ
      (prod-inj U₂.D κ
        (injl-trans U₂.D (prodL κ) κ (tag-union κ (num∈κ ) (num∈κ ) Lω (seqL Z) Lω↪κ seq↪κ) pairκ))
      pairκ

Composing the two injections gives the count of the genuinely new witnesses: every such witness is coded by some p ∈ PB, and PB injects into κ, so Dw injects into κ.

    Dw↪κ : InjL Dw κ
    Dw↪κ = injl-trans Dw PB κ Dw↪PB PB↪κ

The new part D₂ is included in D∅ ∪ Dw. Here D∅ contains precisely the new members equal to the empty set and may itself be empty, while Dw contains the nonempty witness members. Their two counts are tagged into κ × κ and folded by pairκ, giving D₂ ↪ κ.

    D₂↪κ : InjL D₂ κ
    D₂↪κ = injl-trans D₂ U₃.D κ (inclusion-coded D₂ U₃.D D₂⊆)
      (injl-trans U₃.D (prodL κ) κ (tag-union κ (num∈κ ) (num∈κ ) D∅ Dw D∅↪κ Dw↪κ) pairκ)

Every member of ΦZ lies in Z ∪ D₂. The given graph E counts Z, while the preceding construction counts D₂; tagging these injections gives a map into κ × κ, and pairκ completes the injection ΦZ ↪ κ.

    result : InjL ΦZ κ
    result = injl-trans ΦZ U₁.D κ (inclusion-coded ΦZ U₁.D ΦZ⊆)
      (injl-trans U₁.D (prodL κ) κ (tag-union κ (num∈κ ) (num∈κ ) Z D₂ ∣ E , cE ∣₁ D₂↪κ) pairκ)