Turning a definable injection into an internal code

A rule described outside L is not yet an object over which L can quantify. To compare cardinalities internally, we need a constructible set of ordered pairs recording the rule's values. The central question is therefore how definability and pointwise uniqueness let Replacement collect that graph.

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

The sole classical parameter is excluded middle at level ℓ-suc ℓ. The elementary steps in this chapter, such as proving uniqueness, transporting membership, and eliminating a propositional truncation into a proposition, are constructive. The parameter matters when the general Replacement theorem collects the graph as an element of L; no form of choice is used.

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

Fix a universe level ℓ and this instance of excluded middle. The mathematical problem is to pass from a host-level rule to a set that L can quantify over. The rule itself is not inserted into L. Instead, a formula describes its values on a set of L, Replacement forms a constructible graph, and an injectivity proof equips that graph with the code used for internal cardinal comparisons.

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

Three kinds of object must be kept distinct. A formula belongs to the first-order language whose constants are elements of the constructible carrier; satisfaction interprets it in the structure on L; and pr is the ambient Kuratowski code for an ordered pair of underlying sets. Later the defining formula will be read with the value first and the input second, while an entry of the collected graph is pr(input,value).

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )

The proof passes through three mathematical forms. A recursion consists of a domain, a value formula, and a proof that the satisfying-value fiber at each domain point is contractible. Its graph construction uses Replacement to collect ordered pairs and proves single-valuedness and the exact domain. Finally, injAt expresses the remaining injectivity condition: two entries with the same output have equal inputs.

open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Recursion {ℓ} lem using ( Recursion )
open import L.Recursion.Graph {ℓ} lem
  using () renaming ( module Graph to RecursionGraph )
open import L.Coding.Injection {ℓ} lem using ( injAt; injAt-in )

For sets a and b, InjCode F a b has exactly four components. The graph F is single-valued, has domain exactly a, is injective, and every value appearing in it belongs to b. The first three components are satisfaction judgments for object-language formulas; the fourth is a host-level range condition. InjL a b propositionally truncates the existence of such an F and its code.

open import L.Cardinal {ℓ} lem using ( InjCode; InjL )

Two type-theoretic facts govern the proof. When the second component of a dependent pair is proposition-valued, Σ≡Prop lifts a path between first components to a path between the pairs. A propositional truncation retains only inhabitedness. The graph reader pair-out may eliminate a truncated origin because its target fiber is a proposition, while the final step uses ∣_∣₁ to hide the particular graph and code. Neither operation selects a global family of witnesses.

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

The carrier S comes from the structure on L: an element x : S consists of an ambient set fst x together with a propositional certificate that it is constructible. Membership notation is taken from the ambient hierarchy, so expressions in the record explicitly compare underlying sets, such as fst x ∈ˢ fst dom. The certificates remain available in the second components whenever a construction must return an element of L.

open hPropStructure 𝒮ʟ using ( S )
open hPropStructure 𝒮ᵥ using ( _∈ˢ_ )

The notation _⊨_ is satisfaction in the structure obtained by restricting the ambient hierarchy to constructible sets. Thus (y ∷ x ∷ []) ⊨ graph evaluates graph with elements of L in its two free slots. The name AbsL does not assert that arbitrary formulas are absolute between L and the ambient hierarchy; this chapter uses the restricted semantics and the already proved Replacement theorem.

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

What it means for a function to be definable

A DefinableMap first specifies two elements dom and cod of L, with no assumption that they are ordinals or cardinals. Its host-level rule fn is defined only for a pair consisting of x : S and evidence m that x belongs to dom; no value outside the domain is required. The type permits fn x m to mention m. Since membership is a proposition, any two such proofs are equal, and congruence identifies the corresponding values. The field into proves that every selected value belongs to cod.

record DefinableMap : Type (ℓ-suc (ℓ-suc ℓ)) where
  field
    dom cod : S
    fn      : (x : S) → ⟨ fst x ∈ˢ fst dom ⟩ → S
    into    : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩) → ⟨ fst (fn x m) ∈ˢ fst cod ⟩

The remaining fields connect the host-level values to an object-language formula. graph has two free slots and may contain constants from S; it need not be Δ₀. At every x ∈ dom, defines proves that the environment has the chosen value first and x second, while only proves that every satisfying y equals that chosen value in S. These conditions say nothing about inputs outside dom, and only does not assume that its candidate y belongs to cod. The separate field into supplies codomain containment for the selected values.

    graph   : Formula S 
    defines : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩)
            → ⟨ (fn x m ∷ x ∷ []) ⊨ graph ⟩
    only    : (x : S) (m : ⟨ fst x ∈ˢ fst dom ⟩) (y : S)
            → ⟨ (y ∷ x ∷ []) ⊨ graph ⟩ → y ≡ fn x m

Encoding graph entries as ordered pairs

The graph is represented as a set, so each input-output entry must first be expressed as an ordered pair. The defining formula reads the value in its first semantic slot and the input in its second, whereas the set encoding stores the corresponding entry as pr(input,value). Keeping these two orders distinct is essential when the graph is constructed and later read back.

Constructing the graph inside L

The first construction assumes only definability and functionality. From M it will form the complete graph as an element of L and obtain precise ways to insert and read its ordered-pair entries. Injectivity is deliberately postponed: the same graph construction also applies to definable maps, such as a table of least witnesses, whose purpose does not require them to be injective.

module Graph (M : DefinableMap) where
  open DefinableMap M public

To meet the recursion hypothesis, retain dom and graph and prove that the satisfying-value fiber at each domain point has a center. The center is the pair (fn x m, defines x m): the given value together with its satisfaction proof. The membership evidence m is passed directly to fn, so this construction does not extend the rule beyond dom. Neither into nor injectivity is needed at this stage.

  private
    R : Recursion
    R = record
      { dom = dom ; graph = graph
      ; funct = λ x m → (fn x m , defines x m)

It remains to contract every candidate (y,h) to that center. The field only gives y ≡ fn x m, but contractibility asks for a path from the center to the candidate, hence the use of sym. The second component is a satisfaction proof and therefore a proposition. Σ≡Prop consequently lifts the reversed equality of values to equality of the whole dependent pairs. This establishes the required unique existence constructively.

          , λ { (y , h) → Σ≡Prop (λ w → snd ((w ∷ x ∷ []) ⊨ graph)) (sym (only x m y h)) } }

Replacement now collects the ordered-pair values into a constructible set F. The auxiliary pairing formula reconciles the two conventions: the original relation is evaluated as (value,input), while members of F are pr(input,value). F-in inserts every prescribed entry, and F-out says under propositional truncation that every member has such an origin. For fixed x and y, pair-out strengthens membership of pr(x,y) to a domain proof and an equality y = fn(x). This elimination is valid because Fib x y is a proposition, using proof irrelevance of membership and the fact that equality in V is proposition-valued. These readings prove sv, single-valuedness, and dm, that the domain is exactly dom. Forming F is the step that uses the Replacement theorem and hence the given excluded middle; the subsequent readings introduce no choice.

  open RecursionGraph R public
    using ( Mem; isPropMem; F; F-in; F-out; Fib; isPropFib; pair-out; γ; sv; dm )

The fourth condition for the eventual code is containment in the codomain. Given an actual graph entry pr(fst x,fst y) ∈ fst F, pair-out yields m : x ∈ dom and e : fst y ≡ fst(fn x m). The field into x m proves membership of fst(fn x m) in fst cod. Transport must therefore follow sym e, from the chosen value back to y, to conclude y ∈ cod. This proves only that the image is contained in the codomain, not that every codomain element occurs.

  ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → ⟨ fst y ∈ fst cod ⟩
  ran x y h = subst (λ w → ⟨ w ∈ fst cod ⟩) (sym e) (into x m)
    where
    m = fst (pair-out x y h)
    e = snd (pair-out x y h)

From external injectivity to a coded injection

To turn this graph into an injection code, add the genuinely new hypothesis of injectivity. For two inputs equipped with proofs of membership in dom, it says that equality of the underlying sets of their selected values implies equality of the underlying input sets. The membership arguments remain explicit because fn is dependently typed in them. Their proof irrelevance guarantees coherence between different proofs, but the hypothesis is stated with the exact evidence supplied at the two inputs. Its conclusion has precisely the strength required by the equality clause of injAt.

module Inj (M : DefinableMap)
           (inj : (x : S) (m : ⟨ fst x ∈ˢ fst (DefinableMap.dom M) ⟩)
                  (x' : S) (m' : ⟨ fst x' ∈ˢ fst (DefinableMap.dom M) ⟩)
                → fst (DefinableMap.fn M x m) ≡ fst (DefinableMap.fn M x' m')
                → fst x ≡ fst x') where

Opening Graph M makes the already constructed F and its proved properties available in the injective case. This keeps two mathematically useful conclusions at hand. One may retain the particular graph F together with its code when a later construction must name or combine graphs. One may instead use injL, which remembers only that some coded injection exists. The distinction is between concrete data and its propositional existence.

  open Graph M public

The formula injAt zero fixes an output y and compares two inputs x and x': if both pr(x,y) and pr(x',y) lie in F, then the inputs are equal. Applying pair-out to the first entry gives e : y = fn(x), and applying it to the second gives e' : y = fn(x'), together with the two required domain proofs. Hence sym e ∙ e' is the path fn(x) = fn(x'); the host-level hypothesis inj turns it into x = x', and injAt-in translates this property into the satisfaction judgment ij. This argument uses injectivity, not merely only: only compares outputs at one fixed input and is what underlies single-valuedness.

  ij : ⟨ γ ⊨ injAt zero ⟩
  ij = injAt-in zero γ (λ y x x' p q →
    let (m , e)   = pair-out x y p
        (m' , e') = pair-out x' y q
    in inj x m x' m' (sym e ∙ e'))

The tuple sv , dm , ij , ran fills the four fields of InjCode F dom cod in order. Here sv proves single-valuedness, dm proves that the graph domain is exactly dom, and ij proves object-language injectivity, all in the environment F ∷ dom ∷ []. The final field ran states at host level that values occurring in F belong to cod. Nothing in this code asserts surjectivity, so it describes an injection into cod, not a bijection.

  code : InjCode F dom cod
  code = sv , dm , ij , ran

Finally, the concrete pair (F,code) is inserted into a propositional truncation. The resulting term injL : InjL dom cod states that a constructible graph carrying an injection code exists, while forgetting which graph was constructed. This is the proposition needed in cardinal comparisons and can be eliminated when the desired conclusion is again a proposition. The particular F and code remain separately available within the instantiated module when a construction needs them. Thus it is the coded graph, not the external rule itself, that has been internalized in L.

  injL : InjL dom cod
  injL = ∣ F , code ∣₁