---
title: "编码单射的复合与包含"
module: L.InjectionComposition
lang: zh
site: "Bedrock"
description: "编码单射的复合与包含"
stage: "序数、单射与基数"
reading_order: 91
canonical: https://bedrock.institute/zh/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/en/L.InjectionComposition.md, https://bedrock.institute/ja/L.InjectionComposition.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 编码单射的复合与包含

本章在 `L` 内部发展两种编码单射的构造，并证明一个排除。其一，两个编码单射的复合：当某个中间值 `y` 使 `(x, y)` 落在第一个图、`(y, z)` 落在第二个图时，复合图把 `x` 关联到 `z`。其二，集合的包含由较小集合上的恒等映射编码，其图是由相等定义的有序对集合：即满足 `y = x` 的那些对 `(x, y)`。最后，从 `ω` 到有限序数平方的单射不存在。

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

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

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

图的性质与应用由模型语言的公式表达。每个变元空位对照一列元素读取，满足关系即结构的语义。这里有两个结构。外围层级提供集合本身；可构造结构提供图所居、被读取的载体。

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

外围集合的有序对由一个配对运算编码，其两个分量皆可恢复：相等的码有相等的分量。小集合带有呈现，即嵌入层级的索引类型，因此关于被呈现元素的事实可转移为关于索引的事实。可构造性是沿隶属向下封闭的谓词：可构造集合的成员是可构造的。

```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 )
```

四项材料支撑全章。序数 `ω`，连同「其成员恰为数码」的事实。数码与有限集之间的有限词典，及其抽象追逐论证。小域原理：把由可构造集合组成的任何小族界于单一层。以及 `L` 内部的分离，对任意复杂度的公式可用，下文的每个关系都由此从公共界中刻出。

```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 )
```

在 `L` 内部，语言的应用原子在常元处读取：图施于参数后仍是公式，且该读取是忠实的。单射的三条公式条件在这些原子下各有引入与消去两种形式。编码单射还可读回为其定义域与陪域的呈现之间的真正函数。

```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 )
```

单射的码是图连同全部四项条件：单值性、定义域上的全域性、单射性作为在定义域上读取的公式，外加以元语言陈述的值域条款。内部单射关系 `InjL` 仅仅地断言：这样的图连同其四项条件存在。可定义单射构造把连同定义公式一起给出的映射变成这样的码。

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

内部存在经命题截断来断言：陈述成立而无需选定见证，截断后的陈述只能消去到命题。空类型与自然数从两端抑住下文的有限论证。

```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 )
```

有的证明让一对的两个分量同时变动，二元的搬运正为此服务。在两个集合的呈现类型之间，等价把函数与单射搬运过去；集合之间的路径给出这样的等价。外围层级是本章一切成员陈述所读取的载体。

```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 )
```

层级同样地构造后继与极限：后继运算向集合添入一个元素，无穷集合 `ω` 收集诸数码，每个有限序数一个。

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

呈现把索引类型与到层级的嵌入配成一对，其纤维在元素与索引之间搬运事实。取值于命题的存在量词陈述复合所用的定义域条件。

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

可构造载体以本章一切集合所居之名打开。绝对性一章带来两种读法：在可构造结构处的满足 (为本地使用而改名)，及其抬升形式，即原子在常元列表处求值。下文图的一切应用都经过这一抬升读法。

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

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

有限一侧打开其数码词典与抽象追逐，二者都以本章只需例示的形式陈述。

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

## 共同的可构造界

用分离刻出关系，需要候选元素落在同一个可构造集合中。共享装置接收任意小索引族 `g : I → S`，返回包含每个 `g i` 的可构造集合；稍后的 `PairBound` 才把它例示于由选定定义域与陪域产生的有序对。

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

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

读取器直接陈述界的用途：族的每个成员按外围元素读取时都属于该界。此后每个被纳入 `Relation` 的对都经此读取器进入该界。

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

## 排除有限目标

后文所需的有限排除取如下形式：从 `ω` 到有限序数平方的单射不存在。这条路线几乎完全避开 `ω` 的内部隶属。所用到的只是：`ω` 的每个成员仅仅地是某个数码；每个数码呈现一个有限集，且词典在两个方向上都单射；以及一条抽象追逐。给定从每个有限呈现到某个固定类型的单射、再给定从该固定类型到某个有限呈现之平方的单射，便导出从较大有限集到较小有限集的单射。

关于 `ω` 自身的一条事实，取其隶属谓词所能支撑的强度：`ω` 的成员仅仅地是某个数码，而数码 `n` 的后继仍是数码，因而仍是成员。`γ` 与其数码的同一视沿后继搬运。

```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))
```

诸数码嵌入 `ω` 的呈现，路线是直接的。数码 `m` 的呈现的一个索引指名该数码的一个元素；该数码属于 `ω`，而由 `ω` 的传递性，被指名的元素也属于 `ω`；取 `ω` 的呈现在该元素处的纤维，即得呈现它的那个 `ω` 呈现索引。

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

嵌入是单射的。若同一数码的两个索引在 `ω` 的呈现中取值相等，两条纤维的同一视就把像的相等换成该数码内部被呈现元素的相等；而数码自身的呈现是单射的，故两个索引重合。

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

`ω` 一侧用到的单射事实只有数码呈现的单射性。

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

追逐是元理论层面关于呈现索引类型的陈述，并非内部单射关系。其假设有二：其一，对每个数码 `n`，呈现类型 `⟪ # n ⟫` 与有限集 `Fin n` 之间在两个方向各有一个单射，各自单射；其二，每个 `⟪ # m ⟫` 都有到固定类型 `⟪ ω ⟫` 的单射。其结论：从 `⟪ ω ⟫` 到 `⟪ # n ⟫ × ⟪ # n ⟫` 的单射不可能存在。

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

抽象论证恰好消耗那两本词典与到固定类型的单射族。其核心是鸽笼计数：从 `Fin (suc (n · n))` 到 `Fin (n · n)` 的单射不存在，而追逐把所设单射化归为恰是这一形状。

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

本章只需交出数码的词典与到 `ω` 呈现的嵌入。

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

该条款把排除提升到任意有限序数，且始终停留在呈现索引类型层面，保持追逐的形状：此处固定类型是 `⟪ ω ⟫`，有限呈现是诸 `⟪ # 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 β β∈ω)
```

设 `β` 是 `ω` 的序数成员，并设从 `ω` 的呈现到 `β` 之呈现的平方的函数为单射；要证的是矛盾。

```agda
  where
```

`β` 属于 `ω` 仅仅地给出一个与 `β` 同一视的数码，故只需对数码情形导出反驳；截断消去到空类型，而空类型是命题。

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

该同一视是集合之间的路径，对路径取平方便得两个平方呈现之间的等价。所设函数与该等价复合，其单射性沿等价的单位律转移：若被搬运的函数等同了两个输入，原来的函数也会等同它们。

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

于是追逐施于该数码，其矛盾正是所述鸽笼形状：从 `Fin (suc (n · n))` 到 `Fin (n · n)` 的单射。

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

## 有界有序对图所呈现的关系

`L` 中两个集合之间的关系将成为编码有序对组成的集合。界在任何公式出现之前就枚举了这些对：索引类型是定义域的一个呈现索引与陪域的一个呈现索引之积。

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

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

每个呈现索引被实现为载体的元素：即那个被呈现的集合；它是可构造集合 `D` 或 `C` 的成员，可构造性沿隶属向下搬运。

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

每一侧各为每个索引产生一个 L 元素。

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

该族把每对索引送到两个实现元素的编码有序对，共享界装置对这个族一次施用：一个可构造集合包含由 `D` 与 `C` 可能产生的一切编码对。

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

    module SB = StageBound Ix pw
```

界从该装置读出，此后只通过隶属使用；下文无需其构造。

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

读取器把界扩展到呈现之外：对 `D` 的任意元素 `x` 与 `C` 的任意元素 `z`，即便不由索引给出，其编码对仍在界内。此后每个构造触及界用的都是这个形式。

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

由于 `D` 与 `C` 是被呈现的，两个元素各有纤维：一个索引，其被呈现集合与该元素被等同。两条纤维各自独立取得。

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

两个索引构成界的族的一个索引，族在该索引处的取值是被呈现元素们的编码对，沿两条纤维路径它等于 `x` 与 `z` 的编码对。沿该相等搬运隶属，读取器即告完成。

```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)
```

从界中刻出关系需要三份数据：一个三空位公式，以及定义在有序对上的宿主谓词 `P`，连同两个方向的充分性。公式的读取次序是值、索引、对：在环境 `y ∷ x ∷ e` 下，该公式被读作 `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
```

刻画公式对两个空位作存在量化，并且除给定公式外，还在对象语言中断言第三空位编码前两者的有序对。共享界上的分离施于这个单空位公式，返回作为 `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
```

反向读取把隶属换成关于某一对的截断数据。关系的成员 `e` 由分离规格满足刻画公式；两层存在量化解开得到分量 `x`、`y`，以及「`e` 编码其对子」的证明，经充分性恢复为编码运算自身的形式，而公式部分被读成 `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
```

一切都是截断的，与该关系日后被消耗的形式一致。

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

正向由谓词构造隶属。

```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))
```

`x` 与 `y` 的编码对由界的读取器进入共享界；公式的编码条款由编码运算的计算成立，给定公式由充分性成立；分离给出隶属，并沿编码的定义性相等搬运。

```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 ∣₁ ∣₁ ))
```

对 `x` 与 `y` 的真实编码对，反向读取可锐化为非截断的结论。

```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)))
```

其见证把 `e` 呈现为某对 `x'`、`y'` 的编码对；编码的单射性把 `x'` 的底层元素等同于 `x` 的底层元素、`y'` 的等同于 `y` 的；又因可构造性是命题，这些底层等式提升为载体元素的等式。谓词随即被恰好搬到 `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))
```

## 复合编码单射

第一个的陪域是第二个的定义域时，两个编码单射可以复合。复合物仍是图，其验证从不重跑替换：两个输入图已作为集合存在，复合物只是从共享界内分离出的一个关系。模块收取两个图，以及各自的三条读取条件。

```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 ⟩)
```

除三条读取条件外，每个图还以模块的独立假设携带值域条款：第一个图的每个编码对的取值落在中间集合，第二个图的每个编码对的取值落在最终陪域。

```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 ⟩)
```

这两条条款以元语言陈述，而非公式。

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

每个「码与定义域」的对，正是三条公式条件所需的两槽环境：槽 0 放图，槽 1 放定义域。每个图一个环境。

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

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

连接关系说：当对象语言能产生中间值 `y`，使 `(x, y)` 在第一个图中、`(y, z)` 在第二个图中时，`x` 与 `z` 相关。它的截断继承自存在量词的语义：量词取值于命题，公式的满足只带有量化器内建截断意义上的见证。

```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 ⟩) ∥₁
```

刻画公式只有一个存在量化，遍历中间值。其内合取两个应用原子：第一个图以中间值居取值空位、`x` 居索引空位读取，第二个图以 `z` 居取值空位、中间值居索引空位读取。这正是 `(x, y) ∈ F` 与 `(y, z) ∈ H` 的对象语言形状。

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

应用原子的充分性把每个合取项搬到其本意的隶属：第一个搬到第一个图在 `(x, y)` 处的隶属，第二个搬到第二个图在 `(y, z)` 处的隶属。剩下的恰是截断形式的连接见证。

```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 })
```

逆向把连接见证沿同一条充分性的反向搬回对象语言。两个方向合起来说：公式与连接关系互相表达。

```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 })
```

有界关系装置被例示一次，宿主谓词取为连接关系；下文一切都从这个唯一实例读出。

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

复合图就是那个分离出的关系。

```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 ⟩) ∥₁
```

其反向读取原样继承：复合物中的一个编码对仅仅地给出中间值 `y`，使 `(x, y)` 在第一个图、`(y, z)` 在第二个图。下文四项验证都由这一条读取驱动。

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

正向读取即复合律：给定中间值 `y`，使两对分别落在两个图中，把截断的见证交给装置，装置便把 `x` 与 `z` 的编码对放进复合物。

```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 ∣₁
```

复合物现在必须以其自身资格满足四项条件，环境把复合图与第一个定义域配对。先证单值性。

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

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

设复合把 `x` 与两个值 `y`、`y'` 配对。拆开两个截断的连接得中间值 `w` 与 `w'`，`(x, w)` 与 `(x, w')` 在第一个图中。

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

第一个图的单值性等同 `w` 与 `w'`；该同一视被搬入第二个图的对子，其单值性随即等同 `y` 与 `y'`。目标是 h-集合中的路径，因而是命题，故两次截断消去都合法。

```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))
```

接着验证单射性，且两个图的使用次序重要：先用第二个图的单射性，再用第一个图的。

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

设复合把 `x` 与 `x'` 都映到 `y`。两个截断的连接给出中间值 `w` 与 `w'`：`(x, w)` 与 `(x', w')` 在第一个图中，而 `(w, y)` 与 `(w', y)` 都在第二个图中。

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

第二个图在公共值 `y` 处的单射性等同 `w` 与 `w'`；第一个图在此时公共的中间值处的单射性等同 `x` 与 `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))
```

复合在定义域上的全域性是一条等价：`x` 属于第一个定义域，当且仅当它有复合取值。两个方向一并交给引入形式。

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

一个方向直接消去第一个图的定义域条件。

```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))
```

若 `x` 有复合取值，连接见证给出中间值 `w`，使 `(x, w)` 在第一个图中；把定义域原子自身的消去施于该对，即将 `x` 放入 `D`。这个方向用不到第二个图。

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

另一方向串起两条引入。给定 `D` 中的 `x`，第一个图的定义域引入给出中间值 `w`，使 `(x, w)` 在第一个图中，其值域条款把 `w` 放入中间集。

```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 ∣₁ })
```

第二个图的定义域引入在 `w` 处产出 `z`，使 `(w, z)` 在第二个图中；第二个图的值域条款把 `z` 放入 `C`；复合律把 `x` 与 `z` 的对放进复合物。两步都是截断的，结论亦然。

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

值域条件是第二个图的值域条款在中间值处的应用。拆开复合对得到连接见证；其第二分量在第二个图内把中间值与 `z` 配对，条款随即将 `z` 放入 `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)
```

三条读取条件连同值域条款，恰是「编码单射可读回为呈现之间的函数」所需。因此复合物也承认这一读取；该模块私下承载它：公开传递出去的只是图与其四项条件，这一读取所需不外乎此。

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

## 符号化包含

包含不需要新的构造：当 `D` 包含于 `C` 时，`D` 上的恒等映射本来就是到 `C` 的映射。被编码的是这个映射的图，它在对象语言中写作取值空位与索引空位之间的相等。模块收取两个集合与逐点的包含。

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

可定义映射记录由定义域上的恒等填成：函数把每个元素送到自身，逐点包含证明每个取值落入

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

`C`。

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

图公式是两个空位之间的相等，它对函数自身取值成立是定义性的。解的唯一性用的是等式的底层等式：任何解都满足该等式，而那是底层元素之间的相等；又因可构造性是命题，这个底层等式提升为载体元素的等式。排除「与函数取值无关的解」靠的正是这一点。

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

共享构造把该映射变成带三条读取条件的图，但它要从外部收取底层函数为单射的证明。对恒等映射而言这是直接的：该假设等同两个输入的像，而在恒等映射下像的相等就是输入的相等，故所提供的、把等式原样返回的延续恰是所需的证明。

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

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

图连同全部四项条件一并作为从 `D` 到 `C` 的单射之码交付；使用者把整个包当作一个单元接收，无需打开。

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

同一个图经共享读取被读回为 `D` 与 `C` 的呈现之间的函数。这一读取由一个私有的模块承载：公开传递出去的结果只是图与其四项条件，而这正是该读取所需的全部。

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

导出的函数名为 `incl`，其路线值得注意。`D` 呈现的一个索引指名一个底层元素，该元素属于 `D`，因而由包含属于 `C`。函数随后取 `C` 自身呈现在该元素处的纤维：即呈现它的那个 `C` 索引。索引不是被直接搬运的，而是经由元素与纤维找回。

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

## 内部存在层面的包含与复合

至此的构造产出图；而内部单射关系只要求某个图存在。提升是直接的：包含给出恒等图作为见证，断言在其外围截断。包含进入基数论证所用的正是这一形式。

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

复合同样提升：`PT.rec2` 在局部分支中展开两个见证，构造其复合，再次截断结果，而不作代表的全局选择。

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

双重消去局部地拆开两个见证，用已验证的构造组装复合物，再把结果重新截断。它不作任何全局的代表选择：两个见证只作为构造的假设存在，从不被保留。

```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) ∣₁
```

复合模块承载全部验证，因此在这个层面，复合律只有一行。

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

主要实例从序数 `C` 的成员 `D` 出发。唯一的假设是 `D` 属于序数 `C`；`C` 的传递性随即断言 `D` 的每个成员都是 `C` 的成员，而这正是编码所需的逐点包含。模块对这一对打开包含构造，于是其图、码与导出映射都在同一个名字下可用。

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

## 小结

三项结果服务于内部基数论证。有限排除表明从 `ω` 到任何有限序数平方的单射不存在：`ω` 的成员仅仅地是数码，呈现类型 `⟪ # n ⟫` 与有限集 `Fin n` 在两个方向上各有一个单射，若假设存在到某个有限平方的单射，抽象追逐便导出从较大有限集到较小有限集的单射。复合把两个编码单射变成一个，经连接关系核验单值性、定义域上的全域性、单射性与值域条款。包含由恒等图把逐点包含编码为单射。在存在层面，两种操作都提升到截断的内部关系，因此基数界限的构造与比较完全可以经由居于 `L` 内部的图进行。