Coded injections

Later cardinal arguments repeatedly move between two representations of an injection: a graph that a formula can quantify over, and an actual function between the small member types of sets. The gap between them is filled in three layers. The object language first needs a formula saying that the graph is injective, the mirror of the single-valuedness clause already available. Then, assuming single-valuedness and an exact domain, the graph can be read as a genuine function whose values remain elements of the constructible model. Finally that function transfers to the canonical small presentations of a stated domain and range. This chapter adds the injectivity formula and carries out both readback layers used by the Cantor-Bernstein and GCH constructions.

The construction is valid constructively. Although the ambient development carries LEM (ℓ-suc ℓ), the proofs below never invoke it: existence of a graph value is truncated, but single-valuedness makes the entire image fiber a proposition, so truncation elimination recovers its unique inhabitant without a choice principle.

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

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

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

Let S be the carrier of the constructible model. An element of S consists of an ambient set in V ℓ together with evidence that it is constructible. Consequently graph assertions are statements about the first projections. The formulas for application, single-valuedness, and exact domain connect internal satisfaction with precisely these projected graph facts.

open import FOL.ZFStructure using ( module hPropStructure )
open import FOL.Syntax using ( Formula; var; _≐_; _⇒̇_; ∀̇_ )
import FOL.Absoluteness
open import V.Hierarchy {ℓ} using ( 𝒮ᵥ )
open import V.Coding {ℓ} using ( pr )

The second readback layer needs the canonical presentation machinery: a set presented by an index type and an indexing map, with member turning an index into an explicit membership proof and fiber doing the converse by returning an actual index, not a truncated one. Σ≡Prop will reduce equality of dependent pairs to equality of first components when the second components are propositions, which is exactly how the fiber of images and the pairs of the model carrier are handled.

open import L.Constructible {ℓ} using ( 𝒮ʟ; isL; isL-trans )
open import L.Coding.Model {ℓ} using ( appAt; appAt-adequate; svAt; svAt-out; domAt; domAt-in )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import Cubical.HITs.CumulativeHierarchy.Properties using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.Data.Sigma using ( Σ≡Prop )

Truth values here are propositions with their proofs of propositionhood, and the satisfaction relation uses the logical connectives directly on hProp. The satisfaction judgment _⊨_ is then stated for the constructible structure 𝒮ʟ, so a judgment such as γ ⊨ svAt zero is a claim about the projected sets via the adequacy identifications, not about bare satisfaction in an ambient structure.

open import Cubical.HITs.CumulativeHierarchy.Base using ( _∈_ )
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∥_∥₁ )

open hPropStructure 𝒮ʟ using ( S )

Bounded absoluteness relates satisfaction in the constructible model to satisfaction after projecting an assignment with fst. This bridge is used only where an adequacy theorem is applied. It does not turn Extract.toFun into an injection by itself: injectivity enters later as the separate hypothesis ij.

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

Injectivity in the object language

A single-valued graph fixes one input and compares outputs: if two entries share the same first component, their second components agree. Injectivity is the mirror image: it fixes one output and compares inputs. Concretely, if both (x, y) and (x', y) belong to the graph, then the first components of x and x' must be equal. Stating this as a formula of the object language is what lets a cardinal argument quantify over injective graphs inside the model, so this section defines injAt and proves that, under the adequacy identifications for application, the formula holds exactly when the projected graph has the injectivity property.

The formula binds the assignment x′ ∷ x ∷ y ∷ γ: slot 0 is x′, slot 1 is x, and slot 2 is y, while the old graph slot f becomes f + 3. Its two premises say that (x,y) and (x′,y) belong to that graph, and its conclusion equates x and x′. Thus it fixes the output and compares the inputs, exactly the mirror of single-valuedness.

injAt : ∀ {n} → Fin n → Formula S n
injAt f = ∀̇ (∀̇ (∀̇ (
      appAt (suc (suc (suc f))) (suc zero) (suc (suc zero))
  ⇒̇ (appAt (suc (suc (suc f))) zero (suc (suc zero))
  ⇒̇ (var (suc zero) ≐ var zero)))))

For the readback, fix a variable index f and an environment γ of model elements. Holds₀ x y is the projected fact that the ordered pair of the underlying sets of x and y belongs to the underlying graph, the graph being the entry that variable f selects from γ. Both directions below compare a satisfaction judgment of an application clause with this Holds₀, so the adequacy paths are the pivot of the whole argument.

module _ {n : ℕ} (f : Fin n) (γ : S ^ n) where
  private
    Holds₀ : S → S → Type (ℓ-suc ℓ)
    Holds₀ x y = ⟨ pr (fst x) (fst y) ∈ fst (lookup f γ) ⟩

    at₁ : (y x x' : S)

The path at₁ records the adequacy of the first application clause in the extended environment x' ∷ x ∷ y ∷ γ: satisfaction there is identified with the projected membership of the pair (x, y) in the graph. The identification is an equality of propositions, given by appAt-adequate at the stated variable indices, so it can be transported along in either direction.

        → ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) (suc zero) (suc (suc zero)))
        ≡ (pr (fst x) (fst y) ∈ fst (lookup f γ))
    at₁ y x x' = appAt-adequate (suc (suc (suc f))) (suc zero) (suc (suc zero))
                   (x' ∷ x ∷ y ∷ γ)

    at₂ : (y x x' : S)

The path at₂ is the same statement for the other clause: satisfaction of the application at variables 0 and 2 equals the projected membership of (x', y). The two paths differ only in which first component is fed into the pair code, which is precisely the asymmetry that injectivity exploits.

        → ((x' ∷ x ∷ y ∷ γ) ⊨ appAt (suc (suc (suc f))) zero (suc (suc zero)))
        ≡ (pr (fst x') (fst y) ∈ fst (lookup f γ))
    at₂ y x x' = appAt-adequate (suc (suc (suc f))) zero (suc (suc zero))
                   (x' ∷ x ∷ y ∷ γ)

  injAt-out : ⟨ γ ⊨ injAt f ⟩

The outward direction injAt-out starts from a proof that the formula holds at γ and two membership facts Holds₀ x y and Holds₀ x' y. Instantiating the three quantifiers yields a satisfaction proof of the implication body at the extended environment; the membership facts are then transported along the reverses of at₁ and at₂, turning them into satisfaction proofs of the two antecedent clauses. The final fst x ≡ fst x' is read off inside the model's equality.

            → (y x x' : S) → Holds₀ x y → Holds₀ x' y → fst x ≡ fst x'
  injAt-out h y x x' p q = h y x x'
    (subst ⟨_⟩ (sym (at₁ y x x')) p) (subst ⟨_⟩ (sym (at₂ y x x')) q)

  injAt-in : ((y x x' : S) → Holds₀ x y → Holds₀ x' y → fst x ≡ fst x')
           → ⟨ γ ⊨ injAt f ⟩

The inward direction injAt-in runs the same transports forward: given the projected injectivity property as a hypothesis on Holds₀, it transports the two membership facts along at₁ and at₂ themselves to obtain satisfaction of the two antecedents, and the hypothesis then produces the equality the formula's conclusion asks for. Together the two directions say the formula is adequate for injectivity, not stronger and not weaker.

  injAt-in h y x x' p q = h y x x'
    (subst ⟨_⟩ (at₁ y x x') p) (subst ⟨_⟩ (at₂ y x x') q)

Extracting an injection into the model

Assuming a graph is single-valued and has an exact domain, every element of the domain has some image in the graph, but only a merely existing one: domain membership yields a propositional truncation, not a chosen witness. Single-valuedness upgrades the situation. It shows that for a fixed input, the type of pairs consisting of an output and a proof that the pair belongs to the graph is a proposition, and a truncated value can always be eliminated into a proposition. Thus the graph yields a genuine function into the model. Only after the additional injectivity hypothesis is supplied does toFun-inj show that this function is injective. This first readback layer keeps values as elements of the carrier, the form used when later proofs still reason about the coded graph.

The section takes the graph F and the domain D as model elements, together with the two satisfaction hypotheses: single-valuedness of the graph at variable zero, and the exact-domain clause saying that every element of D has a value under F. The environment γ packages them in the fixed order the satisfaction judgments expect.

module Extract (F D : S)
               (sv : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩)
               (dm : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩) where

  γ : S ^ 
  γ = F ∷ D ∷ []

Holds x y is the projected membership of the pair of underlying sets in the underlying graph. The fiber Fib x pairs an output y with such a proof; it is the type whose elements are candidate values of the graph at x, each carrying its own certificate that it really is a value.

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

  Fib : S → Type (ℓ-suc ℓ)
  Fib x = Σ[ y ∈ S ] Holds x y

  isPropFib : (x : S) → isProp (Fib x)

To prove Fib x proposition-valued, compare (y,p) and (y′,q). Single-valuedness supplies the path fst y ≡ fst y′. The inner Σ≡Prop lifts this path to y ≡ y′ because the second component of an element of S, its isL certificate, is a proposition. The outer Σ≡Prop then lifts that equality to the two elements of Fib x because graph-membership proofs are propositions. These are two distinct proof-irrelevance steps; neither says that equality of ambient sets follows merely from constructibility.

  isPropFib x (y , p) (y' , q) =
    Σ≡Prop (λ w → snd (pr (fst x) (fst w) ∈ fst F))
      (Σ≡Prop (λ z → snd (isL z)) (svAt-out zero γ sv x y y' p q))

  toVal : (x : S) → ∥ Fib x ∥₁ → Fib x
  toVal x = PT.rec (isPropFib x) (λ z → z)

Because Fib x is a proposition, toVal can eliminate the truncated existence of a value, ∥ Fib x ∥₁, into an actual fiber. This is the one place where a choice could seem to be hiding, and it is not: propositional truncation eliminates into any proposition-valued target, so no law of excluded middle and no selection of a canonical representative is needed. The domain Dom then packages an input with the projected proof that it belongs to D, and fib feeds each input's truncated image, obtained from domAt-in, through toVal.

  Dom : Type (ℓ-suc ℓ)
  Dom = Σ[ x ∈ S ] ⟨ fst x ∈ fst D ⟩

  fib : (u : Dom) → Fib (fst u)
  fib (x , m) = toVal x (domAt-in zero (suc zero) γ dm x m)

  toFun : Dom → S

The function toFun sends a domain entry to the output y : S in its unique fiber. It discards only the accompanying graph-membership proof; the output remains a model element and therefore retains its constructibility certificate. The theorem toFun-graph recovers exactly that discarded membership evidence as the second component of the fiber.

  toFun u = fst (fib u)

  toFun-graph : (u : Dom) → Holds (fst u) (toFun u)
  toFun-graph u = snd (fib u)

  module _ (ij : ⟨ γ ⊨ injAt zero ⟩) where

    toFun-inj : (u v : Dom) → fst (toFun u) ≡ fst (toFun v)

With injectivity of the graph also assumed, toFun-inj turns equality of outputs into equality of inputs. If the underlying sets of toFun u and toFun v agree, the graph equation of u is transported along that path so that both entries speak about the same output, namely toFun v; injAt-out then compares the two inputs and returns the equality of the first components of fst u and fst v. The result is stated on projected first components, the form in which downstream cardinal arguments compare elements of Dom.

              → fst (fst u) ≡ fst (fst v)
    toFun-inj u v e = injAt-out zero γ ij (toFun v) (fst u) (fst v)
      (subst (λ w → ⟨ pr (fst (fst u)) w ∈ fst F ⟩) e (toFun-graph u))
      (toFun-graph v)

Restricting to the small carriers

The injection toFun acts on pairs of a model element and a membership proof, a carrier that cardinal arguments cannot count. The final step replaces both endpoints by the canonical small presentations: the domain becomes the index type of D, and the range becomes the index type of a set C supplied by the caller, which need only prove that every value of the graph lies in C. The graph clauses, single-valuedness, exact domain and injectivity, are all assumed here at once. What the presentation layer contributes is explicitness: membership in D and in C can be read off from indices and back, because the canonical embedding has proposition-valued fibers.

The parameters name the three constructible sets at play: the graph F, the domain D, and the range C. The first three hypotheses are exactly the satisfaction statements that Extract and toFun-inj consumed. The last, ran, is new: for any input x and value y with the pair (x, y) in the graph, it certifies that the underlying set of y belongs to the underlying set of C. This is a range restriction stated as a hypothesis on the caller's side, so the section itself never assumes that the graph was built with a particular range.

module Small (F D C : S)
             (sv : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩)
             (dm : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩)
             (ij : ⟨ (F ∷ D ∷ []) ⊨ injAt zero ⟩)
             (ran : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩

Under the single-valuedness and exact-domain hypotheses, Extract supplies the unique graph value for each domain member. To compare this construction with the small presentation, toS turns an index m of the canonical presentation of D into a model element. The first component is the presented set itself; the second is its constructibility certificate, obtained by isL-trans from the explicit membership member (fst D) m and the certificate that D itself is constructible. Transitivity is exactly the principle needed: a member of a constructible set is constructible.

                  → ⟨ fst y ∈ fst C ⟩) where

  module E = Extract F D sv dm

  toS : ⟪ fst D ⟫ → S
  toS m = ⟪ fst D ⟫↪ m
        , isL-trans {x = fst D} {y = ⟪ fst D ⟫↪ m} (member (fst D) m) (snd D)

Each small index must also be seen as a member of the domain in Extract's sense, and at supplies that pair: the model element toS m together with the explicit membership proof member (fst D) m. Feeding at m to the graph through E.toFun produces a value, and the range hypothesis certifies that this value belongs to C. Because the membership ⟪ fst C ⟫↪ k ≡ fst (E.toFun (at m)) in the canonical presentation is a fiber of an embedding with proposition-valued fibers, fiber returns an actual index k together with a path, not merely the truncated existence of one.

  at : ⟪ fst D ⟫ → E.Dom
  at m = toS m , member (fst D) m

  fib : (m : ⟪ fst D ⟫)
      → Σ[ k ∈ ⟪ fst C ⟫ ] (⟪ fst C ⟫↪ k ≡ fst (E.toFun (at m)))
  fib m = fiber (fst C)

Discarding the path leaves small, a function from the index type of D to the index type of C. Each domain index is sent to the index naming its image under the graph. At this point the two representations meet: small is a map between types at the fixed universe level, exactly the shape a counting argument requires, and its behavior is tied to the graph through the retained paths.

    (ran (toS m) (E.toFun (at m)) (E.toFun-graph (at m)))

  small : ⟪ fst D ⟫ → ⟪ fst C ⟫
  small m = fst (fib m)

  small-inj : (m n : ⟪ fst D ⟫) → small m ≡ small n → m ≡ n
  small-inj m n e = ↪-inj {a = fst D} {m = m} {n = n}

Injectivity of small is proved by routing an equality of indices back through the presentations. From small m ≡ small n, the path snd (fib m) is reversed to see the presented value at m, congruence under the embedding carries the equality across, and snd (fib n) lands at the presented value at n; the concatenation of the three paths, taken in exactly this direction, equates the underlying sets of the two outputs. Extract's injectivity then equates the underlying sets of the two inputs, and ↪-inj, the injectivity of the domain presentation embedding on indices, concludes m ≡ n. Two distinct injectivity facts are at work, one for the graph and one for the canonical embedding, and neither substitutes for the other.

    (E.toFun-inj ij (at m) (at n)
      (sym (snd (fib m)) ∙ cong ⟪ fst C ⟫↪ e ∙ snd (fib n)))

Recap

injAt expresses injectivity of a coded graph inside the model. Single-valuedness and an exact domain let Extract.toFun read the graph as a function into L; the separate hypothesis ij makes Extract.toFun-inj available. With the stated range condition, Small.small transfers that injection to the canonical small member types of the domain and range. The truncation step uses uniqueness of the image fiber, and the presentation step uses proposition-valued embedding fibers.