---
title: "Coded injections"
module: L.Coding.Injection
lang: en
site: "Bedrock"
description: "Coded injections"
stage: "Ordinals, injections and cardinals"
reading_order: 88
canonical: https://bedrock.institute/en/L.Coding.Injection.html
html: L.Coding.Injection.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/Coding/Injection.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, L.Constructible, L.Coding.Model, V.Presentation]
routes: [cardinal-tools]
translations: [https://bedrock.institute/zh/L.Coding.Injection.md, https://bedrock.institute/ja/L.Coding.Injection.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

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

```agda
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.

```agda
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.

```agda
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`.

```agda
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.

```agda
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.

```agda
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.

```agda
        → ((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.

```agda
        → ((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.

```agda
            → (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.

```agda
  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.

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

  γ : S ^ 2
  γ = 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.

```agda
  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.

```agda
  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`.

```agda
  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.

```agda
  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`.

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

```agda
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.

```agda
                  → ⟨ 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.

```agda
  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.

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

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