---
title: "Composition and inclusion of coded injections"
module: L.InjectionComposition
lang: en
site: "Bedrock"
description: "Composition and inclusion of coded injections"
stage: "Ordinals, injections and cardinals"
reading_order: 91
canonical: https://bedrock.institute/en/L.InjectionComposition.html
html: L.InjectionComposition.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/L/InjectionComposition.lagda.md
prerequisites: [Base.Prelude, Base.Classical, FOL.ZFStructure, FOL.Syntax, FOL.Absoluteness, V.Hierarchy, V.Coding, V.Presentation, L.Constructible, L.Ordinal, L.Ordinal.SquareLaw, L.Recursion, L.Axioms.Full, L.Coding.Model, L.Coding.Injection, L.Cardinal, L.DefinableInjection]
routes: [cardinal-tools]
translations: [https://bedrock.institute/zh/L.InjectionComposition.md, https://bedrock.institute/ja/L.InjectionComposition.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# Composition and inclusion of coded injections

This chapter develops two constructions of coded injections inside `L` and proves one exclusion. First, two coded injections compose: the composite is the graph relating `x` to `z` when some intermediate `y` has `(x, y)` in the first graph and `(y, z)` in the second. Second, an inclusion of sets is coded by the identity map on the smaller set, whose graph is the set of ordered pairs defined by equality: the pairs `(x, y)` with `y = x`. Finally, no injection exists from `ω` into the square of a finite ordinal.

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

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

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

Properties and applications of graphs are expressed by formulas of the model language. Each variable slot is read against a list of elements, and satisfaction is the semantics of the structures. Two structures are in play. The ambient hierarchy supplies the sets; the constructible structure supplies the carrier inside which the graphs live and are read.

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

Ordered pairs of ambient sets are coded by a pairing operation whose two components are recoverable: equal codes have equal components. Small sets come with presentations, an index type embedded into the hierarchy, so that facts about presented elements transfer to facts about indices. Constructibility is a predicate with downward closure along membership: a member of a constructible set is constructible.

```agda
open import V.Coding {ℓ} using ( pr; pr-inj )
open import V.Presentation {ℓ} using ( member; fiber; ↪-inj )
open import L.Constructible {ℓ}
  using ( 𝒮ʟ; isL; isL-trans; IsOrd )
```

Four materials carry the chapter. The ordinal `ω` with the fact that its members are exactly the numerals. The finite dictionary between numerals and finite sets, with its abstract chase argument. The small-domain principle, which bounds any small family of constructible sets by a single stage. And separation inside `L`, available for formulas of arbitrary complexity, which carves every relation below out of a shared bound.

```agda
open import L.Ordinal {ℓ} using ( ω-ord; #∈ω )
import L.Ordinal.SquareLaw {ℓ} lem as SQ
open SQ using ( module FiniteBase )
open import L.Recursion {ℓ} lem using ( smallDom )
open import L.Axioms.Full {ℓ} lem using ( hasSeparationL )
```

Inside `L`, the application atoms of the language are read at constants: a graph applied to arguments is again a formula, and this reading is faithful. The three formula conditions of an injection each have an introduction and an elimination form under these atoms. A coded injection can also be read back as a genuine function between the presentations of its domain and codomain.

```agda
open import L.Coding.Model {ℓ} using ( prAtL; prAtL-adequate; prʟ; prʟ-fst; svAt; svAt-in; svAt-out; domAt; domAt-in; domAt-out; domAt-intro )
open import L.Coding.Model {ℓ} using ( appC; appC-adequate ) public
open import L.Coding.Injection {ℓ} lem
  using ( injAt; injAt-out; injAt-in; module Small )
```

The code of an injection is the graph together with all four conditions: single-valuedness, domain totality, and injectivity as formulas read over the domain, plus the range clause stated in the meta-language. The internal injection relation `InjL` asserts, merely, that such a graph with its four conditions exists. The definable-injection construction converts a map given with a defining formula into such a code.

```agda
open import L.Cardinal {ℓ} lem using ( InjCode; InjL )
open import L.DefinableInjection {ℓ} lem
  using ( DefinableMap ) renaming ( module Inj to DefinableInj )
```

Internal existence is asserted through propositional truncation: a statement holds without a selected witness, and truncated statements eliminate only into propositions. The empty type and the natural numbers bound the finite argument below from both sides.

```agda
import Cubical.Data.Empty as Empty
import Cubical.HITs.PropositionalTruncation as PT
open PT using ( ∣_∣₁; ∥_∥₁; squash₁ )
open import Cubical.Data.Nat using ( ℕ )
open import Cubical.Data.Sigma using ( _×_; Σ≡Prop )
```

Some proofs move both components of a pair at once, and a two-place transport serves them. Between the presentation types of two sets, an equivalence carries functions and injections across; a path between sets yields such an equivalence. The ambient hierarchy is the carrier on which every membership statement of the chapter is read.

```agda
open import Cubical.Foundations.Prelude using ( subst2 )
import Cubical.Foundations.Equiv as Equiv
open Equiv using ( equivFun; invEq; retEq; _≃_ )
open import Cubical.Foundations.Univalence using ( pathToEquiv )
open import Cubical.HITs.CumulativeHierarchy.Base using ( V; _∈_; setIsSet )
```

The hierarchy builds successors and limits alike: the successor operation adds one element to a set, and the infinity set `ω` collects the numerals, one per finite ordinal.

```agda
open import Cubical.HITs.CumulativeHierarchy.Constructions
  using ( module InfinitySet )
module IS = InfinitySet {ℓ}
open IS using ( sucV; #_; ω )
```

Presentations pair index types with embeddings into the hierarchy, and their fibers move facts between elements and indices. A proposition-valued existential quantifier states the domain condition used by the composite.

```agda
open import Cubical.HITs.CumulativeHierarchy.Properties
  using ( ⟪_⟫; ⟪_⟫↪ )
open import Cubical.Functions.Logic using ( ∃[∶]-syntax )
```

The constructible carrier is opened under the name on which every set of the chapter lives. From the absoluteness development come two readings: satisfaction at the constructible structure, renamed for local use, and its raised form, in which an atom is evaluated at a list of constants. Every application of a graph to arguments below goes through the raised reading.

```agda
open hPropStructure 𝒮ʟ using ( S )

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

The finite side opens its numeral dictionary and its abstract chase, both stated in a form that this chapter only instantiates.

```agda
open FiniteBase using ( ω-mem→numeral; toFin; toFin-inj; fromFin; fromFin-inj )
open FiniteBase using ( module AbstractChase )
```

## A common constructible bound

Carving a relation by separation needs its candidates to lie in one constructible set. The shared device accepts any small indexed family `g : I → S` and returns a constructible set containing every `g i`. The later `PairBound` specializes it to the ordered pairs arising from a chosen domain and codomain.

```agda
module StageBound (I : Type ℓ) (g : I → S) where

  opaque
    bnd : S
    bnd = smallDom I g .fst
```

The reader states the bound's purpose directly: each member of the family, read as an ambient element, belongs to the bound. Every pair later admitted to a `Relation` reaches the bound through this reader.

```agda
    below : (i : I) → ⟨ fst (g i) ∈ fst bnd ⟩
    below = smallDom I g .snd
```

## Excluding finite targets

The exclusion reads: no injection exists from `ω` into the square of a finite ordinal. The route avoids the internal membership of `ω` almost entirely. What is used is that every member of `ω` is, merely, a numeral; that each numeral presents a finite set with an injective dictionary in both directions; and an abstract chase which, given injections from each finite presentation into a fixed type and an injection from that fixed type into the square of one finite presentation, derives an injection from a larger finite set into a smaller one.

A fact about `ω` itself, at the strength the membership predicate supports: a member of `ω` is, merely, a numeral, and the successor of the numeral `n` is again a numeral, hence again a member. The identification of `γ` with its numeral is transported along the successor.

```agda
ω-limit : (γ : V ℓ) → ⟨ γ ∈ ω ⟩ → ⟨ sucV γ ∈ ω ⟩
ω-limit γ γ∈ω = PT.rec (snd (sucV γ ∈ ω)) go (ω-mem→numeral γ γ∈ω)
  where
  go : Σ[ n ∈ ℕ ] (γ ≡ # n) → ⟨ sucV γ ∈ ω ⟩
  go (n , p) = subst (λ w → ⟨ sucV w ∈ ω ⟩) (sym p) (#∈ω (suc n))
```

The numerals embed into the presentation of `ω`, and the route is direct. An index of the presentation of the numeral `m` names an element of that numeral; the numeral belongs to `ω`, and by transitivity of `ω` the named element belongs to `ω` as well; the fiber of the presentation of `ω` at that element returns the index of the presentation of `ω` that presents it.

```agda
numeral-into-ω : (m : ℕ) → ⟪ # m ⟫ → ⟪ ω ⟫
numeral-into-ω m i = fiber ω (ω-ord .fst (member (# m) i) (#∈ω m)) .fst
```

The embedding is injective. If two indices of the same numeral have equal images in the presentation of `ω`, the two fiber identifications convert the equality of images into an equality of the presented elements inside that numeral; and since the numeral's own presentation is injective, the indices coincide.

```agda
numeral-into-ω-inj : (m : ℕ) (i₁ i₂ : ⟪ # m ⟫)
                   → numeral-into-ω m i₁ ≡ numeral-into-ω m i₂ → i₁ ≡ i₂
numeral-into-ω-inj m i₁ i₂ e = ↪-inj {a = # m}
  (sym (fiber ω (ω-ord .fst (member (# m) i₁) (#∈ω m)) .snd)
    ∙ cong (⟪ ω ⟫↪) e
```

The only injectivity fact used on the `ω` side is that of the numeral's presentation.

```agda
    ∙ fiber ω (ω-ord .fst (member (# m) i₂) (#∈ω m)) .snd)
```

The chase is a statement of the metatheory about presentation index types; it is not the internal injection relation. Its assumptions are, first, that for each numeral `n` the presentation type `⟪ # n ⟫` and the finite set `Fin n` admit injections in each direction, each injective on its own; second, that every `⟪ # m ⟫` admits an injection into the fixed type `⟪ ω ⟫`. Its conclusion: an injection from `⟪ ω ⟫` into `⟪ # n ⟫ × ⟪ # n ⟫` is impossible.

```agda
no-inj-finite-ω : (n : ℕ) → (f : ⟪ ω ⟫ → ⟪ # n ⟫ × ⟪ # n ⟫)
                → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → Empty.⊥
no-inj-finite-ω n f finj =
```

The abstract argument consumes exactly the dictionaries and the family of injections into the fixed type. Its core is the pigeonhole count: an injection from `Fin (suc (n · n))` into `Fin (n · n)` cannot exist, and the chase reduces the assumed injection to precisely that shape.

```agda
  AbstractChase.NoInj.no-inj
    (λ n → ⟪ # n ⟫)
    toFin toFin-inj
    fromFin fromFin-inj
    (⟪ ω ⟫)
```

The chapter only has to hand over the numerals' dictionary and the embedding into the presentation of `ω`.

```agda
    (numeral-into-ω)
    (numeral-into-ω-inj)
    n f finj
```

The clause lifts the exclusion to an arbitrary finite ordinal, and it stays at the level of presentation index types, in the shape of the chase: here the fixed type is `⟪ ω ⟫` and the finite presentations are the `⟪ # n ⟫`.

```agda
finite-excl-ω : (β : V ℓ) → IsOrd β → ⟨ β ∈ ω ⟩
              → (f : ⟪ ω ⟫ → ⟪ β ⟫ × ⟪ β ⟫)
              → ((x y : ⟪ ω ⟫) → f x ≡ f y → x ≡ y) → Empty.⊥
finite-excl-ω β oβ β∈ω f finj =
  PT.rec Empty.isProp⊥ go (ω-mem→numeral β β∈ω)
```

Let `β` be an ordinal member of `ω`, and let a function from the presentation of `ω` to the square of the presentation of `β` be injective; the claim is a contradiction.

```agda
  where
```

Membership of `β` in `ω` yields, merely, a numeral with which `β` is identified, so it is enough to refute the numeral case; the truncation is eliminated into the empty type, which is a proposition.

```agda
  go : Σ[ n ∈ ℕ ] (β ≡ # n) → Empty.⊥
  go (n , p) = no-inj-finite-ω n f' finj'
    where
```

The identification is a path between sets, and squaring the path gives an equivalence between the two squared presentations. The assumed function is composed with this equivalence, and its injectivity transfers along the equivalence's unit laws: if the transported function identified two inputs, the original would identify them too.

```agda
    e : ⟪ β ⟫ × ⟪ β ⟫ ≃ ⟪ # n ⟫ × ⟪ # n ⟫
    e = pathToEquiv (cong (λ w → ⟪ w ⟫ × ⟪ w ⟫) p)
    f' : ⟪ ω ⟫ → ⟪ # n ⟫ × ⟪ # n ⟫
    f' x = equivFun e (f x)
    finj' : (x y : ⟪ ω ⟫) → f' x ≡ f' y → x ≡ y
```

The chase then applies at the numeral, and its contradiction is of the stated pigeonhole shape, an injection from `Fin (suc (n · n))` into `Fin (n · n)`.

```agda
    finj' x y e' = finj x y
      (sym (retEq e (f x)) ∙ cong (invEq e) e' ∙ retEq e (f y))
```

## Relations as bounded pair graphs

A relation between two sets of `L` will be a set of coded ordered pairs. The bound enumerates its pairs before any formula appears: the index type is the product of one presentation index from the domain and one from the codomain.

```agda
module PairBound (D C : S) where

  Ix : Type ℓ
  Ix = ⟪ fst D ⟫ × ⟪ fst C ⟫
```

Each presentation index is realized as an element of the carrier: the presented set, which is constructible because it is a member of the constructible set `D` or `C`, the constructibility being transported down along membership.

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

    toC : ⟪ fst C ⟫ → S
```

One L-element per index, on each side.

```agda
    toC k = ⟪ fst C ⟫↪ k
          , isL-trans {x = fst C} {y = ⟪ fst C ⟫↪ k} (member (fst C) k) (snd C)
```

The family sends each pair of indices to the coded ordered pair of the two realized elements, and the shared bound device is applied once to this family: one constructible set contains every coded pair that can arise from `D` and `C`.

```agda
    pw : Ix → S
    pw (m , k) = prʟ (toD m) (toC k)

    module SB = StageBound Ix pw
```

The bound is read off the device and used from here on only through membership; nothing below needs its construction.

```agda
  bnd : S
  bnd = SB.bnd
```

The reader extends the bound beyond presentations: for arbitrary elements `x` of `D` and `z` of `C`, not given by indices, their coded pair still lies in the bound. This is the form in which every later construction touches the bound.

```agda
  below : (x z : S) → ⟨ fst x ∈ fst D ⟩ → ⟨ fst z ∈ fst C ⟩
        → ⟨ pr (fst x) (fst z) ∈ fst bnd ⟩
  below x z mx mz = subst (λ w → ⟨ w ∈ fst bnd ⟩) pa (SB.below i)
    where
```

Since `D` and `C` are presented, each of the two elements has a fiber: an index whose presented set is identified with the element. The two fibers are taken independently.

```agda
    fD : Σ[ m ∈ ⟪ fst D ⟫ ] (⟪ fst D ⟫↪ m ≡ fst x)
    fD = fiber (fst D) mx
    fC : Σ[ k ∈ ⟪ fst C ⟫ ] (⟪ fst C ⟫↪ k ≡ fst z)
    fC = fiber (fst C) mz
```

The two indices form one index of the bound's family, whose value is the coded pair of the presented elements; along the two fiber paths this equals the coded pair of `x` and `z`. Transporting membership along that equality finishes the reader.

```agda
    i : Ix
    i = fD .fst , fC .fst
    pa : fst (pw i) ≡ pr (fst x) (fst z)
    pa = prʟ-fst (toD (fD .fst)) (toC (fC .fst))
       ∙ cong₂ pr (fD .snd) (fC .snd)
```

A relation is carved from the bound given three data: a formula in three slots and a host predicate `P` on pairs, with adequacy in both directions. The reading order of the formula is value, index, pair: at the environment `y ∷ x ∷ e`, the formula is read as `P x y`.

```agda
module Relation (D C : S) (φ : Formula S 3) (P : S → S → hProp (ℓ-suc ℓ))
                (read : (x y e : S) → ⟨ (y ∷ x ∷ e ∷ []) ⊨ φ ⟩ → ⟨ P x y ⟩)
                (fill : (x y e : S) → ⟨ P x y ⟩ → ⟨ (y ∷ x ∷ e ∷ []) ⊨ φ ⟩) where
```

The carving formula quantifies the two slots existentially, and besides the given formula it asserts, in the object language, that the third slot codes the ordered pair of the first two. Separation at the shared bound, applied to this one-slot formula, returns the relation as an element of `L`.

```agda
  opaque
    fo : Formula S 1
    fo = ∃̇ (∃̇ (prAtL (suc (suc zero)) (suc zero) zero ∧̇ φ))

    rel : S
    rel = hasSeparationL (PairBound.bnd D C) fo .fst .fst
```

The backward reading turns membership into truncated data about a pair. A member `e` of the relation satisfies the carving formula by the separation specification; the two existentials unwrap to components `x` and `y` with a proof that `e` codes their pair, restored to the coding operation's own form by adequacy, and the formula part is read into `P x y`.

```agda
    out : (e : S) → ⟨ fst e ∈ fst rel ⟩
        → ∥ Σ[ x ∈ S ] Σ[ y ∈ S ] ((fst e ≡ pr (fst x) (fst y)) × ⟨ P x y ⟩) ∥₁
    out e h = PT.rec squash₁ (λ { (x , hx) → PT.map
      (λ { (y , q , hy) → x , y
         , subst ⟨_⟩ (prAtL-adequate (suc (suc zero)) (suc zero) zero (y ∷ x ∷ e ∷ [])) q
```

Everything is truncated, matching the form in which the relation will be consumed.

```agda
         , read x y e hy }) hx })
      (subst ⟨_⟩ (hasSeparationL (PairBound.bnd D C) fo .fst .snd e) h .snd)
```

The forward direction builds membership from the predicate.

```agda
    into : (x y : S) → ⟨ fst x ∈ fst D ⟩ → ⟨ fst y ∈ fst C ⟩ → ⟨ P x y ⟩
         → ⟨ pr (fst x) (fst y) ∈ fst rel ⟩
    into x y mx my h = subst (λ w → ⟨ w ∈ fst rel ⟩) (prʟ-fst x y)
      (subst ⟨_⟩ (sym (hasSeparationL (PairBound.bnd D C) fo .fst .snd (prʟ x y)))
        ( subst (λ w → ⟨ w ∈ fst (PairBound.bnd D C) ⟩) (sym (prʟ-fst x y))
```

The coded pair of `x` and `y` lies in the shared bound by the bound's reader; the coding clause of the formula holds by the coding operation's computation, and the given formula holds by adequacy; separation certifies membership, transported along the coding's definitional equality.

```agda
            (PairBound.below D C x y mx my)
        , ∣ x , ∣ y
          , subst ⟨_⟩ (sym (prAtL-adequate (suc (suc zero)) (suc zero) zero (y ∷ x ∷ prʟ x y ∷ [])))
              (prʟ-fst x y)
          , fill x y (prʟ x y) h ∣₁ ∣₁ ))
```

For the genuine coded pair of `x` and `y`, the backward reading sharpens to an untruncated conclusion.

```agda
  pair-out : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst rel ⟩ → ⟨ P x y ⟩
  pair-out x y h = PT.rec (snd (P x y))
    (λ { (x' , y' , q , h') →
      subst2 (λ a b → ⟨ P a b ⟩)
        (Σ≡Prop (λ v → snd (isL v)) (sym (pr-inj (sym (prʟ-fst x y) ∙ q) .fst)))
```

Its witness presents `e` as the coded pair of some `x'` and `y'`; injectivity of the coding identifies the underlying elements of `x'` with those of `x` and of `y'` with those of `y`; and since constructibility is a proposition, these underlying equalities lift to equalities of carrier elements. The predicate is then transported exactly to `P x y`.

```agda
        (Σ≡Prop (λ v → snd (isL v)) (sym (pr-inj (sym (prʟ-fst x y) ∙ q) .snd))) h' })
    (out (prʟ x y) (subst (λ w → ⟨ w ∈ fst rel ⟩) (sym (prʟ-fst x y)) h))
```

## Composing coded injections

Two coded injections compose when the codomain of the first is the domain of the second. The composite is again a graph, and its verification never re-runs replacement: both input graphs already exist as sets, and the composite is a relation separated inside a shared bound. The module receives the two graphs with three reading conditions each.

```agda
module Comp (D E C F H : S)
            (svF : ⟨ (F ∷ D ∷ []) ⊨ svAt zero ⟩)
            (dmF : ⟨ (F ∷ D ∷ []) ⊨ domAt zero (suc zero) ⟩)
            (ijF : ⟨ (F ∷ D ∷ []) ⊨ injAt zero ⟩)
```

Besides the three reading conditions, each graph carries its range clause as a separate assumption of the module: every coded pair of the first graph has its value in the middle set, and every coded pair of the second has its value in the final codomain.

```agda
            (ranF : (x y : S) → ⟨ pr (fst x) (fst y) ∈ fst F ⟩
                  → ⟨ fst y ∈ fst E ⟩)
            (svH : ⟨ (H ∷ E ∷ []) ⊨ svAt zero ⟩)
            (dmH : ⟨ (H ∷ E ∷ []) ⊨ domAt zero (suc zero) ⟩)
            (ijH : ⟨ (H ∷ E ∷ []) ⊨ injAt zero ⟩)
```

These two clauses are stated in the meta-language, not as formulas.

```agda
            (ranH : (y z : S) → ⟨ pr (fst y) (fst z) ∈ fst H ⟩
                  → ⟨ fst z ∈ fst C ⟩) where
```

Each pair of a code and its domain is just the two-slot environment that the three formula conditions require: slot zero holds the graph, slot one holds the domain. One environment per graph.

```agda
  private
    γF : S ^ 2
    γF = F ∷ D ∷ []

    γH : S ^ 2
    γH = H ∷ E ∷ []
```

The linking relation says: `x` and `z` are related when the object language can produce an intermediate `y` with `(x, y)` in the first graph and `(y, z)` in the second. Its truncation is inherited from the semantics of the existential quantifier, which is proposition-valued: a satisfaction of the formula carries a witness only up to the truncation built into the quantifier.

```agda
  private
    Chain : S → S → Type (ℓ-suc ℓ)
    Chain x z = ∥ Σ[ y ∈ S ] (⟨ pr (fst x) (fst y) ∈ fst F ⟩
                             × ⟨ pr (fst y) (fst z) ∈ fst H ⟩) ∥₁
```

The carving formula has a single existential, over the intermediate value. Inside it, two application atoms are conjoined: the first graph read with the intermediate in the value slot and `x` in the index slot, the second read with `z` in the value slot and the intermediate in the index slot. This is the object-language shape of `(x, y) ∈ F` and `(y, z) ∈ H`.

```agda
    opaque
      body : Formula S 3
      body = ∃̇ (appC F (suc (suc zero)) zero ∧̇ appC H zero (suc zero))
```

Adequacy of the application atoms moves each conjunct to its intended membership: the first into the first graph at the pair `(x, y)`, the second into the second graph at `(y, z)`. What remains is exactly a linking witness, in truncated form.

```agda
      read : (x z p : S) → ⟨ (z ∷ x ∷ p ∷ []) ⊨ body ⟩ → Chain x z
      read x z p = PT.map (λ { (y , hf , hh) → y
        , subst ⟨_⟩ (appC-adequate F (suc (suc zero)) zero (y ∷ z ∷ x ∷ p ∷ [])) hf
        , subst ⟨_⟩ (appC-adequate H zero (suc zero) (y ∷ z ∷ x ∷ p ∷ [])) hh })
```

The converse moves a linking witness back into the object language along the same adequacy, reversed. The two directions say that the formula and the linking relation express one another.

```agda
      fill : (x z p : S) → Chain x z → ⟨ (z ∷ x ∷ p ∷ []) ⊨ body ⟩
      fill x z p = PT.map (λ { (y , hf , hh) → y
        , subst ⟨_⟩ (sym (appC-adequate F (suc (suc zero)) zero (y ∷ z ∷ x ∷ p ∷ []))) hf
        , subst ⟨_⟩ (sym (appC-adequate H zero (suc zero) (y ∷ z ∷ x ∷ p ∷ []))) hh })
```

The bounded-relation device is instantiated once, with the linking relation as its host predicate; everything below is read off that single instance.

```agda
    module Composite = Relation D C body (λ x z → Chain x z , squash₁) read fill
```

The composite graph is the separated relation itself.

```agda
  K : S
  K = Composite.rel

  K-out : (x z : S) → ⟨ pr (fst x) (fst z) ∈ fst K ⟩
        → ∥ Σ[ y ∈ S ] (⟨ pr (fst x) (fst y) ∈ fst F ⟩
                      × ⟨ pr (fst y) (fst z) ∈ fst H ⟩) ∥₁
```

Its backward reading is inherited unchanged: a coded pair in the composite yields, merely, an intermediate `y` with `(x, y)` in the first graph and `(y, z)` in the second. This one reader drives all four verifications.

```agda
  K-out = Composite.pair-out
```

The forward reading is the composition law: given an intermediate `y` with the two pairs in the two graphs, the truncated witness is handed to the device, which places the coded pair of `x` and `z` inside the composite.

```agda
  K-in : (x y z : S) → ⟨ fst x ∈ fst D ⟩ → ⟨ fst z ∈ fst C ⟩
       → ⟨ pr (fst x) (fst y) ∈ fst F ⟩ → ⟨ pr (fst y) (fst z) ∈ fst H ⟩
       → ⟨ pr (fst x) (fst z) ∈ fst K ⟩
  K-in x y z mx mz hf hh = Composite.into x z mx mz ∣ y , hf , hh ∣₁
```

The composite must now satisfy the four conditions on its own, under the environment pairing the composite graph with the first domain. Single-valuedness is first.

```agda
  γK : S ^ 2
  γK = K ∷ D ∷ []

  svK : ⟨ γK ⊨ svAt zero ⟩
```

Suppose the composite pairs `x` with two values `y` and `y'`. Unwrapping both truncated linkings gives intermediates `w` and `w'`, with `(x, w)` and `(x, w')` in the first graph.

```agda
  svK = svAt-in zero γK (λ x y y' p q →
    PT.rec (setIsSet (fst y) (fst y'))
      (λ { (w , (hf , hh)) → PT.rec (setIsSet (fst y) (fst y'))
        (λ { (w' , (hf' , hh')) →
          svAt-out zero γH svH w y y' hh
```

Single-valuedness of the first graph identifies `w` and `w'`; the identification is transported into the second graph's pair, whose single-valuedness then identifies `y` and `y'`. The goal is a path in an h-set, hence a proposition, so both eliminations of truncations are legitimate.

```agda
            (subst (λ t → ⟨ pr t (fst y') ∈ fst H ⟩)
              (sym (svAt-out zero γF svF x w w' hf hf')) hh') })
        (K-out x y' q) })
      (K-out x y p))
```

Injectivity is verified next, and the order of the two graphs matters: the second graph's injectivity is used first, the first graph's second.

```agda
  ijK : ⟨ γK ⊨ injAt zero ⟩
```

Suppose `y` receives both `x` and `x'` under the composite. The two truncated linkings yield intermediates `w` and `w'`, with `(x, w)` and `(x', w')` in the first graph and both `(w, y)` and `(w', y)` in the second.

```agda
  ijK = injAt-in zero γK (λ y x x' p q →
    PT.rec (setIsSet (fst x) (fst x'))
      (λ { (w , (hf , hh)) → PT.rec (setIsSet (fst x) (fst x'))
        (λ { (w' , (hf' , hh')) →
          injAt-out zero γF ijF w x x' hf
```

Injectivity of the second graph at the common value `y` identifies `w` and `w'`; injectivity of the first graph at the now-common intermediate identifies `x` and `x'`.

```agda
            (subst (λ t → ⟨ pr (fst x') t ∈ fst F ⟩)
              (sym (injAt-out zero γH ijH y w w' hh hh')) hf') })
        (K-out x' y q) })
      (K-out x y p))
```

Domain totality for the composite is an equivalence: `x` belongs to the first domain precisely when it has a composite value. Both directions are supplied to the introduction form.

```agda
  dmK : ⟨ γK ⊨ domAt zero (suc zero) ⟩
  dmK = domAt-intro zero (suc zero) γK (λ x → fwd x , bwd x)
```

One direction eliminates the first graph's domain condition directly.

```agda
    where
    fwd : (x : S) → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst K) ⟩
        → ⟨ fst x ∈ fst D ⟩
    fwd x = PT.rec (snd (fst x ∈ fst D))
      (λ { (y , p) → PT.rec (snd (fst x ∈ fst D))
```

If `x` has a composite value, the linking witness exhibits an intermediate `w` with `(x, w)` in the first graph; the domain atom's own elimination, applied to that pair, places `x` in `D`. The second graph plays no role in this direction.

```agda
        (λ { (w , (hf , _)) → domAt-out zero (suc zero) γF dmF x w hf })
        (K-out x y p) })
```

The other direction chains the two introductions. Given `x` in `D`, the first graph's domain introduction yields an intermediate `w` with `(x, w)` in the first graph, and its range clause puts `w` in the middle set.

```agda
    bwd : (x : S) → ⟨ fst x ∈ fst D ⟩
        → ⟨ ∃[ y ∶ S ] (pr (fst x) (fst y) ∈ fst K) ⟩
    bwd x mx = PT.rec squash₁
      (λ { (w , hf) → PT.rec squash₁
        (λ { (z , hh) → ∣ z , K-in x w z mx (ranH w z hh) hf hh ∣₁ })
```

The second graph's domain introduction, applied at `w`, produces `z` with `(w, z)` in the second graph; the range clause of the second graph places `z` in `C`; and the composition law pairs `x` with `z` inside the composite. Both steps are truncated, and so is the conclusion.

```agda
        (domAt-in zero (suc zero) γH dmH w (ranF x w hf)) })
      (domAt-in zero (suc zero) γF dmF x mx)
```

The range condition is the second graph's range clause applied at the intermediate. Unwrapping the composite pair yields the linking witness; its second component pairs the intermediate with `z` inside the second graph, and the clause places `z` in `C`.

```agda
  ranK : (x z : S) → ⟨ pr (fst x) (fst z) ∈ fst K ⟩ → ⟨ fst z ∈ fst C ⟩
  ranK x z h = PT.rec (snd (fst z ∈ fst C))
    (λ { (w , (_ , hh)) → ranH w z hh }) (K-out x z h)
```

The three reading conditions together with the range clause are exactly what lets a coded injection be read back as a function between presentations. The composite therefore admits that reading, and this module carries it privately: what is passed on publicly are the graph and its four conditions, so the reading needs nothing beyond them.

```agda
  private
    module Sm = Small K D C svK dmK ijK ranK
```

## Coding inclusions

An inclusion needs no new construction: when `D` is contained in `C`, the identity map on `D` already maps into `C`. What is coded is that map's graph, written in the object language as equality between the value slot and the index slot. The module receives the two sets and the pointwise inclusion.

```agda
module InclGraph (D C : S)
                 (sub : (z : V ℓ) → ⟨ z ∈ fst D ⟩ → ⟨ z ∈ fst C ⟩) where
```

The definable-map record is filled with the identity on the domain: the function sends each

```agda
  private
    M : DefinableMap
    M = record
      { dom = D ; cod = C
      ; fn = λ x _ → x
```

element to itself, and the pointwise inclusion certifies that every value lands in `C`.

```agda
      ; into = λ x mx → sub (fst x) mx
```

The graph formula is equality between the two slots, and that it holds of the function's own value is definitional. Uniqueness of solutions uses the equation's underlying equality: any solution satisfies the equation, which is an equality of underlying elements, and since constructibility is a proposition, this underlying equality lifts to an equality of carrier elements. This is how unrelatedness to the function's value is excluded.

```agda
      ; graph = var zero ≐ var (suc zero)
      ; defines = λ _ _ → refl
      ; only = λ _ _ _ h → Σ≡Prop (λ w → snd (isL w)) h }
```

The shared construction turns the map into a graph with its three reading conditions, but it demands from outside a proof that the underlying function is injective. For the identity map this is immediate: the hypothesis equates the images of two inputs, and under the identity map equality of images is equality of inputs, so the supplied continuation, which returns the equation itself, is exactly the required proof.

```agda
    module I = DefinableInj M (λ _ _ _ _ e → e)
      using ( F; code )

  opaque
    G : S
    G = I.F
```

The graph with all four conditions is delivered together as the code of an injection from `D` to `C`; consumers receive the package as a unit and never need to open it.

```agda
  opaque
    unfolding G
    code : InjCode G D C
    code = I.code
```

The same graph is read back through the shared reading as a function between the presentations of `D` and `C`. This reading is carried in a private module, because the results that pass on publicly are the graph and its four conditions, and those are all the reading needs.

```agda
  private
    module Sm = Small G D C (code .fst) (code .snd .fst)
      (code .snd .snd .fst) (code .snd .snd .snd)
```

The induced function is named `incl`, and its route matters. An index of `D`'s presentation names an underlying element, which belongs to `D` and therefore, by the inclusion, to `C`. The function then takes the fiber of `C`'s own presentation at that element: the index of `C` presenting it. The index is not transported directly; it is recovered through the element and the fiber.

```agda
  opaque
    incl : ⟪ fst D ⟫ → ⟪ fst C ⟫
    incl = Sm.small
```

## Inclusion and composition at the internal-existence level

The constructions so far produce graphs; the internal injection relation asks only that a graph exist. The lift is immediate: an inclusion yields the identity graph as witness, and the assertion is truncated around it. This is the form in which inclusions reach the cardinal arguments.

```agda
inclusion-coded : (a b : S)
                → ((z : V ℓ) → ⟨ z ∈ fst a ⟩ → ⟨ z ∈ fst b ⟩)
                → InjL a b
inclusion-coded a b sub = ∣ I.G , I.code ∣₁
  where module I = InclGraph a b sub
```

Composition lifts in the same way: `PT.rec2` exposes both witnesses locally, builds their composite, and truncates the result again, without making a global choice of representatives.

```agda
injl-trans : (a b c : S) → InjL a b → InjL b c → InjL a c
injl-trans a b c = PT.rec2 PT.squash₁ step
  where
```

The two-fold elimination locally unwraps the two witnesses, assembles the composite by the verified construction, and truncates the result again. It performs no global choice of representatives: the witnesses exist only as hypotheses of the construction and are never retained.

```agda
  step : Σ[ F ∈ S ] InjCode F a b
       → Σ[ H ∈ S ] InjCode H b c
       → InjL a c
  step (F , svF , dmF , ijF , ranF) (H , svH , dmH , ijH , ranH) =
    ∣ K.K , (K.svK , K.dmK , K.ijK , K.ranK) ∣₁
```

The composite module carries the whole verification, so at this level the composition law is a single line.

```agda
    where
    module K = Comp a b c F H svF dmF ijF ranF svH dmH ijH ranH
```

The principal instance starts from a member `D` of an ordinal `C`. The only assumption is that `D` belongs to the ordinal `C`; transitivity of `C` then says that every member of `D` is a member of `C`, which is exactly the pointwise inclusion the coding requires. The module opens the inclusion construction for this pair, so its graph, code, and induced map are all available under one name.

```agda
module OrdIncl (C : S) (oC : IsOrd (fst C))
               (D : S) (D∈C : ⟨ fst D ∈ fst C ⟩) where

  open InclGraph D C (λ _ z∈D → oC .fst z∈D D∈C) public
```

## Recap

Three results serve the internal cardinal arguments. The finite exclusion shows that no injection exists from `ω` into the square of a finite ordinal: a member of `ω` is, merely, a numeral, the presentation types `⟪ # n ⟫` and the finite sets `Fin n` admit injections in each direction, and the abstract chase derives, from any assumed injection into a finite square, an injection from a larger finite set into a smaller one. The composition turns two coded injections into one, verifying single-valuedness, domain totality, injectivity, and the range clause through the linking relation. The inclusion codes pointwise containment by the identity graph. At the existence level, both operations lift to the truncated internal relation, so cardinal bounds can be built and compared entirely through graphs living inside `L`.